<figure><img src="image_1.png" /></figure>

ifip

International Federation for Information Processing

This document is the original author manuscript of a paper submitted to an IFIP
conference proceedings or other IFIP publication by Springer Nature. As such, there
may be some differences in the official published version of the paper. Such
differences, if any, are usually due to reformatting during preparation for publication or
minor corrections made by the author(s) during final proofreading of the publication
manuscript.
# Operations on Timed Scenarios

Neda Saeedloei¹(✉) and Feliks Kluzniak²

¹ Towson University, Towson, USA
nsaeedloei@towson.edu

² RelationalAI, Berkeley, USA
feliks.kluzniak@relational.ai

**Abstract.** We introduce three operations for timed scenarios: subsump-
tion, intersection and union. They have constructive definitions based on
the syntactic properties of the constituent scenarios. We show that they
have the desired semantic properties. These results expand the theory of
timed scenarios, but their development was inspired by practical consid-
erations: they are directly relevant to the problem of synthesizing a timed
automaton with a minimal number of clocks from a set of scenarios.

## 1 Introduction

Using scenarios for specification and implementation of complex systems (includ-
ing real time systems and distributed systems [1,2]), and synthesizing formal
models of systems from scenarios have been active areas of research for several
decades [3–10].

In our earlier work [11] we developed, from first principles, a formal, yet
simple notation for timed scenarios. Intuitively, a scenario is a sequence of events
along with a set of constraints between the times of these events. It can be used
to specify the partial behaviours of a system or a component of a system. Our
scenarios can be used as a general formalism for modeling the behaviours of a
variety of complex systems, including distributed systems.

We defined the semantics of a timed scenario as the set of all *behaviours*
(a.k.a timed words [12]) that are allowed by the scenario.

One of our objectives is to use our scenarios to automatically synthesize
formal models in the form of timed automata [12] with a *minimal number of
clocks*. This is important, since the number of clocks crucially affects the cost of
verification of timed automata [13].

As part of our earlier work [11] we obtained a canonical representation (a
“stable distance table”) for the entire class of scenarios that are equivalent to a
given one. We used stable distance tables as a linchpin of various algorithms for
determining the consistency and equivalency of scenarios, as well as for optimiz-
ing scenarios [14,15].

In the current paper we use our stable distance tables once more to develop
the notions of intersection, union and subsumption for timed scenarios. We
introduce appropriate operations with well-defined semantics for computing the
intersection and union of two consistent scenarios, as well as for determining
whether a scenario is subsumed by another one.

Intuitively, given two consistent scenarios, their intersection is a scenario that expresses all those behaviours that are allowed by both, while their union is a scenario that captures all the behaviours that are allowed by either of them or both. A scenario is subsumed by another one if its set of behaviours is subsumed by that of the other one.

Having defined these operations, we develop some interesting relationships between them. In particular, we study the conditions under which the union of the behaviours allowed by two scenarios can be represented by a single scenario.

These operations are directly relevant to the problem of synthesizing timed automata from a set of scenarios, which is not addressed in the current paper.

# 2 Preliminaries

## 2.1 Timed Automata

A timed automaton [12] is a tuple $\mathcal{A} = (\Sigma, Q, q_0, Q_f, C, T)$, where $\Sigma$ is a finite alphabet, $Q$ is the (finite) set of locations, $q_0 \in Q$ is the initial location, $Q_f \subseteq Q$ is the set of final locations, $C$ is a finite set of clock variables (clocks for short), and $T \subseteq Q \times Q \times \Sigma \times 2^C \times 2^{\Phi(C)}$ is the set of transitions. In each transition $(q, q', e, \lambda, \phi)$, $\lambda$ is the set of clocks to be reset with the transition and $\phi \subseteq \Phi(C)$ is a set of clock constraints over $C$ of the form $c \sim a$ (where $\sim \in \{\leq, <, \geq, >, =\}$, $c \in C$ and $a$ is a constant in the set of rational numbers, $\mathbb{Q}$). A clock valuation $\nu$ for $C$ is a mapping from $C$ to $\mathbb{R}^{\ge 0}$. Clock valuation $\nu$ satisfies a set of clock constraints $\phi$ over $C$ iff every clock constraint in $\phi$ evaluates to true after each clock $c$ is replaced with $\nu(c)$. For $\tau \in \mathbb{R}$, $\nu + \tau$ denotes the clock valuation which maps every clock $c$ to the value $\nu(c) + \tau$. For $Y \subseteq C$, $[Y \mapsto \tau]\nu$ is the valuation which assigns $\tau$ to each $c \in Y$ and agrees with $\nu$ over the rest of the clocks.

A timed word over an alphabet $\Sigma$ is a pair $(\sigma, \tau)$ where $\sigma = \sigma_1\sigma_2...$ is a finite [16,17] or infinite [12] word over $\Sigma$ and $\tau = \tau_1\tau_2...$ is a finite or infinite sequence of (time) values such that (i) $\tau_i \in \mathbb{R}^{\ge 0}$, (ii) $\tau_i \le \tau_{i+1}$ for all $i \ge 1$, and (iii) if the word is infinite, then for every $t \in \mathbb{R}^{\ge 0}$ there is some $i \ge 1$ such that $\tau_i > t$.

A run $\rho$ of $\mathcal{A}$ over a timed word $(\sigma, \tau)$ is a finite or infinite sequence of the form $\langle q_0, \nu_0 \rangle \xrightarrow{\sigma_1}{\tau_1} \langle q_1, \nu_1 \rangle \xrightarrow{\sigma_2}{\tau_2} \langle q_2, \nu_2 \rangle \xrightarrow{\sigma_3}{\tau_3} ...$, where for all $i \ge 0$, $q_i \in Q$ and $\nu_i$ is a clock valuation such that (i) $\nu_0(c) = 0$ for all clocks $c \in C$ and (ii) for every $i > 1$ there is a transition in $T$ of the form $(q_{i-1}, q_i, \sigma_i, \lambda_i, \phi_i)$, such that $(\nu_{i-1} + \tau_i - \tau_{i-1})$ satisfies $\phi_i$, and $\nu_i$ equals $[\lambda_i \mapsto 0](\nu_{i-1} + \tau_i - \tau_{i-1})$.

A run over a finite timed word is *accepting* if it ends in a final location [17]. The *language* of $\mathcal{A}$, $L(\mathcal{A})$, is the set $\{(\sigma, \tau) \mid \mathcal{A} \text{ has an accepting run}^1 \text{ over } (\sigma, \tau)\}$.

## 2.2 Timed Scenarios

(This subsection briefly recounts our earlier work [11,14].)

<footnote n="1">¹ In this work we only consider finite runs.</footnote>
<table><caption>**Fig. 1.** Two equivalent scenarios</caption><thead><tr><th></th><th></th><th></th><th></th><th></th><th></th><th></th><th></th></tr></thead><tbody><tr><td>0 : a ;</td><td>0 : a ;</td><td>1</td><td>2</td><td>3</td><td>1</td><td>2</td><td>3</td></tr><tr><td>1 : b {τ<sub>0,1</sub> ≤ 1} ;</td><td>1 : b {τ<sub>0,1</sub> ≤ 1} ;</td><td>0</td><td>(0, 1)</td><td>(0, ∞)</td><td>(5, 5)</td><td>0</td><td>(0, 1)</td><td>(3, 5)</td><td>(5, 5)</td></tr><tr><td>2 : c ;</td><td>2 : c {τ<sub>0,2</sub> ≥ 3} ;</td><td>1</td><td>(0, ∞)</td><td>(0, ∞)</td><td></td><td>1</td><td>(2, 5)</td><td>(4, 5)</td><td></td></tr><tr><td>3 : d {τ<sub>0,3</sub> = 5, τ<sub>2,3</sub> ≤ 2} .</td><td>3 : d {τ<sub>0,3</sub> = 5} .</td><td>2</td><td>(0, 2)</td><td></td><td></td><td>2</td><td>(0, 2)</td><td></td><td></td></tr><tr><td>γ</td><td>η</td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td></tr></tbody></table>

<caption>**Fig. 2.** $\gamma$'s initial table and its stable form</caption>

Let $\Sigma$ be a finite set of symbols called *events*. A *behaviour* over $\Sigma$ is a sequence $(e_0, t_0)(e_1, t_1)(e_2, t_2)\dots$, such that $e_i \in \Sigma$, $t_i \in \mathbb{R}^{\ge 0}$ and $t_{i-1} \le t_i$ for $i \in \{1, 2, \dots\}$. For a finite behaviour $\mathcal{B} = (e_0, t_0)(e_1, t_1)\dots(e_{n-1}, t_{n-1})$ of length $n$, and for any $0 \le i < j < n$, the *distance*, in time units, of event $j$ from event $i$ in $\mathcal{B}$ is denoted by $t_{ij}^B$. That is, $t_{ij}^B = t_j - t_i$.

A *timed scenario* (*scenario* for short) of length $n \in \mathbb{N}$ over $\Sigma$ is a pair $(\mathcal{E}, \mathcal{C})$, where $\mathcal{E} = e_0 e_1 \dots e_{n-1}$ is a sequence of events, and $\mathcal{C} \subset \mathcal{F}(n)$ is a finite set of constraints. Each constraint in $\mathcal{F}(n)$ is of the form $b \sim a$, where $b$ is the symbol $\tau_{i,j}$ (for some integers $0 \le i < j < n$), $\sim \in \{\le, \ge\}^2$ and $a$ is a constant in the set of rational numbers, $\mathbb{Q}$. The intended interpretation is that $\tau_{i,j}$ is the time distance between the $i$-th and the $j$-th events in the behaviours described by a timed scenario.

A scenario will be written as a sequence of events, separated by semicolons and terminated by a period. If the scenario contains a constraint such as $\tau_{i,j} \sim a$, then event $j$ in the sequence will be accompanied by the constraint. Equality will be expressed directly using $=$, rather than in terms of $\le$ and $\ge$. We refer to this as the external representation of the scenario. Scenario $\gamma$ in Fig. 1 is the external representation of scenario $(abcd, \{\tau_{0,1} \le 1, \tau_{0,3} \ge 5, \tau_{0,3} \le 5, \tau_{2,3} \le 2\})$.

A behaviour $\mathcal{B} = (e_0, t_0)(e_1, t_1)\dots(e_{n-1}, t_{n-1})$ over $\Sigma$ is allowed by scenario $\xi = (\mathcal{E}, \mathcal{C})$ iff $\mathcal{E} = e_0 \dots e_{n-1}$ and every $\tau_{i,j} \sim a$ in $\mathcal{C}$ evaluates to true after $\tau_{i,j}$ is replaced by $t_{ij}^B$. If $\mathcal{B}$ is allowed by $\xi$, then we say $\mathcal{B}$ satisfies all constraints of $\xi$.

The constraints $\tau_{i,j} \ge 0$ and $\tau_{i,j} \le \infty$, which always evaluate to true after we replace them with some $t_{ij}^B$, will be called *default constraints*.

The semantics of scenario $\xi$, denoted by $[[\xi]]$, is the set of behaviours that are allowed by $\xi$. For scenario $\gamma$ in Fig. 1 $[[\gamma]] = \{(a, t_0)(b, t_1)(c, t_2)(d, t_3) \mid t_3 \ge t_2 \ge t_1 \ge t_0 \wedge t_1 - t_0 \le 1 \wedge t_3 - t_0 = 5 \wedge t_3 - t_2 \le 2\}$.

A scenario $\xi$ is *consistent* iff $[[\xi]] \neq \emptyset$. It is *inconsistent* iff $[[\xi]] = \emptyset$.

Two scenarios $\xi = (\mathcal{E}, C_1)$ and $\eta = (\mathcal{E}, C_2)$ are *equivalent* iff $[[\xi]] = [[\eta]]$. For example, $\gamma$ and $\eta$ of Fig. 1 are equivalent.

For a consistent scenario $\xi$ of length $n$, and for $0 \le i < j < n$, $m_{ij}^\xi = \min\{t_{ij}^B \mid \mathcal{B} \in [[\xi]]\}$ and $M_{ij}^\xi = \max\{t_{ij}^B \mid \mathcal{B} \in [[\xi]]\}$. The absence of an upper bound for some $i$ and $j$ will be denoted by $M_{ij}^\xi = \infty$. We will write just $m_{ij}$ and $M_{ij}$ when $\xi$ is understood. For any behaviour in $[[\xi]]$, $0 \le m_{ij} \le t_{ij} \le M_{ij} \le \infty$.

<footnote n="2">² To keep the presentation compact, sharp inequalities are not allowed [11]. Equality is expressed in terms of $\le$ and $\ge$.</footnote>
For a consistent scenario $\xi$ of length $n$, and for any $0 \le i < j < k < n$ the following inequations hold [11]:

$$m_{ij} + m_{jk} \le m_{ik} \le \left\{ \begin{array}{l} m_{ij} + M_{jk} \\ M_{ij} + m_{jk} \end{array} \right\} \le M_{ik} \le M_{ij} + M_{jk} \quad (1)$$

Let $\xi = (\mathcal{E}, \mathcal{C})$ be a scenario of length $n$, such that, for any $0 \le i < j < n$, $\mathcal{C}$ contains at most one constraint of the form $\tau_{i,j} \ge c$ and at most one of the form $\tau_{i,j} \le c$. A distance table for $\xi$ is a representation of $\mathcal{C}$ in the form of a triangular matrix $\mathcal{D}^{\xi}$. For $0 \le i < j < n$, $\mathcal{D}^{\xi}[i,j] = (l_{ij}^{\xi}, h_{ij}^{\xi})$, where $l_{ij}^{\xi}$ and $h_{ij}^{\xi}$ are rational numbers. If $\tau_{i,j} \ge c \in \mathcal{C}$ then $l_{ij}^{\xi} = c$, otherwise $l_{ij}^{\xi} = 0$; if $\tau_{i,j} \le c \in \mathcal{C}$ then $h_{ij}^{\xi} = c$, otherwise $h_{ij}^{\xi} = \infty$. We will write just $l_{ij}$ and $h_{ij}$ when $\xi$ is understood. The distance table corresponding to $\gamma$ of Fig. 1 is shown on the left of Fig. 2.

A distance table of size $n$ is valid iff $l_{ij} \le h_{ij}$, for all $0 \le i < j < n$. A table that is not valid is invalid. If $\mathcal{D}^{\xi}$ is invalid, then $\xi$ is obviously inconsistent.

A valid distance table of size $n$ is stable iff, for all $0 \le i < j < k < n$, the inequations in (1) hold when $m_{ij}$, $m_{jk}$, $m_{ik}$ are replaced by $l_{ij}$, $l_{jk}$, $l_{ik}$ and $M_{ij}$, $M_{jk}$, $M_{ik}$ are replaced by $h_{ij}$, $h_{jk}$, $h_{ik}$. If $\mathcal{D}^{\xi}$ is stable then $\xi$ is consistent.

To stabilize $\mathcal{D}^{\xi}$ the following six rules are repeatedly applied until the table becomes either invalid or stable<fnref n="3" /> [11]. The stabilized table is denoted by $\mathcal{D}_s^{\xi}$.

$$\begin{align*} l_{ij} + l_{jk} > l_{ik} &\rightarrow l_{ik} := l_{ij} + l_{jk} & l_{ik} > l_{ij} + h_{jk} &\rightarrow l_{ij} := l_{ik} - h_{jk} \\ l_{ik} > h_{ij} + l_{jk} &\rightarrow l_{jk} := l_{ik} - h_{ij} & l_{ij} + h_{jk} > h_{ik} &\rightarrow h_{jk} := h_{ik} - l_{ij} \\ h_{ij} + l_{jk} > h_{ik} &\rightarrow h_{ij} := h_{ik} - l_{jk} & h_{ik} > h_{ij} + h_{jk} &\rightarrow h_{ik} := h_{ij} + h_{jk} \end{align*}$$

At least one of these rules is applicable if and only if some inequation in (1) does not hold. The purpose of each rule is to tighten a constraint just enough to establish a particular inequation. A stable distance table<fnref n="4" /> has two properties. First, as a result of applying the rules above, the table includes all the constraints that are implied (see definitions 1 and 2) by the initial set of constraints. Second, all the constraints represented by the table are as tight as possible:

**Observation 1.** Let $\xi$ be a scenario of length $n$. If $\mathcal{D}_s^{\xi}$ is its stable table, then for every $0 \le i < j < n$, $l_{ij} = m_{ij}$ and $h_{ij} = M_{ij}$, that is, $\mathcal{D}_s^{\xi}[i, j] = (m_{ij}^{\xi}, M_{ij}^{\xi})$.

$\mathcal{D}_s^{\xi}[i, j]$ specifies the set of all the possible values of $t_{ij}$ that can appear in the behaviours allowed by the corresponding scenario.

Two scenarios $\xi$ and $\eta$ are equivalent iff $\mathcal{D}_s^{\xi} = \mathcal{D}_s^{\eta}$. The table on the right-hand side of Fig. 2 is the stable distance table obtained from the constraints of either $\gamma$ or $\eta$ (which shows that they are equivalent: $\llbracket \gamma \rrbracket = \llbracket \eta \rrbracket$).

<footnote n="3">³ The cost is $O(n^3)$, where $n$ is the length of the scenario [11].</footnote>

<footnote n="4">⁴ The stable distance tables, though derived in a very different fashion, turned out to be essentially equivalent to Dill's Difference Bounds Matrices (DBMs) [18]. However, when applied to the particular case of scenarios, the constraint reduction technique for DBMs [19] is weaker than our optimisation algorithms [14, 15]. A detailed comparison can be found in our earlier work [14].</footnote>
Given a scenario $\xi$ with its stable distance table $\mathcal{D}_s^\xi$, we use $\mathcal{C}(\mathcal{D}_s^\xi)$ to denote the set of constraints represented by $\mathcal{D}_s^\xi$.

**Definition 1.** Let $\xi$ be a scenario of length $n$, $\mathcal{D}_s^\xi$ be its stable table, $c \in \mathcal{C}(\mathcal{D}_s^\xi)$ be a non-default constraint, $S \subset \mathcal{C}(\mathcal{D}_s^\xi)$, and $0 \le i < j < k < n$. Constraint $c$ is directly supported by $S$, denoted by $S \rightsquigarrow c$, iff $c$ and $S$ satisfy one of the following six conditions:

1. $c = \tau_{i,k} \ge u, S = \{\tau_{i,j} \ge v, \tau_{j,k} \ge w\}$, and $u = v + w$.

2. $c = \tau_{i,j} \ge u, S = \{\tau_{i,k} \ge v, \tau_{j,k} \le w\}$, and $u = v - w$.

3. $c = \tau_{j,k} \ge u, S = \{\tau_{i,k} \ge v, \tau_{i,j} \le w\}$, and $u = v - w$.

4. $c = \tau_{j,k} \le u, S = \{\tau_{i,k} \le v, \tau_{i,j} \ge w\}$, and $u = v - w$.

5. $c = \tau_{i,j} \le u, S = \{\tau_{i,k} \le v, \tau_{j,k} \ge w\}$, and $u = v - w$.

6. $c = \tau_{i,k} \le u, S = \{\tau_{i,j} \le v, \tau_{j,k} \le w\}$, and $u = v + w$.

Each of the cases in Definition 1 corresponds to one of the six rules of stabilization mentioned before. For example, if $m_{13} = 3$, $M_{36} = 4$ and $m_{16} = 0$ (i.e., the corresponding constraint is missing), then the first rule will force $m_{16}$ to be 7: the constraint $m_{16} = 7$ is directly supported by the other two.

**Definition 2.** (quasi-transitivity) Let $\mathcal{D}_s^\xi$ be a stable table. $\rightsquigarrow^+ \subset 2^{\mathcal{C}(\mathcal{D}_s^\xi)} \times \mathcal{C}(\mathcal{D}_s^\xi)$ is the smallest relation that satisfies the following two conditions:

1. If $S \rightsquigarrow c$ then $S \rightsquigarrow^+ c$;

2. If $S \rightsquigarrow^+ c$ and there is a constraint $d \in S$ such that, for some $S' \in \mathcal{C}(\mathcal{D}_s^\xi)$, $S' \rightsquigarrow^+ d$ and $c \notin S'$, then $(S \setminus \{d\}) \cup S' \rightsquigarrow^+ c$.

Constraint $c$ is supported by $S$ when $S \rightsquigarrow^+ c$. $S$ is then called a support of $c$.

If $S \rightsquigarrow^+ c$, then we say that $c$ is implied by $S$.

Intuitively, if a constraint $d$ has a support, then $d$ can be removed from the scenario. The removed $d$ can be a member of the supports of other constraints, e.g., $d$ can appear in a set $S$ that supports $c$. As long as $d$ has a support $S'$ that does not include $c$, $S$ can be updated by replacing $d$ with $S'$. The relation $\rightsquigarrow^+$ captures all the possible supports for the constraints in $\mathcal{C}(\mathcal{D}_s^\xi)$.

**Observation 2.** If $S \rightsquigarrow^+ c$, then $c \notin S$.

**Observation 3.** Let $S \rightsquigarrow^+ c$. If behaviour $B$ satisfies all the constraints in $S$, then it also satisfies $c$.

## 2.3 Timed Scenarios and Timed Automata

If $\xi = (\mathcal{E}, \mathcal{C})$ is a scenario of length $n$, and $\mathcal{C}$ contains a constraint $\tau_{i,j} \sim a$ for some $0 \le i < j < n$, and some $a \in \mathbb{Q}$, then the index $i$ is an anchor. For an anchor $i$, if $0 < j < n$ is the largest number such that $\tau_{i,j} \sim a$ is a constraint in $\mathcal{C}$, then $[i, j)$ is the range of anchor $i$. If $i_1$ and $i_2$ are two anchors with ranges $[i_1, j_1)$ and $[i_2, j_2)$ in $\xi$, then the two ranges overlap iff $i_1 < i_2 < j_1$ or $i_2 < i_1 < j_2$.

For example, in scenario $\gamma$ of Fig. 1, the range of anchor 0 is $[0, 3)$ and the range of anchor 2 is $[2, 3)$: these are overlapping.
<figure><img src="image_2.png" /></figure>

<figure><img src="image_3.png" /><figcaption>Fig. 3. Equivalent timed automata corresponding to the scenarios of Fig. 1</figcaption></figure>

Anch$_{ξ}$ is used to denote the set of anchors of $ξ$. If $X$ is a set of clock variables, then the relation $alloc_{ξ} \subset Anch_{ξ} \times X$ is a clock allocation for $ξ$. $alloc_{ξ}$ is complete iff for every anchor $i \in Anch_{ξ}$ there is a clock $x \in X$ such that $(i, x) \in alloc_{ξ}$. $alloc_{ξ}$ is incorrect iff there exist two different anchors $i$ and $j$ in $Anch_{ξ}$ whose ranges overlap, such that $(i, x) \in alloc_{ξ}$ and $(j, x) \in alloc_{ξ}$ for some $x \in X$. $alloc_{ξ}$ is correct iff it is not incorrect. A correct and complete clock allocation is optimal if there is no other correct and complete allocation that uses fewer clocks. ${\{(0, x), (2, y)\}}$ is an optimal clock allocation for scenario $γ$ of Fig. 1.

A scenario $ξ$ can be trivially converted to a simple timed automaton $A_ξ$: the language of $A_ξ$ is equivalent to the set of behaviours allowed by $ξ$: $L(A_ξ) = [[ξ]]$.

A scenario $ξ$, can be transformed to an equivalent scenario $η$, by optimizing its set of constraints [15], so that (i) $η$ has a minimal set of constraints<fnref n="5" />, and (ii) $A_η$ has the *minimal* number of clocks in the entire class of timed automata obtained from all scenarios equivalent to $ξ$. We call $η$ the *optimized* form of $ξ$.

For example, scenario $η$ of Fig. 1 is the optimized form of $γ$ in that figure. Their corresponding language-equivalent timed automata are shown in Fig. 3. Notice that $A_η$ has only one clock, while $A_γ$ requires two clocks.

## 3 Operations on Scenarios and the Synthesis Problem

In this section we briefly present the motivation behind developing the notions of *subsumption*, *intersection*, and *union* for timed scenarios.

Given a finite set $Ξ$ of scenarios, our ultimate goal is to synthesize a timed automaton $A_Ξ$ whose language would be $\bigcup_{\xi \in \Xi} [[\xi]]^6$. We want $A_Ξ$ to have the minimal number of clocks in the entire class of language-equivalent timed automata.

Let $Ξ_o$ be the set of optimized scenarios obtained from the members of $Ξ$. Let $Γ_ε = \{(E, C^0), (E, C^1), ...\} \subseteq Ξ_o$, i.e., the set of those members of $Ξ_o$ that have $E$ as their sequence of events. The members of $Γ_ε$ may be involved in interesting relationships that may have a bearing on the best way to reach our goal.

**Subsumption.** If $Γ_ε$ contains two scenarios $ξ$ and $η$, such that $[[ξ]] \subseteq [[η]]$, then $ξ$ can be removed from $Ξ$. This cannot increase the number of clocks in $A_Ξ$, but may decrease it, so such subsumed scenarios should always be removed.

For example, consider scenarios $ξ$ and $γ$ of Fig. 4. Notice that $[[ξ]] \subseteq [[γ]]$, that is, $ξ$ is subsumed by $γ$ (see Definition 4 in Sec. 4). So $ξ$ can be removed from $Ξ$.

<footnote n="5">⁵ That is, a constraint cannot be removed without changing the semantics.</footnote>

<footnote n="6">⁶ The complete account of the synthesis problem is addressed in a forthcoming paper.</footnote>
<figure><img src="image_4.png" /><figcaption>**Fig. 4.** Two scenarios $\xi$ and $\eta$ with complementary constraints, and their combination</figcaption></figure>

This removal will result in a reduction in the number of clocks in the synthesized automaton: the two anchors in $\xi$ have overlapping ranges, so $A_\xi$ would require two clocks, but $A_\gamma$ would only require one clock.

**Union.** The set $\Gamma_\epsilon$ may contain a subset $S$, such that $|S| > 1$, but all its members can be replaced by a single scenario. More precisely, there may exist a scenario $\eta$ such that $[[\eta]] = \bigcup_{\xi \in S} [[\xi]]$. We then say that the members of $S$ can be combined. Combining scenarios can, in general, result in a reduction in the number of clocks in the synthesized automaton. We discuss this for a very simple case.

Let $\xi = (\mathcal{E}, C^\xi)$ and $\eta = (\mathcal{E}, C^\eta)$ in $\Gamma_\epsilon$ be such that they can be combined into one scenario. Let the scenarios contain a pair of explicit constraints that are complementary, i.e., for some $i, j$ and $a$ we have $\tau_{i,j} \le a \in C^\xi$ and $\tau_{i,j} \ge a \in C^\eta$. Then in the combined scenario (see Definition 6 in Sec. 4) the only constraints on $\tau_{i,j}$ will be implicit default constraints.

As an example consider scenarios $\xi$ and $\eta$ of Fig. 4. These two scenarios can be combined: $[[\xi]] \cup [[\eta]]$ is captured by scenario $\gamma$ in that figure. That is, $\xi$ and $\eta$ can be replaced by $\gamma$ in $\Xi$. Notice that $\xi$ and $\eta$ each have two anchors 0 and 1 whose ranges overlap. Therefore $A_\xi$ and $A_\eta$ each would require two clocks. So the number of clocks in the automaton synthesized from $\xi$ and $\eta$ cannot be smaller than 2. However, a language-equivalent automaton synthesized from $\gamma$ would require only one clock: by combining $\xi$ and $\eta$ we got rid of the pair of complementary constraints, (i.e., $\tau_{1,2} \le 5$ and $\tau_{1,2} \ge 5$) and thus of anchor 1.

In general, there are two situations where combining scenarios results in a reduction in the number of clocks in a synthesized automaton. One is when an anchor $i$ disappears entirely, and another when the number of ranges that overlap with the range of $i$ decreases.

So before we begin the synthesis process we should try to combine scenarios with identical sequences of events.

**Intersection.** $\Gamma_\epsilon$ might contain two scenarios $\xi$ and $\eta$, such that $[[\xi]] \cap [[\eta]] \ne \emptyset$. In that case, the intersection can be expressed by a timed scenario.

Computing the intersection of a set of scenarios is not directly relevant to our task, but will be useful in computing their union (see Sec. 4 for details).

Next, we formally define these three operations.
4 Subsumption, Intersection and Union

For a given scenario $\xi = (\mathcal{E}, \mathcal{C})$ the members of $\mathcal{C}$ will be referred to as explicit
constraints. We know that in the stable distance table, $\mathcal{D}_s^\xi$, there are also implicit
constraints: default constraints and constraints that are implied by $\mathcal{C}$.

**Definition 3.** Let $\xi$ be a scenario of length $n$ and let $\mathcal{D}_s^\xi$ be its stable distance table. Then, for any $0 \le i < j < n$, the interval $I_{ij}^\xi$ is $\{a \in \mathbb{Q} \mid m_{ij}^\xi \le a \le M_{ij}^\xi\}$ where $\mathcal{D}_s^\xi[i, j] = (m_{ij}^\xi, M_{ij}^\xi)$.

Intuitively, $I_{ij}^{\xi}$ corresponds to a pair of constraints: the time distance between events $i$ and $j$ in every behaviour in $[[\xi]]$ must be at least $m_{ij}^{\xi}$ and at most $M_{ij}^{\xi}$.

**Definition 4.** Let $\xi$ and $\eta$ be two consistent scenarios with the same sequence of events. We say $\xi$ is subsumed by $\eta$, denoted by $\xi \subseteq \eta$, when $[[\xi]] \subseteq [[\eta]]$.

**Observation 4.** Let $\xi$ and $\eta$ be two consistent scenarios of length $n$ with the same sequence of events. Then $\xi \subseteq \eta$ iff $\forall_{0 \le i < j < n} I_{ij}^{\xi} \subseteq I_{ij}^{\eta}$.

Thanks to Observation 4, it can be easily checked, in quadratic time, whether a
scenario is subsumed by another one.

**Definition 5.** Let $\xi$ and $\eta$ be two consistent scenarios of length $n$ with the same sequence of events, $\mathcal{E}$, such that $\forall 0 \le i < j < n$ $I_{ij}^{\xi} \cap I_{ij}^{\eta} \neq \emptyset$. The intersection of $\xi$ and $\eta$, denoted by $\xi \cap \eta$, is a scenario whose sequence of events is $\mathcal{E}$ and whose constraints are given by $\mathcal{D}^{\xi \cap \eta}$, where $\mathcal{D}^{\xi \cap \eta}[i, j] = (\max(m_{ij}^{\xi}, m_{ij}^{\eta}), \min(M_{ij}^{\xi}, M_{ij}^{\eta}))$.

If $\exists_{0 \le k < l < n} I_{kl}^{\xi} \cap I_{kl}^{\eta} = \emptyset$, then $\xi \cap \eta$ is not defined.

Assume $\mathcal{D}_s^\xi[i, j] = (a_1, b_1)$, $\mathcal{D}_s^\eta[i, j] = (a_2, b_2)$, and $\xi \cap \eta$ is defined. Then $\mathcal{D}^{\xi \cap \eta}[i, j] = (I_{ij}^{\xi \cap \eta}, h_{ij}^{\xi \cap \eta}) = (\max(a_1, a_2), \min(b_1, b_2))$. Since $I_{ij}^{\xi} \cap I_{ij}^{\eta} \neq \emptyset$, we have $\max(a_1, a_2) \le \min(b_1, b_2)$. So the initial table is always valid. But it might not be stable, so we must stabilise it to check whether $\xi \cap \eta$ is consistent. In the resulting stable table $I_{ij}^{\xi \cap \eta} \le m_{ij}^{\xi \cap \eta} \le M_{ij}^{\xi \cap \eta} \le h_{ij}^{\xi}$ for every $0 \le i < j < n$, because stabilisation only tightens the constraints.

Figures 5 and 6 show two scenarios, $\xi$ and $\eta$, along with their stable distance tables. Observe that $I_{ij}^{\xi} \cap I_{ij}^{\eta} \neq \emptyset$, for $0 \le i < j \le 2$. Figure 7 shows the initial table corresponding to their intersection and its stabilized form.

**Lemma 1.** Let $\xi$ and $\eta$ be two consistent scenarios such that $[[\xi]] \cap [[\eta]] \neq \emptyset$. Then the scenario $\xi \cap \eta$ is defined and consistent. Moreover, $[[\xi]] \cap [[\eta]] \subseteq [[\xi \cap \eta]]$.

*Proof.* Let $\mathcal{B} \in [[\xi]] \cap [[\eta]]$. Then

$\forall 0 \le i < j < n \ t_{ij}^{\mathcal{B}} \le M_{ij}^{\xi} \wedge t_{ij}^{\mathcal{B}} \le M_{ij}^{\eta}$. So $t_{ij}^{\mathcal{B}} \le \min(M_{ij}^{\xi}, M_{ij}^{\eta})$.

$\forall 0 \le i < j < n \ t_{ij}^{\mathcal{B}} \ge m_{ij}^{\xi} \wedge t_{ij}^{\mathcal{B}} \ge m_{ij}^{\eta}$. So $t_{ij}^{\mathcal{B}} \ge \max(m_{ij}^{\xi}, m_{ij}^{\eta})$.

Therefore $\forall 0 \le i < j < n \ \max(m_{ij}^{\xi}, m_{ij}^{\eta}) \le \min(M_{ij}^{\xi}, M_{ij}^{\eta})$. So $\xi \cap \eta$ is defined.

Behaviour $\mathcal{B}$ satisfies all the constraints represented by the initial table of $\xi \cap \eta$, i.e., $\mathcal{D}^{\xi \cap \eta}$ (see Definition 5). Stabilization does not remove any behaviour, so $\mathcal{B}$ satisfies also all the constraints represented by $\mathcal{D}_s^{\xi \cap \eta}$. That is, $\mathcal{B} \in [[\xi \cap \eta]]$. Therefore $[[\xi \cap \eta]] \neq \emptyset$, and hence $\xi \cap \eta$ is consistent. Moreover, $[[\xi]] \cap [[\eta]] \subseteq [[\xi \cap \eta]]$. $\square$
$$ \begin{array}{l} 0 : a ; \\ 1 : b \{ \tau_{0,1} \le 2 \} ; \\ 2 : c \{ \tau_{0,2} \ge 5 \} . \end{array} $$

$$ \begin{array}{c|cc} 1 & 2 & \\ \hline 0 & (0, 2) & (5, \infty) \\ 1 & & (3, \infty) \end{array} $$

$$ \begin{array}{l} 0 : a ; \\ 1 : b ; \\ 2 : c \{ \tau_{1,2} = < 3 \} . \end{array} $$

$$ \begin{array}{c|cc} 1 & 2 & \\ \hline 0 & (0, \infty) & (0, \infty) \\ 1 & & (0, 3) \end{array} $$

<caption>Fig. 5. $\xi$ and its stable distance table</caption>

<caption>Fig. 6. $\eta$ and its stable distance table</caption>

$$ \begin{array}{c|cc} 1 & 2 & \\ \hline 0 & (0, 2) & (5, \infty) \\ 1 & & (3, 3) \end{array} $$

$$ \begin{array}{c|cc} 1 & 2 & \\ \hline 0 & (2, 2) & (5, 5) \\ 1 & & (3, 3) \end{array} $$

$$ \begin{array}{l} 0 : a ; \\ 1 : b \{ \tau_{0,1} = 2 \} ; \\ 2 : c \{ \tau_{1,2} = 3 \} . \end{array} $$

<caption>Fig. 7. The initial table and its stabilized form for $\xi \cap \eta$</caption>

<caption>Fig. 8. $\xi \cap \eta$</caption>

**Theorem 1.** Let $\xi$ and $\eta$ be two consistent scenarios such that $\xi \cap \eta$ is defined and consistent. Then $[\xi \cap \eta] = [[\xi]] \cap [[\eta]]$.

*Proof.* Assume the length of $\xi$ and $\eta$ is $n$, and let $\mathcal{B} \in [[\xi \cap \eta]]$. Then

$\forall 0 \le i < j < n: t_{ij}^{\mathcal{B}} \ge m_{ij}^{\xi \cap \eta} \ge l_{ij}^{\xi \cap \eta} = \max(m_{ij}^{\xi}, m_{ij}^{\eta})$. So $t_{ij}^{\mathcal{B}} \ge m_{ij}^{\xi}$ and $t_{ij}^{\mathcal{B}} \ge m_{ij}^{\eta}$.

$\forall 0 \le i < j < n: t_{ij}^{\mathcal{B}} \le M_{ij}^{\xi \cap \eta} \le h_{ij}^{\xi \cap \eta} = \min(M_{ij}^{\xi}, M_{ij}^{\eta})$. So $t_{ij}^{\mathcal{B}} \le M_{ij}^{\xi}$ and $t_{ij}^{\mathcal{B}} \le M_{ij}^{\eta}$.

Therefore $\mathcal{B} \in [[\xi]]$ and $\mathcal{B} \in [[\eta]]$, that is, $\mathcal{B} \in [[\xi]] \cap [[\eta]]$. So $[\xi \cap \eta] \subseteq [[\xi]] \cap [[\eta]]$.

Since $[\xi \cap \eta] \ne \emptyset$, it follows that $[[\xi]] \cap [[\eta]] \ne \emptyset$ and, by Lemma 1, $[[\xi]] \cap [[\eta]] \subseteq [[\xi \cap \eta]]$. So $[[\xi \cap \eta]] = [[\xi]] \cap [[\eta]]$. $\square$

Consider $\xi$ and $\eta$ of Figs. 5 and 6 once more. A simple analysis shows that in the set of behaviours that are allowed by both $\xi$ and $\eta$ the time distance between $a$ and $b$, and between $b$ and $c$ must be exactly 2 and 3, respectively. Indeed, this is captured by scenario $\xi \cap \eta$, shown in Fig. 8, which is obtained from the stabilized table of Fig. 7.

**Definition 6.** Let $\xi$ and $\eta$ be two consistent scenarios of length $n$ with the same sequence of events, $\mathcal{E}$, such that $\forall 0 \le i < j < n: I_{ij}^{\xi} \cap I_{ij}^{\eta} \ne \emptyset$. The combination of $\xi$ and $\eta$, denoted by $\xi \uplus \eta$, is a scenario whose sequence of events is $\mathcal{E}$ and whose constraints are given by $\mathcal{D}^{\xi \uplus \eta}$, where $\mathcal{D}^{\xi \uplus \eta}[i, j] = (\min(m_{ij}^{\xi}, m_{ij}^{\eta}), \max(M_{ij}^{\xi}, M_{ij}^{\eta}))$.

If $\exists 0 \le i < j < n: I_{ij}^{\xi} \cap I_{ij}^{\eta} = \emptyset$, then $I_{ij}^{\xi} \cup I_{ij}^{\eta}$ does not constitute a single interval. In that case $\xi$ and $\eta$ cannot be combined, and so $\xi \uplus \eta$ is not defined.

Let $\mathcal{D}_s^{\xi}[i, j] = (a_1, b_1)$, $\mathcal{D}_s^{\eta}[i, j] = (a_2, b_2)$, and assume $\xi \uplus \eta$ is defined. Then $\mathcal{D}^{\xi \uplus \eta}[i, j] = (l_{ij}^{\xi \uplus \eta}, h_{ij}^{\xi \uplus \eta}) = (\min(a_1, a_2), \max(b_1, b_2))$. Clearly, $\mathcal{D}^{\xi \uplus \eta}$ is stable, since all the inequations in 1 are satisfied by its contents:

**Observation 5.** If $\xi \uplus \eta$ is defined, then $\mathcal{D}^{\xi \uplus \eta} = \mathcal{D}_s^{\xi \uplus \eta}$. So $\xi \uplus \eta$ is consistent.

**Lemma 2.** Let $\xi$ and $\eta$ be two consistent scenarios such that $\xi \uplus \eta$ is defined. Then $[\xi] \cup [[\eta]] \subseteq [[\xi \uplus \eta]]$.

*Proof.* $\xi$ is consistent, so $[[\xi]] \ne \emptyset$. Let $\mathcal{B} \in [[\xi]]$. Then

$\forall 0 \le i < j < n: t_{ij}^{\mathcal{B}} \ge m_{ij}^{\xi} \ge \min(m_{ij}^{\xi}, m_{ij}^{\eta}) = l_{ij}^{\xi \uplus \eta}$, and
<figure><img src="image_5.png" /><figcaption>Fig. 9. Two scenarios, $\xi$ and $\eta$, and their stable tables</figcaption></figure>

<figure><img src="image_6.png" /><figcaption>Fig. 10. The combination of $\xi$ and $\eta$ of Fig. 9, and scenario $\zeta$ with its stabilized table</figcaption></figure>

$$ \forall 0 \le i < j < n \quad t_{ij}^{\mathcal{B}} \le M_{ij}^{\xi} \le \max(M_{ij}^{\xi}, M_{ij}^{\eta}) = h_{ij}^{\xi \mathcal{W} \eta}. $$

Then $t_{ij}^{\mathcal{B}} \in I_{ij}^{\xi \mathcal{W} \eta}$. Therefore $\mathcal{B}$ satisfies all the constraints represented by $\mathcal{D}^{\xi \mathcal{W} \eta}$, which is stable by Observation 5. So $\mathcal{B} \in [[\xi \mathcal{W} \eta]]$. Therefore $[[\xi]] \cup [[\eta]] \subseteq [[\xi \mathcal{W} \eta]]$. A similar argument can be made if $\mathcal{B} \in [[\eta]]$. $\square$

Table $\mathcal{D}_s^{\xi \mathcal{W} \eta}$ allows all the behaviours in $[[\xi]] \cup [[\eta]]$. But there is a possibility that it may also allow some extra behaviours, namely those that satisfy all the constraints of the combination, but do not satisfy some of the constraints in $\xi$ and some of the constraints in $\eta$.

**Observation 6.** Let $\xi$ and $\eta$ be two consistent scenarios such that $\xi \mathcal{W} \eta$ is defined. Then $[[\xi \mathcal{W} \eta]] = [[\xi]] \cup [[\eta]] \cup \mathcal{Z}(\xi, \eta)$, where $[[\xi]] \cap \mathcal{Z}(\xi, \eta) = \emptyset$ and $[[\eta]] \cap \mathcal{Z}(\xi, \eta) = \emptyset$.

Observation 6 effectively defines $\mathcal{Z}(\xi, \eta)$. We call members of $\mathcal{Z}(\xi, \eta)$ zigzagging behaviours. Our goal is to characterize the conditions under which $\mathcal{Z}(\xi, \eta) = \emptyset$.

It is not too difficult to find such zigzagging behaviours, if they exist. We discuss this for the case of combining two scenarios $\xi$ and $\eta$ into a scenario $\gamma$.

We identify a value $\alpha \in I_{ij}^{\xi}$ such that $\alpha \notin I_{ij}^{\eta}$, and a value $\beta \in I_{kl}^{\eta}$ ($i \neq k$ or $j \neq l$) such that $\beta \notin I_{kl}^{\xi}$. We then construct a scenario $\zeta$ with the same sequence of events as $\xi$ and $\eta$, and the constraints $\{\tau_{i,j} = \alpha, \tau_{k,l} = \beta\}$. If $\zeta$ is consistent, we compute its intersection with $\gamma$. If the intersection is not empty, then $\gamma$ is too permissive, since none of the behaviours allowed by $\zeta$ is allowed by $\xi$ or $\eta$.

As an example consider two scenarios, $\xi$ and $\eta$, of Fig. 9 along with their stable tables. Scenario $\gamma$ of Fig. 10 shows the combined scenario along with its stable table. Scenario $\zeta$ of Fig. 10 represents a set of behaviours in which the time distance between events a and b is exactly 5, and between events a and c is exactly 6 units of time. There is no behaviour in the semantics of $\zeta$ that is allowed by either $\xi$ or $\eta$ of Fig. 9. Yet its intersection with $\gamma$ (the combination of $\xi$ and $\eta$) is not empty. This indicates that the union of the sets of behaviours allowed by $\xi$ and $\eta$ cannot be represented by a single scenario.
<figure><img src="image_7.png" /><figcaption>**Fig. 11.** Two scenarios that can be combined</figcaption></figure>

As another example consider $\xi$ and $\eta$ of Fig. 11 where the union of behaviours allowed by $\xi$ and $\eta$ can be represented by a single scenario, namely their combination (see the scenario on the right). That is, no zigzagging behaviour is allowed by $\xi \uplus \eta$: every behaviour in $[[\xi \uplus \eta]]$ is in $[[\xi]]$ or in $[[\eta]]$ or in both.

The union of two scenarios $\xi$ and $\eta$ can be expressed by a single scenario, namely their combination, if there are no zigzagging behaviours possible between $\xi$ and $\eta$, i.e., $\mathcal{Z}(\xi, \eta) = \emptyset$.

**Theorem 2.** Let $\xi$ and $\eta$ be two consistent scenarios of length $n$ with the same sequence of events, $\mathcal{E}$, such that $\xi \uplus \eta$ is defined. Behaviour $\mathcal{B}^z$ with the sequence of events $\mathcal{E}$ belongs to $\mathcal{Z}(\xi, \eta)$ iff

1. For every $0 \le i < j < n$, $t_{ij}^{\mathcal{B}^z} \in I_{ij}^{\xi \uplus \eta}$,

2. There exist $0 \le i < j < n$ and $0 \le k < l < n$ such that

(a) $i \ne k$ or $j \ne l$, and

(b) $t_{ij}^{\mathcal{B}^z} \notin I_{ij}^{\xi}$, $t_{ij}^{\mathcal{B}^z} \in I_{ij}^{\eta}$, and

(c) $t_{kl}^{\mathcal{B}^z} \in I_{kl}^{\xi}$, $t_{kl}^{\mathcal{B}^z} \notin I_{kl}^{\eta}$.

*Proof.* Let $\mathcal{B}^z \in \mathcal{Z}(\xi, \eta)$. Then, by Observation 6, $\mathcal{B}^z \in [[\xi \uplus \eta]]$. Therefore, for every $0 \le i < j < n$, $t_{ij}^{\mathcal{B}^z} \in I_{ij}^{\xi \uplus \eta}$.

$\mathcal{B}^z \in \mathcal{Z}(\xi, \eta)$, so, by Observation 6, $\mathcal{B}^z \notin [[\xi]]$. Therefore there must be some constraint in $\xi$ that is not satisfied by $\mathcal{B}^z$. So there exist some $0 \le i < j < n$ such that $t_{ij}^{\mathcal{B}^z} \notin I_{ij}^{\xi}$. Therefore $t_{ij}^{\mathcal{B}^z} \in I_{ij}^{\eta}$.

$\mathcal{B}^z \notin [[\eta]]$, so by a similar argument it can be shown that there exist some $0 \le k < l < n$ such that $t_{kl}^{\mathcal{B}^z} \notin I_{kl}^{\eta}$ and $t_{kl}^{\mathcal{B}^z} \in I_{kl}^{\xi}$.

If $i = k$ and $j = l$, then $t_{ij}^{\mathcal{B}^z} \notin I_{ij}^{\xi}$ and $t_{kl}^{\mathcal{B}^z} \in I_{kl}^{\xi}$, which is a contradiction.

For the other direction, let $\mathcal{B}^z$ be a behaviour that satisfies conditions 1 and 2. Then $\mathcal{B}^z \in [[\xi \uplus \eta]]$, but $\mathcal{B}^z \notin [[\xi]]$ and $\mathcal{B}^z \notin [[\xi]]$. So, by Observation 6, $\mathcal{B}^z \in \mathcal{Z}(\xi, \eta)$. $\square$

In the rest of the paper when we write $ij \ne kl$, we mean $i \ne k \lor j \ne l$.

**Observation 7.** Let $\xi$ and $\eta$ be two consistent scenarios. $\xi \subseteq \eta$ iff $\xi \uplus \eta = \eta$.

**Definition 7.** A scenario $\xi = (\mathcal{E}, \mathcal{C})$ is trivial if $\mathcal{C} = \emptyset$. $\xi$ is non-trivial if it is not trivial.
Intuitively, all the constraints of a trivial scenario are default constraints. For instance, scenario $\gamma$ of Fig. 10 is trivial.

**Observation 8.** Let $\xi$ and $\eta$ be two consistent scenarios with the same sequence of events. If $\xi$ is trivial, then $\xi \cap \eta = \eta$ and $\xi \uplus \eta = \xi$.

**Lemma 3.** Let $\xi$ and $\eta$ be two consistent scenarios. If $\mathcal{Z}(\xi, \eta) \neq \emptyset$, then neither $\xi$ nor $\eta$ is trivial.

*Proof.* Assume $\xi$ is trivial. Then, by Observation 8, $\xi \uplus \eta = \xi$.

Let $B^z \in \mathcal{Z}(\xi, \eta)$. By Observation 6, $B^z \notin [[\xi]]$. So $B^z \notin [[\xi \uplus \eta]]$. But this is contradictory to Observation 6.

By a similar argument it can be shown that $\eta$ is not trivial.

□

The consequence of Lemma 3 is that if $\mathcal{Z}(\xi, \eta)$ is not empty, then $\xi$ and $\eta$ must each have at least one explicit constraint.

**Lemma 4.** Let $\xi$ and $\eta$ be two consistent scenarios. If $\mathcal{Z}(\xi, \eta) \neq \emptyset$, then $\xi \not\subseteq \eta$ and $\eta \not\subseteq \xi$.

*Proof.* Assume $\xi \subseteq \eta$ or $\eta \subseteq \xi$.

Let $B^z$ be a behaviour in $\mathcal{Z}(\xi, \eta)$. By Observation 6, $B^z \notin [[\xi]]$, and $B^z \notin [[\eta]]$.

If $\eta \subseteq \xi$, then by Observation 7, $\xi \uplus \eta = \xi$. So $B^z \notin [[\xi \uplus \eta]]$: a contradiction.

If $\xi \subseteq \eta$, then we can show a contradiction by a similar argument.

□

We will now examine ways of determining whether $\mathcal{Z}(\xi, \eta) \neq \emptyset$. This will be important for Observation 10 at the end of this section.

**Lemma 5.** Let $\xi = (\mathcal{E}, C_1)$ and $\eta = (\mathcal{E}, C_2)$ be two optimized (see Sec. 2) scenarios. If $\mathcal{Z}(\xi, \eta) \neq \emptyset$, then there must be $c_1 \in C_1$ and $c_2 \in C_2$, such that $c_1 \notin C_2$ and $c_2 \notin C_1$.

*Proof.* By Lemma 3, $\xi$ and $\eta$ are not trivial. That is, $C_1 \neq \emptyset$ and $C_2 \neq \emptyset$. Assume that every constraint in $C_1$ is also in $C_2$, or every constraint in $C_2$ is also in $C_1$. Then $\eta \subseteq \xi$ or $\xi \subseteq \eta$. Then, by Lemma 4, $\mathcal{Z}(\xi, \eta) = \emptyset$. But this is a contradiction.

□

**Lemma 6.** Let $\xi = (\mathcal{E}, C_1)$ and $\eta = (\mathcal{E}, C_2)$ be two optimized scenarios of length $n$, such that $\xi \uplus \eta$ is defined and $\mathcal{Z}(\xi, \eta) \neq \emptyset$.

If $\forall c_1=\tau_{i,j} \sim a \in C_1 \forall c_2=\tau_{k,l} \sim b \in C_2 (c_1 \in C_2 \lor c_2 \in C_1 \lor (i = k \land j = l))$, then there exists $0 \le u < v < n$ such that every constraint in $C_1 \setminus C_2$ and every constraint in $C_2 \setminus C_1$ is between $u$ and $v$ (i.e., it is of the form $\tau_{u,v} \sim d$).

*Proof.* By Lemma 5, $C_1 \setminus C_2 \neq \emptyset$ and $C_2 \setminus C_1 \neq \emptyset$. Let $c_1$ be a constraint for some $\tau_{p,q}$ ($0 \le p < q < n$) in $C_1 \setminus C_2$. Then, by the assumption, every constraint in $C_2$ is between events $p$ and $q$, or is also in $C_1$. So every constraint in $C_2 \setminus C_1$ must be between $p$ and $q$. Similarly, every constraint in $C_1$ is in $C_2$ or between events $p$ and $q$. So all the other constraints in $C_1 \setminus C_2$ (if any) must also be between events $p$ and $q$.

□
Intuitively, if two optimized scenarios $\xi = (\mathcal{E}, C_1)$ and $\eta = (\mathcal{E}, C_2)$ are such that $\mathcal{Z}(\xi, \eta) \neq \emptyset$, and $C_1$ and $C_2$ differ only on constraints between a pair of events, say $u$ and $v$, then both $C_1$ and $C_2$ must contain explicit constraints between $u$ and $v$: if the constraint of, say, $\xi$ were implicit, then that would imply $\eta \subseteq \xi$.

**Theorem 3.** Let $\xi = (\mathcal{E}, C_1)$ and $\eta = (\mathcal{E}, C_2)$ be two optimized scenarios of length $n$ such that $\xi \uplus \eta$ is defined. If $\mathcal{Z}(\xi, \eta) \neq \emptyset$, then there exist a constraint $\alpha \in C_1$ of the form $\tau_{i,j} \sim a$ ($0 \le i < j < n, a \in \mathbb{Q}$), and a constraint $\beta \in C_2$ of the form $\tau_{k,l} \sim b$ ($0 \le k < l < n, ij \neq kl, b \in \mathbb{Q}$), such that $\alpha \notin C_2$ and $\beta \notin C_1$.

*Proof.* Assume the negation of the conclusion, that is,
$\forall_{c_1=\tau_{i,j}} \sim a \in C_1 \forall_{c_2=\tau_{k,l}} \sim b \in C_2 (c_1 \in C_2 \lor c_2 \in C_1 \lor (i=k \land j=l))$.

By Lemma 6, the explicit constraints of $\xi$ and $\eta$ must be identical, except for those that are between a single pair of event numbers, say $p$ and $q$.

In that case, for every $0 \le i < j < n$, the intervals $I_{ij}^{\xi}$ and $I_{ij}^{\eta}$ both correspond to explicit constraints or both correspond to implicit constraints in $\xi$ and $\eta$.

$\mathcal{Z}(\xi, \eta) \neq \emptyset$, so there exists some behaviour $\mathcal{B}^z$ in $\mathcal{Z}(\xi, \eta)$. By Theorem 2, there must exist $0 \le u < v < n$ and $0 \le w < z < n$, where $uv \neq wz$, such that $t_{uv}^{\mathcal{B}^z} \notin I_{uv}^{\xi}$, $t_{uv}^{\mathcal{B}^z} \in I_{uv}^{\eta}$, and $t_{wz}^{\mathcal{B}^z} \in I_{wz}^{\xi}$, $t_{wz}^{\mathcal{B}^z} \notin I_{wz}^{\eta}$. So $I_{uv}^{\xi} \neq I_{uv}^{\eta}$ and $I_{wz}^{\xi} \neq I_{wz}^{\eta}$.

At least one of the intervals between $u$ and $v$ and between $w$ and $z$ must correspond to implicit constraints in both $\xi$ and $\eta$. This is because there is only one pair of event numbers, $p$ and $q$, that correspond to different explicit constraints in $\xi$ and $\eta$. We consider three cases:

1. Both $I_{uv}^{\xi}$ and $I_{wz}^{\eta}$ correspond to implicit constraints in $\xi$ and $\eta$.

Assume $I_{uv}^{\xi}$ corresponds to some constraint $d$ in $\xi$. Because $t_{uv}^{\mathcal{B}^z} \notin I_{uv}^{\xi}$, $d$ is not satisfied by $\mathcal{B}^z$. But then, by Observation 3, at least one explicit constraint $\alpha \in C_1$ that is in the support of $d$ must also not be satisfied by $\mathcal{B}^z$.

Similarly, assume $I_{wz}^{\xi}$ corresponds to some implicit constraint $e$ in $\eta$. Because $t_{wz}^{\mathcal{B}^z} \notin I_{wz}^{\eta}$, constraint $e$ is not satisfied by behaviour $\mathcal{B}^z$. By Observation 3 at least one explicit constraint $\beta \in C_2$ ($\beta \neq \alpha$) that is in the support of $e$ must also not be satisfied by $\mathcal{B}^z$. But in that case, there are two possibilities:

(a) $\alpha$ is of the form $\tau_{p,q} \sim a$ and $\beta$ is of the form $\tau_{p,q} \sim b$.

Neither $\alpha$ nor $\beta$ are satisfied by $\mathcal{B}^z$, so $t_{pq}^{\mathcal{B}^z} \notin I_{pq}^{\xi}$, and $t_{pq}^{\mathcal{B}^z} \notin I_{pq}^{\eta}$. But then, $t_{pq}^{\mathcal{B}^z} \notin I_{pq}^{\xi \uplus \eta}$, which is in contradiction to pt. 1. of Theorem 2.

(b) Only one of $\alpha$ or $\beta$ corresponds to $\tau_{p,q}$.

Let $\alpha$ be of the form $\tau_{p,q} \sim a$ and $\beta$ be of the form $\tau_{r,s} \sim b$, where $rs \neq pq$. Then $\beta$ must also belong to $C_1$. Therefore, $\beta$ in $C_1$ is also not satisfied by $\mathcal{B}^z$. So, $t_{rs}^{\mathcal{B}^z} \notin I_{rs}^{\xi}$, and $t_{rs}^{\mathcal{B}^z} \notin I_{rs}^{\eta}$. But then, $t_{rs}^{\mathcal{B}^z} \notin I_{rs}^{\xi \uplus \eta}$, which is a contradiction. If $\beta$ is of the form $\tau_{p,q} \sim a$, we can show a contradiction by a similar argument.

2. $I_{uv}^{\xi}$ corresponds to an explicit constraint in both $\xi$ and $\eta$, while $I_{wz}^{\xi}$ corresponds to an implicit constraint in both $\xi$ and $\eta$. Then $uv = pq$.

Let $I_{pq}^{\xi}$ and $I_{pq}^{\eta}$ correspond to explicit constraints $d$ and $d'$ in $\xi$ and $\eta$, respectively. $t_{uv}^{\mathcal{B}^z} \notin I_{uv}^{\xi}$ and $uv = pq$, so $t_{pq}^{\mathcal{B}^z} \notin I_{pq}^{\xi}$. Therefore, constraint $d$ is not satisfied by $\mathcal{B}^z$. But because $t_{uv}^{\mathcal{B}^z} \in I_{uv}^{\eta}$ and $uv = pq$, $t_{pq}^{\mathcal{B}^z} \in I_{pq}^{\eta}$, and therefore constraint $d'$ is satisfied by $\mathcal{B}^z$.
<figure><img src="image_8.png" /><figcaption>Fig. 12. Two scenarios, $\xi$ and $\eta$, and their stable tables</figcaption></figure>

Let $I_{wz}^{\xi}$ and $I_{wz}^{\eta}$ correspond to implicit constraints $e$ and $e'$ in $\xi$ and $\eta$ respectively. Since $t_{wz}^{B^z} \in I_{wz}^{\xi}$, constraint $e$ is satisfied by $B^z$, but $e'$ is not satisfied by $B^z$, because $t_{wz}^{B^z} \notin I_{wz}^{\eta}$. So $e'$ is not a default constraint, and $e \neq e'$.

By Observation 3 at least one explicit constraint $\beta \in C_2$ that is in the support of $e'$ must also not be satisfied by $B^z$. $\beta$ cannot be equal to $d'$, because $d'$ is satisfied by $B^z$.

Then $\beta$ must also belong to $C_1$. Therefore, $\beta$ in $C_1$ is also not satisfied by $B^z$.

Let $\beta$ correspond to some constraint between $r$ and $s$. Then, $t_{rs}^{B^z} \notin I_{rs}^{\xi}$, and $t_{rs}^{B^z} \notin I_{rs}^{\eta}$. But then, $t_{rs}^{B^z} \notin I_{rs}^{\xi \cup \eta}$, which is a contradiction.

3. $I_{uv}^{\xi}$ corresponds to an implicit constraint in both $\xi$ and $\eta$, while $I_{wz}^{\xi}$ corresponds to an explicit constraint in both $\xi$ and $\eta$. The argument is very similar to the one above. $\square$

Theorem 3 provides a sufficient condition for the non-existence of zigzagging behaviours: if $\xi = (\mathcal{E}, C_1)$ and $\eta = (\mathcal{E}, C_2)$ do not contain such an $\alpha$ and $\beta$, then $\mathcal{Z}(\xi, \eta) = \emptyset$. But the condition is not necessary, in general: if $\xi$ and $\eta$ contain such an $\alpha$ and $\beta$, there might still be no $\zeta$ in $\mathcal{Z}(\xi, \eta)$. As an example consider scenarios $\xi$ and $\eta$ of Fig. 12: $\xi$ has an explicit constraint between events 0 and 2 (which is not in $\eta$), and $\eta$ has an explicit constraint between events 0 and 1 (which is not in $\xi$), however, there is no behaviour in $\mathcal{Z}(\xi, \eta)$. If we take, say, $t_{12} = 11$ from $I_{12}^{\xi} \setminus I_{12}^{\eta}$ and $t_{02} = 6$ from $I_{02}^{\eta} \setminus I_{02}^{\xi}$, then $t_{02} < t_{12}$, which is impossible. Any other attempt at creating a zigzagging behaviour would fail for similar reasons.

To find out whether $\mathcal{Z}(\xi, \eta)$ is empty, we perform the following steps:

1. Let $\alpha = \tau_{i,j} \sim a \in C_1 \setminus C_2$, and $\beta = \tau_{k,l} \sim b \in C_2 \setminus C_1$ ($ij \neq kl$).

2. We construct scenarios (at most four$^7$) that constrain $t_{ij}$ to be in $I_{ij}^{\xi} \setminus I_{ij}^{\eta}$ and $t_{kl}$ to be in $I_{kl}^{\eta} \setminus I_{kl}^{\xi}$.

3. Let $\zeta$ be one of these scenarios.

4. We stabilize $\zeta$'s initial table, i.e., $\mathcal{D}^{\zeta}$. If the resulting table is valid, and $\zeta \cap (\xi \uplus \eta)$ is defined and consistent, then there exists at least one zigzagging behaviour in $[[\zeta]]$: $\mathcal{Z}(\xi, \eta) \neq \emptyset$.

<footnote n="7">⁷ $I_{ij}^{\xi}$ might be a subset of $I_{ij}^{\eta}$, and vice versa. Similarly, $I_{kl}^{\xi}$ might be a subset of $I_{kl}^{\eta}$, and vice versa.</footnote>
If no zigzagging behaviour can be found for any such pair of constraints $\alpha$ and $\beta$, then $\mathcal{Z}(\xi, \eta) = \emptyset$.

As an example consider scenarios $\xi$ and $\eta$ of Fig. 9 along with their stable distance tables once more. Observe that $\xi$ and $\eta$ are optimized. By comparing the corresponding intervals of the distance tables, it is easy to see that $\xi$ and $\eta$ are not subsets of each other. Moreover, $\xi \uplus \eta$ (shown on the left of Fig. 10) is defined (and therefore consistent).

As we mentioned before the union of the behaviours in $[[\xi]]$ and $[[\eta]]$ cannot be captured by their combination: $\mathcal{Z}(\xi, \eta) \neq \emptyset$. Scenario $\zeta$, shown on the right of Fig. 10, is constructed following the steps above. Obviously, $\zeta$ is consistent: it allows all behaviours in which the time distance between $a$ and $b$ is at least 5, and between $a$ and $c$ is at most 6. Clearly, these behaviours are in $\xi \uplus \eta$, but are neither in $[[\xi]]$, nor in $[[\eta]]$. So in accordance with Theorem 3 there must be a pair of explicit constraints, one in $\xi$ but not in $\eta$, and another one in $\eta$, but not in $\xi$, that are not between the same events. Indeed, the only explicit constraint of $\xi$ (which is not in $\eta$) is between events 0 and 1, while $\eta$'s only explicit constraint (which is not in $\xi$) is between events 0 and 2.

As another example consider the scenarios of Fig. 11 once more. The explicit constraints of $\xi$ and $\eta$ differ only on the constraints between one pair of events, namely, events 0 and 2, so by Theorem 3, $\mathcal{Z}(\xi, \eta) = \emptyset$.

**Observation 9.** If $\mathcal{Z}(\xi, \eta) = \emptyset$, then every behaviour in $[[\xi \uplus \eta]]$ must satisfy all the constraints in $\xi$, or all the constraints in $\eta$, or all the constraints in both $\xi$ and $\eta$.

**Observation 10.** Let $\xi$ and $\eta$ be two consistent scenarios with the same sequence of events, such that $\xi \uplus \eta$ is defined. Then $[[\xi \uplus \eta]] = [[\xi]] \cup [[\eta]]$ iff $\mathcal{Z}(\xi, \eta) = \emptyset$.

Intuitively, the union of two scenarios $\xi$ and $\eta$ exists only when $\mathcal{Z}(\xi, \eta) = \emptyset$. In that case, their combination, i.e., $\xi \uplus \eta$ (Definition 6) becomes their union.

# 5 Conclusions and Related Work

We introduce subsumption, intersection and union operations for timed scenarios. We formally define these operations and their semantics.

Given two consistent scenarios $\xi$ and $\eta$, $\xi$ is subsumed by $\eta$, i.e., $\xi \subseteq \eta$, iff $[[\xi]] \subseteq [[\eta]]$, that is, the set of behaviours allowed by $\xi$ is a subset of that for $\eta$. We provide a constructive way of verifying whether that is the case (Definition 4 and Observation 4).

Next, we show that for two consistent scenarios $\xi$ and $\eta$, if the set of behaviours allowed by both $\xi$ and $\eta$ is not empty, then the set can be captured by a single scenario, namely the intersection of $\xi$ and $\eta$, i.e., $\xi \cap \eta$. Definition 5 shows how to construct $\xi \cap \eta$ and Theorem 1 describes its semantic properties.

Then we turn our attention to the union of scenarios. Given two consistent scenarios $\xi$ and $\eta$, we want to know whether there exists a single scenario that
would express the set of behaviours that are allowed by $\xi$ or $\eta$, i.e., the union of the behaviours allowed by $\xi$ and $\eta$. We constructively define $\xi \Join \eta$ (Definition 6) and show that it captures the expected properties of union only under certain conditions: in particular, when it does not contain “zigzagging” behaviours (Observation 10). Intuitively, zigzagging behaviours belong neither to $[[\xi]]$, nor to $[[\eta]]$, even though they belong to $[[\xi \Join \eta]]$. We formalize zigzagging behaviours, and show that such behaviours are possible *only* when there is a certain relationship between the constraints of $\xi$ and $\eta$ (Theorem 3). This provides us with a syntactic criterion for determining whether $\xi \Join \eta$ does indeed have the required semantic properties of union.

To the best of our knowledge this is the first attempt at developing such operations for timed scenarios. These operations are directly relevant to the problem of synthesizing timed automata with minimal number of clocks from a set of scenarios (see Sec. 3 for a brief discussion), which we will address in a forthcoming paper.

A detailed comparison of timed scenarios with other related work, in particular with Difference Bounds Matrices (DBMs), can be found in our earlier work [10, 14].

Inclusion and intersection operations have been defined for DBMs [20]. However, our subsumption and intersection operations, developed from first principles for timed scenarios, are naturally different.

Union of DBMs has been handled by convex hulls, leading to an approximation algorithm [21] and a safe abstraction [22]: the union of two zones (represented by DBMs) is generally a non-convex set, and therefore cannot be represented by a zone, i.e., a DBM.

Another method for checking whether the union of two DBMs is itself a DBM has been developed using convex hulls together with Clock Difference Diagrams (CDDs) [23].

Our union operation, with well-defined semantics, is defined in a different and straightforward way using the stable distance tables. An interesting property of our union is that no approximation is required, thanks to our syntactic criterion used for the existence of union.

## References

1. Salah, A., Mizouni, R., Dssouli, R., Parreaux, B.: Formal composition of distributed scenarios. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 213–228. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30232-2_14

2. Greenyer, J.: Scenario-based modeling and programming of distributed systems. In: M. Köhler-Bussmeier, E. Kindler, H. Rölke (Eds.), Proceedings of the International Workshop on Petri Nets and Software Engineering 2021 co-located with the 42nd International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS 2021), Paris, France, June 25th, 2021 (due to COVID-19: virtual conference), Vol. 2907 of CEUR Workshop Proceedings, CEUR-WS.org, pp. 241–252 (2021)
3. Somé, S., Dssouli, R., Vaucher, J.: From scenarios to timed automata: building specifications from users requirements. In: Proceedings of the Second Asia Pacific Software Engineering Conference, APSEC 1995, IEEE Computer Society, pp. 48–57 (1995)

4. Chandrasekaran, P., Mukund, M.: Matching scenarios with timing constraints. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 98–112. Springer, Heidelberg (2006). https://doi.org/10.1007/11867340_8

5. Harel, D., Kugler, H., Pnueli, A.: Synthesis revisited: generating statechart models from scenario-based requirements. In: Kreowski, H.-J., Montanari, U., Orejas, F., Rozenberg, G., Taentzer, G. (eds.) Formal Methods in Software and Systems Modeling. LNCS, vol. 3393, pp. 309–324. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31847-7_18

6. Uchitel, S., Kramer, J., Magee, J.: Synthesis of Behavioral Models from Scenarios. IEEE Trans. Softw. Eng. 29(2), 99–115 (2003)

7. Akshay, S., Mukund, M., Kumar, K.N.: Checking coverage for infinite collections of timed scenarios. In: CONCUR 2007 - Concurrency Theory, 18th International Conference, CONCUR 2007, Proceedings, pp. 181–196 (2007)

8. Bollig, B., Katoen, J., Kern, C., Leucker, M.: Replaying play in and play out: synthesis of design models from scenarios by learning. In: Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, 2007, pp. 435–450 (2007)

9. Alur, R., Martin, M., Raghothaman, M., Stergiou, C., Tripakis, S., Udupa, A.: Synthesizing finite-state protocols from scenarios and requirements. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 75–91. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-13338-6_7

10. Saeedloei, N., Kluźniak, F.: From scenarios to timed automata. In: Formal Methods: Foundations and Applications - 20th Brazilian Symposium, SBMF 2017, Proceedings, pp. 33–51 (2017)

11. Saeedloei, N., Kluźniak, F.: Timed scenarios: consistency, equivalence and optimization. In: Formal Methods: Foundations and Applications - 21st Brazilian Symposium, SBMF 2018, Proceedings, pp. 215–233 (2018)

12. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)

13. Alur, R., Madhusudan, P.: Decision problems for timed automata: a survey. In: Formal Methods for the Design of Real-Time Systems, International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM-RT, Revised Lectures, pp. 1–24 (2004)

14. Saeedloei, N., Kluźniak, F.: Optimization of timed scenarios. In: Carvalho, G., Stolz, V. (eds.) SBMF 2020. LNCS, vol. 12475, pp. 119–136. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-63882-5_8

15. Saeedloei, N., Kluźniak, F.: Minimization of the number of clocks for timed scenarios. In: Campos, S., Minea, M. (eds.) SBMF 2021. LNCS, vol. 13130, pp. 122–139. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-92137-8_8

16. Abdulla, P.A., Deneux, J., Ouaknine, J., Worrell, J.: Decidability and complexity results for timed automata via channel machines. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1089–1101. Springer, Heidelberg (2005). https://doi.org/10.1007/11523468_88

17. Baier, C., Bertrand, N., Bouyer, P., Brihaye, T.: When are timed automata determinizable? In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 43–54. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02930-1_4
18. Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52148-8_17

19. Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of real-time systems: compact data structure and state-space reduction. In: 18th IEEE Real-Time Systems Symposium, pp. 14–24 (1997)

20. Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27755-2_3

21. Balarin, F.: Approximate reachability analysis of timed automata. In: 17th IEEE Real-Time Systems Symposium, pp. 52–61 (1996). https://doi.org/10.1109/REAL.1996.563700

22. Daws, C., Tripakis, S.: Model checking of real-time reachability properties using abstractions. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 313–329. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0054180

23. Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Efficient Timed Reachability Analysis Using Clock Difference Diagrams. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 341–353. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48683-6_30