Model-Checking Real-Time Systems: Revisiting the Alternating Automaton Route

Model-Checking Real-Time Systems. The task of verifying if a model A (typically a network of automata) satisfies a specification \(\varphi \) (a formula in a logic) can be cast as the emptiness of an automaton \(A \times B_{\lnot \varphi }\), where \(B_{\lnot \varphi }\) is an automaton recognizing the set of behaviours that violate the specification – in other words, an automaton corresponding to \(\lnot \varphi \). This is the well-known model-checking paradigm. In the context of real-time systems, timed automata [4] are the de-facto choice for the automaton model. For the logic part, metric temporal logic (MTL) is a natural extension of the widely used linear temporal logic (LTL), incorporating timing constraints in the modalities. However, timed logics cannot be easily converted to timed automata, since they are not closed under complementation.

A popular choice for logic-to-automata translations for timed logics, is the model of 1-clock Alternating Timed Automata (1-ATAs) [29, 33]. 1-ATAs are closed under complementation, and are incomparable in expressive power to (multi-clock) timed automata. The power of alternation enables resetting fresh copies of the single clock at different positions along the word. Therefore, while reading a timed word, a 1-ATA can keep track of the time elapsed from multiple positions in the word. This feature is quite convenient to handle future operators like \(\operatorname {U}_I\), an Until operator with an interval constraint I. Therefore, the model-checking problem reduces to checking the emptiness of \(A \times B_{\lnot \varphi }\) where A is a timed automaton and \(B_{\lnot \varphi }\) is a 1-ATA. This is a rather natural formulation of the model-checking problem in the real-time setting. Surprisingly, there is no tool that implements an algorithm to this problem, to the best of our knowledge. Decidability of this question follows from [31] and [29]. However it is based on extended regions and not suitable for practical implementations.

On the other hand, emptiness for timed automata has been extensively studied over the last three decades, and there are mature and well developed tools like UPPAAL [28], PAT [35], LTSMin [25], TChecker [22], Theta [36]. Algorithms for timed automata are based on zones. These are convenient data structures that symbolically capture reachable configurations of a timed automaton. Our goal is to adapt the best known methods from timed automata literature to solve the emptiness of \(A \times B_{\lnot \varphi }\). The crucial missing piece in this picture is a zone-based algorithm to handle 1-ATAs, like \(B_{\lnot \varphi }\). This is the subject of this paper.

The Challenge. Undoubtedly, the biggest challenge in developing a zone-based procedure for 1-ATA is the unbounded size of the configurations that it generates (illustrated in Fig. 4). A 1-ATA maintains several copies of its clock, each of them storing the time since a specific position. This not only adds technical difficulty in describing zone graphs, but it also makes some of the operations used in the computation algorithmically hard. In this work, we pinpoint the challenges and provide some efficient algorithmic solutions for some restricted cases of 1-ATA which arise from fragments of MTL.

Contributions. As a first contribution, we introduce a new deactivation operation for the clock, on transitions. When a clock is deactivated, the branch of the 1-ATA that passes through the transition maintains only the control state, and not the clock value (until the clock gets reactivated again through a reset). This explicit deactivation helps reducing the number of active clock copies maintained by the 1-ATA. To substantiate this idea, we improve the MTL-to-1-ATA construction of [33] using the deactivation operator and identify a fragment that induces 1-ATAs with bounded width – these are automata which contain a bounded number of active clock copies in any reachable configuration.

Next, we present a definition of a zone graph for the enhanced 1-ATAs with the deactivation operation, and provide an algorithm to compute the zone successors. For termination of the zone graph computation, we adapt the entailment relation between zones, studied in [1], to our setting. Our main technical contribution is a close study of this entailment check.

Related Work. Recall the casting of the model-checking question as an emptiness of \(A \times B_{\lnot \varphi }\) where \(B_{\lnot \varphi }\) is a 1-ATA. Since timed automata tools are mature, some of the existing techniques convert \(B_{\lnot \varphi }\) into a timed automaton. MightyL [14] is a tool that converts Metric Interval Temporal Logic (MITL) into a network of timed automata, by observing special properties of the 1-ATA obtained from MITL [13]. Recently, a conversion of MITL into a network of generalized timed automata [2] has been developed [3]. Both these works deal with the MITL fragment. To the best of our knowledge, the only available logic-to-automaton procedure for the full MTL fragment is the MTL-to-1-ATA conversion of [33]. Hence, our work would be the first attempt at an implementable algorithm for the full MTL model-checking (over finite timed words).

The core zone based algorithm for timed automata reachability was proposed in [15]. Termination of the zone enumeration has been an intricate topic since then [7, 9, 21, 23]. We refer the reader to the surveys [10, 34] for a more detailed exposition on this topic. An important ingredient in the zone enumeration is a simulation operation between zones (similar in spirit to the entailment check as said above). For extended models of timed automata – like timed automata with diagonal constraints [9] and event-clock automata [6], there is a translation to classical timed automata. Therefore emptiness for these extended automata can be reduced to emptiness of a bigger timed automaton. However, previous works have observed that zone-based algorithms which work directly on the extended automata perform better than the zone-based algorithms that run on equivalent bigger timed automata: [21] shows it for timed automata with diagonal constraints; [2] introduces generalized timed automata which can model event-clock automata and provides a comparison of the direct method versus the conversion to timed automata. The main reason is that the conversion to timed automata adds many control states which cannot be handled well by the current zone-based algorithms. Algorithms which work directly on the extended automata encode the extra information using zones and manage the explosion using zone simulation techniques. For timed automata with diagonal constraints, the simulation check is \(\textsf{NP}\)-hard. Nevertheless an algorithm using basic zone operations has been proposed [21] and has been shown to work well on examples. This history of successful zone-based methods on extensions of timed automata encourages us to look for direct zone based methods for 1-ATAs as well.

Alternating Timed Automata appeared in [29, 33]. With two clocks, emptiness is undecidable, simply because universality for 2-clock timed automata is undecidable [4]. Emptiness for 1-ATA is known to be decidable with a non-primitive recursive complexity – one reason why 1-ATAs have been ignored for direct manipulations. However, several timed logics have been compiled into 1-ATA [13, 26] and multiple restrictions of 1-ATAs with better complexity, like very weak 1-ATA [14], 1-ATA with reset-free loops [26] have been independently considered in the literature.

In the untimed setting, emptiness of Alternating Finite Automata (AFA) can be performed by a de-alternation that computes an equivalent NFA on-the-fly. To deal with large state-spaces, techniques based on antichains have been extensively explored in the literature [17, 18, 38]. Essentially, the algorithms maintain an antichain of the state space, induced by various simulation preorders. Several heuristics based on preprocessing of the automaton [37] and making use of SAT solvers [24] have been investigated. A comparative study of various AFA emptiness algorithms can be found in [19].

In the timed setting, the closest to our work is [1], which presents a zone-based approach for answering universality of 1-clock timed automata. Our zone construction for 1-ATA builds on this approach. The entailment check between zones that we use has been proposed in [1]. However, there is no algorithm given for the entailment check. An approximation of the check is encoded as an SMT formula. In this work, we make a comprehensive study of this entailment check in terms of algorithms and complexity.

Organization. Section 2 defines the syntax and semantics of 1-ATA with the deactivation operation, and defines 1-ATAs with bounded width. Section 3 presents an improvement of the MTL-to-1-ATA construction and identifies a fragment of MTL which generates bounded width 1-ATAs through the new construction. Section 4 provides a comprehensive description of zone graphs for ATAs. Finally, in Section 5 we delve into an in-depth study of the entailment relation that is essential for termination of the zone graph computation.

All missing proofs can be found in the extended version of the paper [12].

In what follows, we use \(\mathbb {N},\mathbb {Z}\), and \(\mathbb {R}_{\ge 0}\) to represent the set of natural numbers, integers and non-negative real numbers respectively. For \(d \in \mathbb {R}_{\ge 0}\), we use \(\lfloor d \rfloor \) to denote the integral part and \(\operatorname {fract}(d)\) to denote the fractional part of d. We will refer to the single clock of the alternating timed automaton as x. We define intervals as \(I := [a,b] \mid [a,b) \mid (a,b] \mid (a,b) \mid [a, \infty ) \mid (a, \infty ) \) where \(a,b \in \mathbb {N}\). We write \(\mathcal {I}\) for the set of all such intervals. For a finite set S, we define \(\varPhi (S)\) as the set of formulas generated by the following grammar, where \(s \in S\) and \(I \in \mathcal {I}\):Here, I denotes the clock interval guard, \(x.\varphi \) corresponds to resetting the clock (followed by applying \(\varphi )\), and \(\overline{x}.\varphi \) corresponds to making the clock inactive and then applying \(\varphi \).

A timed word over a finite alphabet \(\varSigma \) is a finite sequence of the form \((d_{1},a_{1}) \dots (d_{n},a_{n})\), where \(a_{1},\dots ,a_{n} \in \varSigma \) are events and \(d_{1},\dots ,d_{n} \in \mathbb {R}_{\ge 0}\) are time delays. For example, \(d_2\) is the time between \(a_1\) and \(a_2\), \(d_3\) is between \(a_2\) and \(a_3\), and so on. Alternating timed automata were introduced independently in [32, 33] and [29, 30]. In this paper, we consider the model as defined in [32, 33], with the added deactivation operator.

Before we explain the formal semantics, we give two 1-ATA examples and an informal explanation of their mechanics. Fig. 1 shows 1-ATA \(\mathcal {A}_1\) with \(\varSigma = \{a\}\). It accepts all timed words such that no two as are at distance 1 apart. The initial location is \(q_0\). On reading the first a, \(\mathcal {A}_1\) opens two branches, one that comes back to \(q_0\) and the other that resets clock x and goes to \(q_1\). Similarly, for each of the next as that are read, the \(q_0\) branch spawns into two. The purpose of the \(q_1\) branch is to check if there is an a at distance 1 from the a that created the branch. If yes, the branch goes to a non-accepting state \(q_2\). Fig. 2 illustrates 1-ATA \(\mathcal {A}_2\) with \(\varSigma = \{a, b, c\}\) that accepts timed words satisfying the property: for every a in the word, there is a c at a later position (with no timing constraints), and a b at a later position which is at 1 time unit away from a. Intuitively, at location \(q_a\), whenever an a is read, two obligations are generated in the form of locations \(q_c\) and \(q_b\). Since the only timing constraints are on \(q_b\), we deactivate the clock while going to \(q_c\). This is reflected by \(\bar{x}. q_c\) in the transition \(\delta (q_a, a)\). Location \(q_c\) waits for a c, and on seeing a c, the obligation is discharged (using \(\delta (q_c, c) = {{\textbf {true}}}\), the obligation \(q_c\) “disappears”). Location \(q_b\) waits for a b at time 1 from the a where the obligation appeared. The only accepting location is \(q_a\). Therefore a configuration containing \(q_b\) or \(q_c\) will denote unfulfilled obligations, and hence will be non-accepting. We now present the formal semantics.

We fix a 1-ATA \(\text{\AA }= (Q, \varSigma , q_0, F, \delta )\) for the rest of this section. We define the set of valuations, or values of the clock x, as \(\operatorname {Val}= \mathbb {R}_{\ge 0}\cup \{\bot \}\), where \(\bot \) means the clock is inactive. A state of \(\mathcal {A}\) is a pair (q, v), where \(q \in Q\) and \(v \in \operatorname {Val}\). The state (q, v) is said to be active if \(v \in \mathbb {R}_{\ge 0}\) and inactive if \(v = \bot \). We say \(\textit{val}((q,v))=v\). We call \((q_{0},0)\) the initial state. We define \(S = Q \times \operatorname {Val}\) as the set of all states of \(\mathcal {A}\). Since transitions in a 1-ATA are formulas, potentially with conjunctions, each state (q, v) could result in a set of states after a transition. For example, if there is a transition \(t:= q_0 \wedge x. q_2\) from q, then (q, v) on t results in \(\{(q_0, v), (q_2, 0)\}\). To formalize the idea, we first recursively define when a formula \(\varphi \in \varPhi (Q)\) is satisfied by a set of states \(M \subseteq S\) on a value v, or \(M \models _{v} \varphi \):If \(M \models _v \varphi \), we call M to be a model of \(\varphi \) on v. If \(M \models _{v} \varphi \) and for all \(M' \subsetneq M\), \(M' \not \models _{v} \varphi \), then M is called a minimal model of \(\varphi \) on v.

For e.g., let \(\varphi = q_{0} \wedge x.q_{1}\), \(M_{1} = \{(q_{0},1),(q_{1},0),(q_{2},1)\}\), \(M_{2} = \{(q_{0},1),(q_{1},0)\}\), and \(v=1\) both \(M_{1},M_{2} \models _{v}\varphi \), and \(M_{2}\) is a minimal model on v for \(\varphi \). Let \(\varphi = [1, 2] \wedge x. q_1\), and \(v = 0.2\). Since \(v \notin [1,2]\), there is no model for \(\varphi \) on v. Let \(\varphi = x.([0,1] \wedge q_1)\) and \(v = 2.5\). Then \(\{(q_1, 0)\}\) is a minimal model for \(\varphi \) on v.

A configuration \(\gamma \) of \(\mathcal {A}\) is a finite set of states \(\{(q_{1},v_{1}),\dots ,(q_{n},v_{n})\} \subseteq S\). We call \(\gamma _{0} = \{(q_{0},0)\}\) the initial configuration. We say that a configuration \(\gamma \) is accepting if for every \((q,v)\in \gamma \), we have \(q \in F\). The point is that each state with a non-accepting location is an obligation that is required to be discharged. Therefore, an accepting configuration is one containing no obligations. Observe that by definition of an accepting configuration, the empty configuration \(\{ \}\) consisting of no states is accepting. We define the location signature of a configuration \(\gamma = \{(q_{1},v_{1}),\dots ,(q_{n},v_{n})\}\) as the multiset \(\operatorname {loc-sign}(\gamma ) = \{q_{1},\dots ,q_{n}\}\).

Next we look at definition of the transitions. We define two kinds of transitions from \(\gamma \):

Timed transitions. for \(d \in \mathbb {R}_{\ge 0}\), we define \(\gamma + d = \{(q, v + d) \mid (q, v) \in \gamma ,\,v \in \mathbb {R}_{\ge 0}\} \cup \{(q,\bot )\mid (q,\bot ) \in \gamma \}\). We add an edge \(\gamma \xrightarrow {d} \gamma + d\) for all \(d \in \mathbb {R}_{\ge 0}\).

Discrete transitions. let \(\gamma = \{(q_{1},v_{1}),\dots ,(q_{n},v_{n})\}\) and let \(a \in \varSigma \); recall that \(\delta (q_i, a)\) is a formula in disjunctive normal form for all \(1 \le i \le n\); for each combination \(C=(C_{1},\dots ,C_{n})\) such that \(C_{i}\) is one disjunct of \(\delta (q_{i},a)\), we add an edge \(\gamma \xrightarrow {a,C} \gamma '\) if \(\gamma ' = \bigcup _{i=1}^{n} M_{i}\) where each \(M_{i}\) is a minimal model of \(C_{i}\) on \(v_{i}\), for all \(1 \le i \le n\).

For example, consider the 1-ATA \(\mathcal {A}_1\) of Fig. 1. Let \(\gamma = \{ (q_0, 0.4), (q_1, 0.2) \}\). We have \(\delta (q_0, a)\) to be a single clause and \(\delta (q_1, a)\) to be a disjunction of three clauses. So, there are three possible combinations, out of which only \(([0, 1) \wedge q_1)\) has an extension: \(\gamma \xrightarrow {a, (q_0 \wedge x.q_1, ~[0,1) \wedge q_1)} \gamma '\) with \(\gamma '= \{(q_0, 0.4), (q_1, 0), (q_1, 0.2)\}\).

We use \(\gamma \xrightarrow {d,a,C} \gamma '\) as shorthand to mean there is some \(\gamma ''\) such that \(\gamma \xrightarrow {d} \gamma '' \xrightarrow {a,C} \gamma '\). We define a run from \(\gamma \) as a sequence of transitions:The run is accepting if \(\gamma _{n}\) is accepting. A timed word \((d_1, a_1) \dots (d_n, a_n)\) is accepted by \(\mathcal {A}\) if there is an accepting run of the above form from \(\gamma _{0}\). We define the language of \(\mathcal {A}\), or \(L(\mathcal {A})\) to be the set of words accepted by \(\mathcal {A}\).

Given a 1-ATA \(\mathcal {A}\), the emptiness problem asks whether \(L(\mathcal {A})\) is empty or not. To decide the emptiness problem, it is enough to find if there is some accepting run from \(\gamma _{0}\) in the transition system above. This problem has been proven decidable with non-primitive recursive complexity in [29]. The decidability result relies on the construction of extended regions, on which a well-quasi order can be defined. In this paper, following standard techniques for timed automata [10, 15], we design a symbolic zone-based approach to decide the emptiness problem for 1-ATA. Before we delve into it, we consider a special restriction of 1-ATAs.

1-ATA with Bounded Width. We define the width of a configuration \(\gamma \) to be the number of active states present in \(\gamma \). For instance \(\{(q_{0},1.2),(q_{1},0),(q_{1},\bot )\}\) has width 2. From Example 1, we notice that the run can be extended to generate configurations of larger and larger width. Each transition out of \(q_0\) generates two more states, and the existing states with \(q_1\) remain. We say that a 1-ATA \(\mathcal {A}\) has width k if every reachable configuration starting from the initial configuration of \(\mathcal {A}\) has width \(\le k\). It can be checked that \(\mathcal {A}_1, \mathcal {A}_2\) of Fig. 1 and 2 have unbounded width.

In this section, we revisit the MTL-to-1-ATA construction of [32, 33] and propose a modified construction using the deactivation operation. We identify a fragment of MTL which yields bounded width 1-ATAs with the proposed modification. The syntax of MTL is described using the grammar: \(\varphi := a \mid \lnot a \mid \varphi \wedge \varphi \mid \varphi \vee \varphi \mid \operatorname {X}_{I} \varphi \mid \varphi \operatorname {U}_{I} \varphi \), where \(a \in \varSigma \) and I is an interval. Given a timed word \(w = (d_{1},a_{1}),\dots ,(d_{n},a_{n})\), a position \(1 \le i \le n\) and an MTL formula \(\varphi \), we define \((w,i) \models \varphi \) as follows:

We say a timed word w satisfies formula \(\varphi \), denoted as \(w \models \varphi \), if \((w, 1) \models \varphi \). Observe that the time stamp of the first letter is not relevant for the satisfaction of the formula, and therefore the semantics is translation invariant. We define \(L(\varphi )\) as the set of timed words that satisfy \(\varphi \).

MTL to 1-ATA Construction of [33]. Given a formula \(\varphi \), [33] gives a method to construct a 1-ATA \(\mathcal {A}_\varphi \) with the same language. Without loss of generality, we assume that \(\varphi \) is in negation normal form: all negations appear only at the atomic level. Locations of \(\mathcal {A}_\varphi \) include all subformulas of \(\varphi \), a location \((X_I \psi )^r\) for every subformula \(X_I \psi \) of \(\varphi \) and and a special location \(\varphi _{init}\). The initial location is \(\varphi _{init}\). The transition relation \(\delta \) is designed so that the following invariant is satisfied [33]: on a word \(w = (d_1, a_1) \dots (d_n, a_n)\) the presence of state \((\psi , 0)\) in the configuration occuring after reading \(a_j\), ensures that \((w, j) \models \psi \). With this in mind, the transition relation \(\delta \) is given as follows, for each \(a \in \varSigma \):Proposed Modification. The idea is that if \(\psi \) is a pure LTL formula, then in the state \((\psi , 0)\) generated to check \(\psi \), the value of x is unnecessary. Hence, we deactivate the clock whenever we generate an obligation for a pure LTL formula. More precisely, we replace every occurrence of \(x. \psi \) in \(\delta \) above by:

Call the resulting 1-ATA \(\mathcal {A}'_\varphi \). We can then say the following:

Fig. 3 gives an example of the proposed construction for the formula \((\textbf{F}a) \operatorname {U}_{[1, 2]} c\) where \(\textbf{F}a\), a short form for \({{\textbf {true}}}\operatorname {U}a\), is a pure LTL formula. In the figure, the transition system on the right depicts a run. In the original construction, each b generates a new copy of location \(\textbf{F}a\) with an active clock, and makes the 1-ATA unbounded. On the other hand, with the deactivated clock, the resulting 1-ATA becomes bounded width, in fact, it has width 1 – the only active state checks for an occurrence of c within the interval [1, 2] starting from the initial position. Motivated by this observation, we define a fragment of MTL for which our proposed construction results in 1-ATAs with bounded width. This fragment is inspired by the flat-MTL fragment defined in [11].

The key idea is that in the \(\operatorname {U}_I\) modality, the left branch is an LTL formula. For example, the formula \((\textbf{F}a) \operatorname {U}_{[1,2]} c\), is a one-sided MTL formula. Notice that in the Flat-MTL fragment([11]), the Until formulas either have bounded intervals, or have pure LTL formulas on the left branch. Here, we only allow the latter kind of formulas. Also, this fragment is different from MITL([5]) as we do not forbid singular intervals. Here is the main result of this section:

We will now move on to solving the emptiness problem for 1-ATAs using zone based techniques. Algorithms based on zones are well known in the timed automata literature. We begin this section with two examples that provide an overview of our zone graphs for 1-ATAs.

We now move on to a formal definition of the zone graph and the procedure to compute successors. Fix a 1-ATA \(\text{\AA }= (Q, \varSigma , q_0, F, \delta )\) for the rest of this section. We assume an infinite supply of variable names \(x_{q,0}, x_{q,1}, \dots \) and \(x'_{q,0}, x'_{q,1}, \dots \) for each location q of \(\mathcal {A}\). For variables \(x_{q,i}\) and \(x'_{q,i}\), we define \(\operatorname {loc}(x_{q,i}) = q\), \(\operatorname {loc}(x'_{q,i}) = q\). For a set of variables X, we define its location signature, \(\operatorname {loc-sign}(X)\) to be the multi-set \(\{ \operatorname {loc}(y) \mid y \in X \}\).

Zones and Nodes. A zone is a conjunction of constraints of the form \((y \sim k)\) or \((y - x \sim k)\), where \({\sim } \in \{<,\le ,>,\ge \}\), \(k \in \mathbb {Z}\) and x, y are variables. We write Var(Z) for the set of variables used in Z. We define \(\operatorname {loc-sign}(Z) := \operatorname {loc-sign}(Var(Z))\). To deal with the inactive valuations, we define the nodes of a zone graph to be of the form \((Z,\operatorname {IA})\) where Z is a zone and \(\operatorname {IA}\subseteq \{ x_{q,0} \mid ~\hbox {q} \text { is a location of } \mathcal {A}\}\) is a set of variables that are currently inactive. Notice that we always use variables with index 0 in \(\operatorname {IA}\), and hence there are finitely many choices for the \(\operatorname {IA}\) component of nodes. We say \(Var(Z,\operatorname {IA}) = Var(Z) \cup \operatorname {IA}\) and \(\operatorname {loc-sign}(Z,\operatorname {IA}) = \operatorname {loc-sign}(Z) \cup \operatorname {loc-sign}(\operatorname {IA})\). We will call the pair \((Z,\operatorname {IA})\) a node.

We say that a configuration \(\gamma \) satisfies a node \((Z,\operatorname {IA})\), denoted as \(\gamma \models (Z,\operatorname {IA})\), if there is a surjection \(h:Var(Z,\operatorname {IA}) \mapsto \gamma \) such that (i) \(\operatorname {loc}(y) = \operatorname {loc}(h(y))\) for every \(y \in Var(Z, \operatorname {IA})\), (ii) for every \(x_{q,0} \in \operatorname {IA}\), \(val(h(x_{q,0})) = \bot \) and (iii) replacing every variable \(y \in Var(Z)\) with val(h(y)) satisfies all the zone constraints. We can now define \(\llbracket (Z,\operatorname {IA}) \rrbracket = \{\gamma \mid \gamma \models (Z,\operatorname {IA})\}\). This means we can look at zones as a representation of a set of configurations. For convenience, we will simply use \((Z,\operatorname {IA})\) to refer to both the zone and the set \(\llbracket (Z,\operatorname {IA}) \rrbracket \) of configurations. For instance, we will use \(\gamma \in (Z,\operatorname {IA})\) to mean \(\gamma \in \llbracket (Z,\operatorname {IA}) \rrbracket \). Zones can be represented using Difference-Bound-Matrices (DBMs) [16]. We refer the reader to [8, 10] for an exposition of algorithms for some of the standard operations on zones.

Computing Successors. Given a node \((Z, \operatorname {IA})\) and a letter \(a \in \varSigma \), we need to first pick an outgoing transition for each variable – more precisely, for the location corresponding to the variable. For instance, in Fig. 5, consider the node \(\langle x_{\varphi ,1} \ge 0 \rangle , \{x_{\textbf{F}a,0}\}\). On b, location \(\varphi \) has transition \(\varphi \wedge \bar{x}. (\textbf{F}a)\) and location \(\textbf{F}a\) has a loop back to it. Hence the successor is computed on the tuple \((\varphi \wedge \bar{x}. (\textbf{F}a), \textbf{F}a)\). In Fig. 4, consider node \(\langle x_{q_0, 1} \ge 0 \wedge x_{q_1, 1} = 0 \rangle \). From \(q_0\) there is a unique outgoing transition, whereas from \(q_1\), there are three possible transitions. So the targets out of this node are \((q_0 \wedge x. q_1, (1, \infty ) \wedge q_1)\), \((q_0 \wedge x. q_1, [0, 1) \wedge q_1)\) and \((q_0 \wedge x. q_1, [1,1] \wedge q_2)\). In Fig. 4 we depict the only successor on \((q_0 \wedge x. q_1, [0, 1) \wedge q_1)\).

Assume \((Z, \operatorname {IA})\) is a non-empty node with \(Var(Z) = \{x_{q_1, i_1}, x_{q_2, i_2}, \dots , x_{q_k, i_k} \}\) (indices 1 to k) and \(\operatorname {IA}= \{ x_{q_{k+1}, 0}, \dots , x_{q_m, 0} \}\) (indices \(k+1\) to m). For an \(a \in \varSigma \), we define:Pick \((C_1, \dots , C_m)\). Our goal is to compute the successor node \((Z, \operatorname {IA}) \xrightarrow {a, (C_1, \dots , C_m)} (Z', \operatorname {IA}')\). If some \(C_j = {{\textbf {false}}}\) then according to our definition, there is no model for it, w.r.t. to any valuation.  We discard such targets. Let us assume none of the \(C_j\) is \({{\textbf {false}}}\). We do the following sequence of operations

Time elapse. Compute node \((Z_1, \operatorname {IA}_1)\) where \(\llbracket (Z_1, \operatorname {IA}_1) \rrbracket = \{ \gamma + \delta \mid \delta \ge 0 \}\) and \(\operatorname {IA}_1 = \operatorname {IA}\). The zone \(Z_1\) represents the closure of Z w.r.t. time successors. It can be computed using a standard DBM technique as in [8].

Guard intersection. For every active variable j ranging from 1 to k, and for every interval \(I_j \in C_j\), add the constraints corresponding to \(x_{q_j,i_j} \in I_j\). After adding all the constraints, we tighten the constraints using an operation known as canonicalization in the timed automata literature [8]. For instance if \(x' = x, y' = y\) and \(x = y\), we derive the constraint \(x' = y'\). Let the resulting node be \((Z_2, \operatorname {IA}_2)\) with \(\operatorname {IA}_2 = \operatorname {IA}_1\). We have \(\llbracket (Z_2, \operatorname {IA}_2) \rrbracket := \{ \gamma \in (Z_1, \operatorname {IA}_1) \mid \gamma \text { satisfies~\hbox {all} clock constraints in the transition } \}\).

Reset and move to new variables. Since we have dealt with intervals already, we can now assume that each \(C_j\) is a conjunction of atoms of the form q, x.q and \(\bar{x}.q\), or \(C_j = {{\textbf {true}}}\). If \(C_j = {{\textbf {true}}}\) for all \(1 \le ~\hbox {j} \le m\), the successor of \((Z, \operatorname {IA})\) is a special empty node \((Z_\emptyset , \{\})\) where \(Z_\emptyset \) denotes a zone with \(\llbracket Z_\emptyset \rrbracket = \emptyset \) (see Fig. 5, the successor of \((\langle x_{\varphi , 1} \ge 0 \rangle , \{\} )\) for instance). Otherwise, we will iteratively compute a new set of constraints \(\varPhi \), and a new set of variables \(\operatorname {IA}_3\). Initially, \(\varPhi := {{\textbf {true}}}\), \(\operatorname {IA}_3 = \emptyset \). Pick each variable \(x_{q_j, i_j}\), with j ranging from 1 to m in some order, and consider all the atoms in the conjunction \(C_j\):

Define \(Z_3 = Z_2 \wedge \varPhi \).

Remove old variables. Tighten all the constraints of \(Z_3\) by the canonicalization procedure. After canonicalization, remove all the old unprimed variables, and remove the primes from the newly introduced variables, i.e., \(x'_{q,1}\) becomes \(x_{q,1}\) and so on. This new node is the required \((Z', \operatorname {IA}')\).

Zone Graph of a 1-ATA. The initial node is \((Z_0, I_0)\) where \(Z_0 := (x_{q_0, 1} = 0)\) (with \(q_0\) being the initial state) and \(\operatorname {IA}_0 = \emptyset \). There is a special node \((Z_\emptyset , \{\})\) denoting the empty configuration, with \(\llbracket Z_\emptyset \rrbracket = \emptyset \). Successors are systematically computed by enumerating over all the outgoing targets, and performing the successor computation as explained earlier.  The resulting graph that is computed is called the zone graph of the 1-ATA. A node \((Z, \operatorname {IA})\) is said to be accepting if for every \(x \in Var(Z) \cup \operatorname {IA}\), we have \(\operatorname {loc}(x)\) to be accepting. In particular, the special node \((Z_{\emptyset }, \{\})\) is accepting. We can prove the soundness and completeness of this zone graph – the language of a 1-ATA is non-empty iff there is a path in the zone graph starting from the initial node to an accepting node.

Zone enumeration suffers from two sources of infinity: (1) the width of the zone (number of active states) can increase in an unbounded manner, and (2) the constants appearing in the zone constraints can be unbounded too. For timed automata, the number of clocks (and hence the width of the zones) is fixed. However, the second challenge does manifest and there is a long line of work coming up with better termination mechanisms that tackle the unbounded growth of constants. The termination mechanism is essentially a subsumption relation between zones, which allows to prune the search.

For zone-based universality in 1-clock timed automata, an entailment relation between zones was used as a termination mechanism [1]. We provide an algorithm for this check that makes use of zone operations from the timed automata literature. We then prove that the entailment is \(\textsf{NP}\)-hard. As the entailment check is an important operation in the zone graph, done each time a new zone is added, the \(\textsf{NP}\)-hardness illuminates the difficulty caused due to point (1) above.

Finally, for 1-ATA with bounded width, where (1) is not an issue any more, we provide a slight modification to the test, which makes it polynomial-time checkable, and yet ensures termination.

The entailment check is based on an equivalence between configurations \(\gamma \simeq _M \gamma '\), first proposed in [31]. The equivalence can be adapted to our setting by considering the \(\bot \) states by adding that there is a one-to-one correspondence between inactive states in \(\gamma \) and \(\gamma '\).

For the rest of the document, it is sufficient to observe that \(\simeq _M\) is a time-abstract bisimulation on the configurations. The equivalence \(\simeq _M\) is defined on configurations with the same size. However, as noticed in Fig. 4, the size of the configurations could be unbounded, and we need a way to relate configurations of different sizes. We adapt an entailment relation proposed in [1] to our setting:

The idea is that when \(\gamma \sqsubseteq \gamma '\), if \(\gamma '\) reaches an accepting configuration, then so does \(\gamma \). In other words, if \(\gamma '\) (the bigger configuration) is able to discharge all its obligations, the small configuration \(\gamma \) (with fewer obligations) is also able to discharge its own obligations. The same idea holds in the case of nodes. If \((Z, \operatorname {IA}) \sqsubseteq (Z', \operatorname {IA}')\), then if \((Z', \operatorname {IA}')\) reaches an accepting node, then so does \((Z, \operatorname {IA})\). Therefore, if we reach \((Z', \operatorname {IA}')\) during the zone enumeration, while \((Z, \operatorname {IA})\) has already been visited, we can stop exploring \((Z', \operatorname {IA}')\). Moreover, by definition of \(\simeq _M\), it follows that \((Z, IA) \sqsubseteq (Z', IA')\) iff \(IA \subseteq IA'\) and \(Z \sqsubseteq Z'\) (relation restricted to active states).

We still need to show that this pruning results in a finite zone graph. To do so, we will use the following: a relation \(\prec ~\subseteq A \times A\) for a set A is a well-quasi order (WQO) if for every infinite sequence \(a_{1} a_{2} \dots \) where \(a_{1},a_{2},\dots \in A\), there exists some i and j such that \(a_{i} \prec a_{j}\). It was shown in [1] that the entailment restricted to zones \(Z \sqsubseteq Z'\) is a well-quasi order. Since the \(\operatorname {IA}\) sets are finite, \(IA \subseteq IA'\) is also a well-quasi order. Finite cartesian products of WQOs are WQOs [27]. Now, we can observe since \(\sqsubseteq \) is a WQO on nodes, every sequence of nodes will hit a node which is bigger than an existing node w.r.t \(\sqsubseteq \) and hence the computation will terminate at this node, implying that every path in the zone graph pruned using \(\sqsubseteq \), is finite.

Algorithm for the Entailment Check. To get to an algorithm to check entailment on two zones, we look at the cases when the entailment will not hold, i.e. the conditions when \((Z,\operatorname {IA}) \not \sqsubseteq (Z',\operatorname {IA}')\). We observe that \((Z,\operatorname {IA}) \not \sqsubseteq (Z',\operatorname {IA}')\) if either \(\operatorname {IA}\not \subseteq \operatorname {IA}'\), orAs the first case is easy to check, we assume \(\operatorname {IA}\subseteq \operatorname {IA}'\) and focus on the second case, which means that for this particular \(\gamma ' \in Z'\), for each of its subsets \(\gamma ''\), there is no configuration that is region equivalent to it in Z. We see that for \(\gamma '' \subseteq \gamma '\) such that \(\operatorname {loc-sign}(\gamma '') \ne \operatorname {loc-sign}(Z)\), there will trivially be no region equivalent configuration for \(\gamma ''\) in Z. Thus we look at the subsets \(\gamma ''\) such that \(\operatorname {loc-sign}(\gamma '') = \operatorname {loc-sign}(Z)\) and investigate the entailment check (1).

Consider a one-to-one mapping \(r: Var(Z) \rightarrow Var(Z')\) that preserves locations: that is, for every \(x \in Var(Z)\), we have \(\operatorname {loc}(x) = \operatorname {loc}(r(x))\). Let \(\operatorname {range}(r)\) be the set of variables of \(Var(Z')\) that are in the range of r. Rename variables Var(Z) to \(y_1, y_2, \dots , y_n\), making Z a zone over these fresh variables. Similarly, project \(Z'\) to \(\operatorname {range}(r)\) and rename \(r(y_1), r(y_2), \dots , r(y_n)\) as \(y_1, y_2, \dots , y_n\). Call the resulting zones \(Z_r\) and \(Z'_r\) respectively. These are zones on the same fixed set of variables and are hence amenable to techniques from timed automata literature. A valuation \(v' \in Z'_r\) associates a real to each variable \(y_i\). Define: \(N_r := \{v' \in Z'_r \mid \forall v \in Z_r, v \not \simeq _M v' \}\). Given \(Z_r, Z'_r\), there is a method to check if \(N_r\) is non-empty [23]. Using this algorithm, we can in fact describe \(N_r\) as a finite union of zones. The complexity of this method is quadratic in the number of variables used in \(Z_r\) and \(Z'_r\). Then, we translate \(N_r\) back to \(Z'\): let \(N'_r = \{ \gamma ' \in Z' \mid \gamma ' \text { restricted to } r \text { belongs to }N_r \}\).

The above lemma leads to an algorithm: compute \(N'_r\) for each location preserving mapping in time \(\mathcal {O}(|Var(Z)|^2)\) and check if the intersection is non-empty. Notice that the number of mappings r could be exponential in |Var(Z)| – it is bounded by the number of subsets of size |Var(Z)| in \(Var(Z')\), which is given by \({|Var(Z')|}\atopwithdelims (){|Var(Z)|}\). The overall complexity is \(\mathcal {O}({{|Var(Z')|}\atopwithdelims (){|Var(Z)|}} \cdot |Var(Z)|^2)\). In practice, one can envisage an algorithm that enumerates each location preserving r, and keeps the intersection of \(N'_r\) among all the r enumerated so far. This intersection will be a union of zones. If at some point, the intersection becomes empty, the algorithm can stop. Otherwise, the algorithm continues until all location-preserving maps are considered.

Hardness. Let \(V = \{ p_1, p_2, \dots , p_n\}\) be a set of propositional variables, taking values either \(\top \) (true) or \(\bot \) (false). An assignment fixes a value to each of the variables. A positive literal is an element of \(L_+ = V\) and a negative literal is an element of \(L_- = \{ \bar{p}_1, \bar{p}_2, \dots , \bar{p}_n\}\). When \(p_i = \top \), the literal \(\bar{p}_i = \bot \) and vice-versa.  We denote by \(L := L_+ \cup L_-\), the set of all literals. A 3-clause (hereafter called simply a clause) C is a disjunction of three literals. The clause is said to be monotone if either all its literals are positive, or all its literals are negative: \(C \subseteq L_+\) or \(C \subseteq L_-\). A boolean formula in 3-CNF form is a conjunction of clauses: \(\bigwedge _{i=1}^{i=m} C_i\). A 3-CNF formula is monotone if each of its clauses is monotone. The MONOTONE-3-SAT problem: given a monotone 3-CNF formula, is it satisfiable? This problem is known to be \(\textsf{NP}\)-complete [20].

Let 1-ATA-Zone-Non-Entailment be the decision problem which takes as input two nodes \((Z, \operatorname {IA})\), \((Z', \operatorname {IA}')\), and a constant M, and checks if \((Z, \operatorname {IA}) \not \sqsubseteq (Z', \operatorname {IA}')\), where \(\sqsubseteq \) makes use of the region equivalence w.r.t M.

To prove the theorem, we present a reduction from MONOTONE-3-SAT to 1-ATA-Zone-Non-Entailment. Given a monotone 3-CNF formula \(\varphi \), we construct zones \((Z_\varphi , \operatorname {IA}_\varphi )\), \((Z'_\varphi , \operatorname {IA}'_\varphi )\) together with the constant \(M_\varphi \) such that \(\varphi \) is satisfiable iff \((Z_\varphi , \operatorname {IA}_\varphi ) \not \sqsubseteq (Z'_\varphi , \operatorname {IA}'_\varphi )\). To start off with, we assume \(\operatorname {IA}_\varphi = \operatorname {IA}'_\varphi = \emptyset \). This means \((Z_\varphi ,\operatorname {IA}_\varphi ) \not \sqsubseteq (Z'_\varphi , \operatorname {IA}'_\varphi )\) iff \((Z_{\varphi }, \emptyset ) \not \sqsubseteq (Z'_{\varphi }, \emptyset )\). So for simplicity we will use the notation \(Z_\varphi \not \sqsubseteq Z'_\varphi \) in the rest of this section. We now define the zones constructed for the monotone 3-CNF formula \(\varphi = C_{1} \wedge C_{2} \wedge \dots \wedge C_{n}\), where we assume that \(C_{1},\dots ,C_{k}\) have all positive literals and \(C_{k+1},\dots ,C_{n}\) have all negative literals.

The Idea: We see that \(\varphi \) is satisfied iff there exists some assignment of the variables of \(\varphi \) such that for every clause \(C_{i}\) for \(1 \le i \le n\), \(C_{i}\) is true. Comparing this with the definition of non-entailment: \(Z_{\varphi } \not \sqsubseteq Z'_{\varphi }\) iff there exists \(\gamma ' \in Z'_{\varphi }\) such that for every \(\gamma '' \subseteq \gamma '\) and \(\gamma \in Z_{\varphi }\), we have \(\gamma '' \not \simeq _M \gamma \). In our construction, we will pick a large enough constant \(M_{\varphi }\) so that \(\gamma '' \simeq _M \gamma \) boils down to simply \(\gamma '' = \gamma \). So, we see that we need to construct zones \(Z_{\varphi }\) and \(Z'_{\varphi }\) such that each \(\gamma ' \in Z'_{\varphi }\) corresponds to an assignment, and having no subset \(\gamma '' \subseteq \gamma '\) with \(\gamma '' \in Z_{\varphi }\) corresponds to every clause being true. To encode assignments through our zones, we use two variables, x and y and use the value of their difference, \(y-x\), to decide the assignment of the variable they encode: [0, 1] as false and (1, 2] as true. Due to space constraints, we present an overview of our construction though an example \(\varphi = (p_{1} \vee p_{2} \vee p_{3}) \wedge (\bar{p}_{4} \vee \bar{p}_{1} \vee \bar{p}_{5})\). Fig. 7 illustrates the construction for \(\varphi \).

Zone \(Z'_\varphi \). We want to construct this zone to encode the possible assignments to the variables of \(\varphi \). To do this, we consider variables \(x_j^i, y_j^i\) for \(1 \le j \le 3\) and \(1 \le i \le m\) with constraints \(0 \le y_j^i - x_j^i \le 2\). Each valuation to the x, y variables assigns a value between 0 to 2 for the difference. For it to encode an assignment, the assigned values should be consistent across all occurrences of the same variable: for example, in Fig. 7, variable \(p_1\) occurs in \(C_1\) positively and in \(C_2\) negatively. We add two constraints \(x_2^2 - x_1^1 = 17\) and \(y_2^2 - y_1^1 = 17\). These constraints ensure that \( y_1^1 - x_1^1 = y_2^2 - x_2^2\). Therefore, in all occurrences of the variable, we have the difference \(y - x\) to be the same, and hence we can extract an assignment of the variables of \(\varphi \) from a valuation of the x, y variables in \(Z'_\varphi \). Fig. 7 also shows other variables \(px_j, py_j\) and \(nx_j, ny_j\), which we will explain later, after describing \(Z_\varphi \).

Zone \(Z_{\varphi }\): In the entailment check \(Z_\varphi \sqsubseteq Z'_\varphi \), we pick a \(\gamma ' \in Z_\varphi '\), select a subset \(\gamma '' \subseteq \gamma '\) and check whether \(\gamma '' \notin Z_\varphi \). The subset selection \(\gamma ''\) should correspond to a clause and \(Z_\varphi \) intuitively encodes one clause and checks if all literals are false. Since negative and positive clauses need to be dealt with differently, we instead encode two clauses, one positive (the green part of \(Z_\varphi \) in Fig. 7) and one negative (the red part in the figure). The constraints of \(Z_\varphi \) ensure that all literals are false, hence the two selected clauses are false. The extra constraints [1, 5] ensure that all three literals are picked from the same clause. Moreover, for the mapping to work correctly, we set \(\operatorname {loc}(x_j^i) = q_x\) and \(\operatorname {loc}(x_i^+) = \operatorname {loc}(x_i^-) = q_x\), and \(\operatorname {loc}(y_j^i) = q_y\), \(\operatorname {loc}(y_i^+) = \operatorname {loc}(y_i^-) = q_y\) for all relevant indices.

While evaluating \(Z_\varphi \not \sqsubseteq Z'_\varphi \), we will consider each \(\gamma ' \in Z'_\varphi \), and find projections \(\gamma '' \subseteq \gamma '\) that map to \(Z_\varphi \). By our choice of the variable signatures, each projection will pick a positive clause and a negative clause.

We add 12 extra variables \(px_j, py_j, nx_j, ny_j\) for \(j=1,2,3\) to correspond to a dummy positive and a negative clause. The values of \(py_j - px_j\) and \(ny_j - nx_j\) encode false for the corresponding literals. Therefore, for a \(\gamma '\) that is not a satisfying assignment, we can pick a projection \(\gamma ''\) that chooses a clause that is made false by \(\gamma '\) and a dummy clause of the opposite polarity. This takes care of the second point above. However, due to this addition, there is a projection \(\gamma ''\) consisting of both dummy clauses. One can always choose this pair of dummy clauses to belong to \(Z_\varphi \), even when \(\gamma '\) is a satisfying assignment. To eliminate this, we add a final constraint to \(Z_\varphi \) which bounds the distance between the two extremes (\(y_3^- - x_1^+ < 50\) in Fig. 7) preventing choosing both the dummy clauses. The full details of the construction can be found in [12].

Entailment for Bounded Width 1-ATAs. Suppose we start with a 1-ATA \(\mathcal {A}\) with width k. Then in the zone graph computation as explained in Section 4, every variable name \(x_{q, i}\) will have index \(i \le k\). For each state q, there are at most k variables in the zone (along with potentially an \(x_{q, 0}\) in the inactive part). In such a scenario, we can use a modified entailment check that only compares zones with the same set of variable names.

Let Z and \(Z'\) be two zones such that \(Var(Z) = Var(Z')\). Let \(\iota :Var(Z) \rightarrow Var(Z')\) be the identity mapping. Let \(\simeq _M^\iota \) be the equivalence of Definition 3 with h being the identity function \(\iota \). So, \(\simeq _M^\iota \) is simply the classical region equivalence of [4]. This can be naturally lifted to zones: \((Z, \operatorname {IA}) \sqsubseteq ^b_M (Z', \operatorname {IA}')\) if \(\operatorname {IA}\subseteq \operatorname {IA}'\) and for every \(\gamma ' \in Z'\) there is some \(\gamma \in Z\) such that \(\gamma \simeq ^\iota _M \gamma '\). he check \(\sqsubseteq ^b\) is identical to a simulation test \(\preccurlyeq _M\) used in the timed automata literature [23], but with the direction reversed: \((Z, \operatorname {IA}) \sqsubseteq ^b_M (Z', \operatorname {IA}')\) iff \(\operatorname {IA}\subseteq \operatorname {IA}'\) and \(Z' \preccurlyeq _M Z\). This test can be done with quadratic complexity and is known to be a well-quasi-order on zones with a fixed number of variables.

Notice that \(\sqsubseteq ^b\) implies \(\sqsubseteq \), but not the other way around. Therefore, the zone graph obtained by \(\sqsubseteq ^b\) is correct but it could be an over-approximation, with potentially more nodes. However, the entailment check \(\sqsubseteq ^b\) is efficient. Moreover, since there are at most \(|Q| \times k\) number of variables generated, and since we know that for each \(j \le |Q| \times k\), the relation \(\sqsubseteq ^b\) induces a well-quasi-order, the overall computation using \(\sqsubseteq ^b\) terminates: if not, there is an infinite path in the zone graph with an infinite subsequence of zones over the same set of variables, which is non-increasing w.r.t \(\sqsubseteq ^b_M\). A contradiction.

In timed automata literature, 1-ATAs have played the role of an excellent technical device for logic-to-automata translations. Perhaps, owing to the high general complexity, there have been no attempts at aligning the analysis of 1-ATAs to the well developed timed automata algorithms. Typically, 1-ATAs are converted to equivalent network of timed automata, with a blowup in the control states. Our aim in this paper is to pass on the message that these conversions of 1-ATAs to TAs may not really be needed and instead one could embed the analysis of 1-ATAs into the current timed automata algorithms. To substantiate this claim, we have given a zone-based emptiness algorithm for 1-ATAs. In [12], we show how we can lift it to a model-checking algorithm, by providing a zone graph for the product of a timed automaton with a 1-ATA (the \(A \times B_{\lnot \varphi }\) as described in the introduction). We have also demonstrated a logical fragment which induces bounded width 1-ATAs, for which the operations in the zone enumeration are as good as the counterparts used in timed automata reachability. One important idea that we wish to highlight is the addition of an explicit deactivation operation for 1-ATAs. This is a simple trick that can have a substantial impact on the analysis.

We believe that the theoretical foundations we lay here pave the way for studying further optimizations, implementing the ideas and understanding the practical impact. As part of future work, it would be interesting to study whether the best known simulation techniques for timed automata [10] can be incorporated into the 1-ATA zone graphs. What about ATAs with multiple clocks? They are undecidable, of course. But, are there good restrictions that make the modeling more succinct and still enable a zone-based analysis? It would be interesting to extend the notion of boundedness on multi-clock ATAs and find out if there are fragments of MTL (MITL for instance) that are expressible by it. This study also motivates the question of understanding zone-based liveness algorithms for ATAs, in particular, bounded-width ATAs. Another direction is to explore the extensive literature based on antichain algorithms studied for alternating finite automata emptiness, in the real-time setting. Here is another natural problem that we leave open: given a 1-ATA \(\mathcal {A}\) and a constant k, decide whether \(\mathcal {A}\) has width k?