MightyL: A Compositional Translation from MITL to Timed Automata

The design of critical software that respect real-time specifications is a notoriously difficult problem. In this context, verification of programs against formal specifications is crucial, in order to handle the thin timing behaviours. In the untimed setting, a logic widely used both in academia and industry is Linear Temporal Logic (LTL) [32]. A crucial ingredient of its success is the possibility to translate LTL formulae into (Büchi) automata. In the real-time counterpart, Metric Interval Temporal Logic (MITL) [3] has been introduced twenty years ago where it was established that it can be translated into (Büchi) timed automata (TA). Beyond verification of real-time software, there are numerous interests in MITL from other domains, e.g. automated planning and scheduling [39], control engineering [18] and systems biology [6]. The translation from MITL to TA s is complicated and has led to some simplified constructions, e.g. [17, 28]. However, despite these efforts, the tool support for MITL is still lacking to this day. To the best of our knowledge, the only implementation of an automata-based construction is described in [10, 11], but is not publicly available. Since existing verification tools based on timed automata have been around for quite some time and have been successful (e.g. Uppaal [27] first appeared in 1995), it would be preferable if such translation can be used with these tools.

In the present paper, we attempt to amend the situation by proposing a more practical construction from MITL to (Büchi) timed automata. Compared to [10, 11], our construction has the following advantages:

1. 1.

   While we also use one-clock alternating timed automata (OCATA ) [30] as an intermediate formalism, our construction exploits the ‘very-weakness’ of the structure of OCATA s obtained from MITL formulae to reduce state space. In particular, our construction subsumes LTL2BA [19] in the case of LTL.

2. 2.

   The number of clocks in the resulting TA is reduced by a factor of up to two. This is achieved via a more fine-grained analysis of the possible clock values (see Sect. 5).

3. 3.

   The construction is compositional: for each location of the OCATA \(\mathcal {A}\) obtained from the input MITL formula, we construct a ‘component’ TA and establish a connection between the runs of \(\mathcal {A}\) and the runs of the synchronous product of these components. Thanks to this connection, we can give the output TA in terms of components; this greatly simplifies the implementation, and speeds up its execution.

4. 4.

   The construction is compatible with off-the-shelf model-checkers: our tool MightyL generates output automata in the Uppaal xml format which, besides Uppaal [27] itself, can also be analysed by LTSmin [24] with opaal front-end, TiAMo [9], ITS-tools [35], DiVinE [5], etc.

Related Work. There is already a number of MITL-to-TA constructions in the literature [3, 17, 28]. However, most of them interpret MITL over signals (i.e. the continuous semantics of MITL) and hence generate signal automata. This choice unfortunately hinders the possibility to leverage existing tools based on classical timed automata over timed words [2] and is probably one of the reasons why the aforementioned constructions have never been implemented.^{Footnote 1} We, following [4, 10, 11, 37] (among others), interpret MITL over timed words (i.e. the pointwise semantics of MITL). Note that there have been some implementations that deal with peculiar specification patterns over timed words (e.g. [1]). For MITL, apart from [10, 11] that we mentioned earlier, we are only aware of implementations for rather restricted cases, such as the safety fragment of \(\textsf {MITL} _{0,\infty }\) [12] or MITL over untimed words [39]. Our construction subsumes all of these approaches.

Using alternating automata as an intermediate formalism is a standard approach in LTL model-checking [36]. However, the translation from alternating automata to Büchi automata may incur an exponential blow-up if the output automaton is constructed explicitly [19]. For this reason, an on-the-fly approach is proposed in [21], but it requires a specialised model-checking algorithm. Alternatively, [8] gives a symbolic encoding of alternating automata which can be used directly with NuSMV [13], but minimality of transitions (which may potentially improve the performance of verification algorithms, cf. [21]) is difficult to enforce in this setting (see also [14, 34]). Our construction combines the advantages of these approaches—it can be regarded as a symbolic encoding of OCATA s in TA s, enforcing some minimality criteria on transitions for efficiency (see Sect. 6)—and provides compatibility with existing tools that construct state spaces on-the-fly. By contrast, [17, 28], not based on OCATA s, also give the resulting automaton in terms of smaller component automata, but they have to use specialised product constructions to synchronise the components.

Apart from automata-theoretic approaches, [7] considers ‘bounded model-checking’ which encodes the satisfiability problem for MITL (in the continuous semantics) into an SMT problem (Satisfiability Modulo Theories) [15]. This approach is complete when very large bounds (numbers of regions of equivalent TA) are used, but such bounds are clearly impractical for current SMT solvers.

Outline. Section 2 starts with preliminary definitions of timed logics and (alternating) timed automata. Sections 3, 4 and 5 then give our new translation from formulae to generalised Büchi (timed) automata for LTL, \(\textsf {MITL} _{0,\infty }\) (a fragment of MITL where only intervals of the form [0, a], [0, a), \([a,+\infty )\), or \((a,+\infty )\) are allowed), and full MITL, respectively. We report on our OCaml implementation MightyL and some promising experiments on several benchmarks in Sect. 6.

Timed Languages. Let \(\textsf {AP} \) be a finite set of atomic propositions, and \(\varSigma =2^{\textsf {AP} }\). A timed word over \(\varSigma \) is an infinite sequence \(\rho =(\sigma _1,\tau _1) (\sigma _2,\tau _2)\cdots \) over \(\varSigma \times \mathbb R^+\) with \((\tau _i)_{i\ge 1}\) a non-decreasing sequence of non-negative real numbers. We denote by \(T\varSigma ^\omega \) the set of timed words over \(\varSigma \). A timed language is a subset of \(T\varSigma ^\omega \).

Timed Logics. We consider the satisfiability and model-checking problem of Metric Interval Temporal Logic (MITL), an extension of Linear Temporal Logic (LTL) in which temporal operators can be labelled with non-singular timed intervals (or [0, 0], which is the only singular interval we allow). Formally, MITL formulae over \(\textsf {AP} \) are generated by the grammar

where \(p\in \textsf {AP} \) and I is either a non-singular interval over \(\mathbb {R}^+\) with endpoints in \(\mathbb N\cup \{+\infty \}\) or [0, 0]. To simplify our explanations, we will only consider closed non-singular intervals in the sequel, i.e. intervals of the form [a, b] or \([a,+\infty )\), with \(0\le a<b<+\infty \). We let |I| be the length of the interval I: \(|[a,b]|=b-a\) for \(0\le a<b<+\infty \) and \(|[a,+\infty )|=+\infty \).

We consider the pointwise semantics and interpret MITL formulae over timed words. The semantics of a formula \(\varphi \) in MITL is defined inductively: given \(\rho =(\sigma _1,\tau _1)(\sigma _2,\tau _2)\cdots \in T\varSigma ^\omega \), and a position \(i \ge 1\), we let

• \((\rho , i)\models p\) if \(p\in \sigma _i\);

• \((\rho , i)\models \varphi _1\wedge \varphi _2\) if \((\rho ,i)\models \varphi _1\) and \((\rho ,i)\models \varphi _2\);

• \((\rho ,i)\models \lnot \varphi \) if \((\rho ,i)\not \models \varphi \);

• \((\rho ,i)\models \mathbf {X}_I \varphi \) if \((\rho ,i+1)\models \varphi \) and \(\tau _{i+1}-\tau _i\in I\);

• \((\rho ,i)\models \varphi _1\mathbin {\mathbf {U}}_I \varphi _2\) if there exists \(j\ge i\), \((\rho ,j)\models \varphi _2\), \(\tau _j-\tau _i\in I\), and, for all \(i\le k< j\), \((\rho , k)\models \varphi _1\).

We derive other Boolean operators with the following macros: \(\varphi _1\vee \varphi _2 \equiv \lnot (\lnot \varphi _1\wedge \lnot \varphi _2)\), \(\top \equiv p\vee \lnot p\), \(\bot \equiv \lnot \top \), and \(\varphi _1\Rightarrow \varphi _2 \equiv \lnot \varphi _1\vee \varphi _2\). We also define other temporal operators as usual: the ‘eventually’ operator \(\mathbf {F}_I\varphi \equiv \top \mathbin {\mathbf {U}}_I\varphi \), the ‘globally’ operator \(\mathbf {G}_I\varphi \equiv \lnot \mathbf {F}_I\lnot \varphi \), the ‘release’ operator \(\varphi _1\mathbin {\mathbf {R}}_I \varphi _2 \equiv \lnot ((\lnot \varphi _1)\mathbin {\mathbf {U}}_I(\lnot \varphi _2))\), and the ‘dual-next’ operator \(\overline{\mathbf {X}}_I \varphi \equiv \lnot \mathbf {X}_I \lnot \varphi \) (contrary to LTL, it is not true that \(\lnot \mathbf {X}_I \varphi \equiv \mathbf {X}_I \lnot \varphi \)). With the release and dual-next operators, we can transform every formula \(\varphi \) into negative normal form, i.e. formulae using only predicates of \(\textsf {AP} \), their negations, and the operators \(\vee \), \(\wedge \), \(\mathbin {\mathbf {U}}_I\), \(\mathbin {\mathbf {R}}_I\), \(\mathbf {X}_I\), and \(\overline{\mathbf {X}}_I\). To help the understanding, let us detail the semantics of \(\varphi _1\mathbin {\mathbf {R}}_I\varphi _2\):

• \((\rho ,i)\models \varphi _1\mathbin {\mathbf {R}}_I\varphi _2\) if for all \(j\ge i\) such that \(\tau _j-\tau _i\in I\), either \((\rho ,j)\models \varphi _2\), or there exists \(i\le k<j\) such that \((\rho ,k)\models \varphi _1\).

We say that \(\rho \) satisfies the formula \(\varphi \), written \(\rho \models \varphi \) if \((\rho ,1)\models \varphi \), and we denote by \(\llbracket \varphi \rrbracket \) the set of all timed words satisfying \(\varphi \). When writing formulae, we omit the trivial interval \([0, +\infty )\). LTL is the fragment of MITL where all operators are labelled by \([0,\infty )\); and \(\textsf {MITL} _{0,\infty }\) is the fragment where, in all intervals, either the left endpoint is 0 or the right endpoint is \(+\infty \).

Timed Automata. Let X be a finite set of real valued variables, called clocks. The set \(\mathcal G(X)\) of clock constraints g over X is defined by \(g:= \top \mid g\wedge g \mid x\bowtie c\), where \({\bowtie }\in \{{\le },{<},{\ge },{>}\}\), \(x\in X\) and \(c\in \mathbb N\). A valuation over X is a mapping \(v :X \rightarrow \mathbb R^+\). We denote by \(\mathbf {0}\) the valuation that maps every clock to 0, and we write the valuation simply as a value in \(\mathbb R^+\) when X is a singleton. The satisfaction of a constraint g by a valuation v is defined in the usual way and noted \(v \models g\), and we denote by \(\llbracket g\rrbracket \) the set of valuations v satisfying g. For \(t\in \mathbb R^+\), we let \(v +t\) be the valuation defined by \((v +t)(x) = v (x)+t\) for all \(x\in X\). For \(R\subseteq X\), we let \(v [R\leftarrow 0]\) be the valuation defined by \((v [R\leftarrow 0])(x) = 0\) if \(x\in R\), and \((v [R\leftarrow 0])(x) = v (x)\) otherwise.

We introduce the notion of generalised Büchi timed automaton (GBTA) as an extension of classical timed automata [2] with a generalised acceptance condition (used by [20] in the untimed setting). A GBTA is a tuple \(\mathcal A= (L,\varSigma ,\ell _0,\varDelta ,\mathcal F)\) where L is a finite set of locations, \(\varSigma \) is a finite alphabet, \(\ell _0\in L\) is the initial location, \(\varDelta \subseteq L\times \varSigma \times \mathcal G(X) \times 2^X\times L\) is the transition relation, and \(\mathcal F=\{F_1,\dots ,F_n\}\), with \(F_i\subseteq L\) for all \(1\le i \le n\), is the set of sets of final locations. A timed automaton (TA), as described in [2], is a special case of GBTA where \(\mathcal F=\{F\}\) is a singleton (F contains the accepting locations of the TA). A state of \(\mathcal A\) is a pair \((\ell ,v )\) of a location \(\ell \in L\) and a valuation v of the clocks in X. A run of \(\mathcal A\) over the timed word \((\sigma _1,\tau _1)(\sigma _2,\tau _2)\cdots \in T\varSigma ^\omega \) is a sequence of states \(C_0,C_1,\dots \) where (i) \(C_0=(\ell _0, \mathbf {0})\) and (ii) for each \(i\ge 0\) such that \(C_i=(\ell ,v)\), there is a transition \((\ell ,\sigma _{i+1},g,R,\ell ')\) such that \(C_{i+1} = (\ell ',v')\), \(v +(\tau _{i+1}-\tau _i)\models g\) (assuming \(\tau _0=0\)) and \(v'=(v +(\tau _{i+1}-\tau _i))[R\leftarrow 0]\). By the generalised Büchi acceptance condition, a run is accepting if and only if the set of locations that it visits infinitely often contains at least one location from each set \(F_i\), for all \(1\le i\le n\). We let \(\llbracket \mathcal A\rrbracket \) be the set of timed words on which there exist accepting runs of \(\mathcal A\).

Synchronisation of Timed Automata. In the following, we will consider GBTA s described by synchronous products of several components. More precisely, given two GBTA s \(\mathcal A^1 = (L^1,\varSigma ,\ell _0^1,\varDelta ^1,\mathcal F^1)\) and \(\mathcal A^2 = (L^2,\varSigma ,\ell _0^2,\varDelta ^2,\mathcal F^2)\) over disjoint sets of clocks, we define the GBTA \(\mathcal A^1\times \mathcal A^2= (L,\varSigma ,\ell _0,\varDelta ,\mathcal F)\) obtained by synchronising \(\mathcal A^1\) and \(\mathcal A^2\). Its set of locations is \(L=L^1\times L^2\), with \(\ell _0=(\ell _0^1,\ell _0^2)\). The acceptance condition is obtained by mimicking a disjoint union of the generalised Büchi conditions: assuming \(\mathcal F^1=\{F_1,\dots ,F_n\}\) and \(\mathcal F^2=\{G_1,\dots ,G_m\}\), we let \(\mathcal F= \{F_1\times L^2,\dots ,F_n\times L^2, L^1\times G_1,\dots ,L^1\times G_{m}\}\). Finally, \(((\ell ^1_1,\ell ^2_1),\sigma ,g,R,(\ell ^1_2,\ell ^2_2))\in \varDelta \) if there exists \((\ell ^1_1,\sigma ,g^1,R^1,\ell ^1_2)\in \varDelta ^1\) and \((\ell ^2_1,\sigma ,g^2,R^2,\ell ^2_2)\in \varDelta ^2\) such that \(g=g^1\wedge g^2\) and \(R=R^1\cup R^2\). This definition can be extended for the synchronisation of a set of GBTA s \(\{\mathcal A^i\mid i\in I\}\): the product is then written as \(\prod _{i\in I} \mathcal A^i\).

One-Clock Alternating Timed Automata. One-clock alternating timed automata (OCATA) [30] extend (non-deterministic) one-clock timed automata by adding conjunctive transitions. Intuitively, a conjunctive transition spawns several copies of the automaton that run in parallel from the targets of the transition. A word is accepted if and only if all copies accept it. An example is shown in Fig. 1, where the conjunctive transition is the hyperedge starting from \(\ell _0\).

Formally, we consider a single clock x and, for a set L of locations, let \(\varGamma (L)\) be the set of formulae defined by

where \(c\in \mathbb N\), \({\bowtie } \in \{{\le },{<},{\ge },{>}\}\), and \(\ell \in L\). Compared to the clock constraints defined above for TA s, \(\varGamma (L)\) allows non-determinism (\(\vee \) operator), locations as atoms, and expressions of the form \(x.\gamma \) (meaning that x is reset in \(\gamma \)). An OCATA is a tuple \(\mathcal A=(L,\varSigma ,\ell _0,\delta ,F)\) where L is a finite set of locations, \(\varSigma \) is a finite alphabet, \(\ell _0\in L\) is the initial location, \(\delta :L\times \varSigma \rightarrow \varGamma (L)\) is the transition function, and \(F\subseteq L\) is the set of final locations. A state of \(\mathcal A\) is a pair \((\ell ,v)\) of a location in L and a valuation of the single clock x. Models of the formulae in \(\varGamma (L)\), with respect to a clock valuation \(v\in \mathbb R^+\), are sets of states M:

• \(M\models _v \top \); \(M\models _v \ell \) if \((\ell ,v)\in M\); \(M\models _v x\bowtie c\) if \(v\bowtie c\); \(M\models _v x.\gamma \) if \(M\models _0 \gamma \);

• \(M\models _v \gamma _1\wedge \gamma _2\) if \(M\models _v \gamma _1\) and \(M\models _v \gamma _2\);

• \(M\models _v \gamma _1\vee \gamma _2\) if \(M\models _v \gamma _1\) or \(M\models _v \gamma _2\).

A set M of states is said to be a minimal model of the formula \(\gamma \in \varGamma (S)\) with respect to a clock valuation \(v\in \mathbb R^+\) if and only if \(M\models _v \gamma \) and there is no proper subset \(M'\subset M\) with \(M'\models _v \gamma \). A run of \(\mathcal A\) over a timed word \(\rho =(\sigma _1,\tau _1)(\sigma _2,\tau _2)\cdots \in T\varSigma ^\omega \) is a rooted directed acyclic graph (DAG) \(G=(V,{\rightarrow })\) with vertices of the form \((\ell ,v,i)\in L\times \mathbb R^+\times \mathbb N\), \((\ell _0,0,0)\) as root, and edges as follows: for every vertex \((\ell ,v,i)\), we choose a minimal model M of the formula \(\delta (\ell ,\sigma _{i+1})\) with respect to \(v+(\tau _{i+1}-\tau _i)\) (again, \(\tau _0=0\)), and we have an edge \((\ell ,v,i) \rightarrow (\ell ',v',i+1)\) in G for every state \((\ell ',v')\) appearing in model M. Such a run is accepting if and only if there is no infinite path in G that visit final locations only finitely often. We let \(\llbracket \mathcal A\rrbracket \) be the set of timed words on which there exist accepting runs of \(\mathcal A\).

It is also useful to see a run as a linear sequence of configurations (i.e. finite sets of states) which gather all states at a given DAG level. Formally, from a DAG \(G=(V,{\rightarrow })\) we extract the sequence of configurations \(K_0, K_1,\dots \) where \(K_i=\{(\ell ,v)\mid (\ell ,v,i)\in V\}\) for all \(i\ge 0\).^{Footnote 2}

An OCATA accepting the language of \(\mathbf {G}(p\Rightarrow \mathbf {F}_{[0,1]}q)\).

Full size image

A run of the OCATA of Fig. 1 over \((\emptyset ,0.42)(\{p\},0.42)(\{q\},0.7)\cdots \).

Full size image

Example 1

Consider the OCATA of Fig. 1 on the alphabet \(\varSigma =2^{\{p,q\}}\). For each proposition \(\pi \in \{p,q\}\), we write \(\varSigma _\pi =\{\sigma \in \varSigma \mid \pi \in \sigma \}\). A run over the timed word \((\emptyset ,0.42)(\{p\},0.42)(\{q\},0.7)\cdots \) is depicted in Fig. 2. It starts with the DAG rooted in \((\ell _0,0,0)\) (initially, there is only one copy in \(\ell _0\) with the clock equal to 0). This root has a single successor \((\ell _0,0.42,1)\), which has two successors \((\ell _0,0.42,2)\) and \((\ell _1,0,2)\) (after firing the conjunctive transition from \(\ell _0\)). Then, \((\ell _1,0,2)\) has no successor since the empty model is a minimal model of the next transition (the transition from \(\ell _1\) points to no location). The associated sequence of configurations starts by: \(\{(\ell _0,0)\},\{(\ell _0,0.42)\},\{(\ell _0,0.42),(\ell _1,0)\}\cdots \)

Each formula \(\varphi \) of MITL can be translated into an OCATA \(\mathcal A_\varphi \) that accepts the same language [11, 30], and with a number of locations linear in the number of subformulae of \(\varphi \). We recall the definition of \(\mathcal A_\varphi \) for the sake of completeness. The set of locations of \(\mathcal A_\varphi \) contains: (i) \(\varphi _{init}\); (ii) all the subformulae of \(\varphi \) (that we suppose to be in negative normal form) whose outermost operator is \(\mathbin {\mathbf {U}}_I\) or \(\mathbin {\mathbf {R}}_I\); and (iiii) \(\psi ^r\) for each subformulae \(\psi \) of \(\varphi \) whose outermost operator is \(\mathbf {X}_I\) or \(\overline{\mathbf {X}}_I\). Its initial location is \(\varphi _{init}\), and the accepting locations of F are all the subformulae of the form \(\varphi _1 \mathbin {\mathbf {R}}_I \varphi _2\). Finally, \(\delta \) is defined inductively:

• \(\delta (\varphi _{init},\sigma )=x.\delta (\varphi ,\sigma )\), \(\delta (\top ,\sigma )=\top \), and \(\delta (\bot ,\sigma )=\bot \);

• \(\delta (p,\sigma ) = \top \) if \(p\in \sigma \), \(\delta (p,\sigma )=\bot \) otherwise;

• \(\delta (\lnot p,\sigma ) = \top \) if \(p\notin \sigma \), \(\delta (\lnot p,\sigma )=\bot \) otherwise;

• \(\delta (\varphi _1\vee \varphi _2,\sigma )=\delta (\varphi _1,\sigma )\vee \delta (\varphi _2,\sigma )\), and \(\delta (\varphi _1\wedge \varphi _2,\sigma )=\delta (\varphi _1,\sigma )\wedge \delta (\varphi _2,\sigma )\);

• \(\delta (\varphi _1\mathbin {\mathbf {U}}_I\varphi _2,\sigma )= (x.\delta (\varphi _2,\sigma )\wedge x\in I)\vee (x.\delta (\varphi _1,\sigma )\wedge \varphi _1\mathbin {\mathbf {U}}_I\varphi _2\wedge x\le \sup I)\);

• \(\delta (\varphi _1\mathbin {\mathbf {R}}_I\varphi _2,\sigma )= (x.\delta (\varphi _2,\sigma )\vee x\notin I)\wedge (x.\delta (\varphi _1,\sigma )\vee \varphi _1\mathbin {\mathbf {R}}_I\varphi _2\vee x> \sup I)\);

• \(\delta (\mathbf {X}_I \varphi ,\sigma )=x.(\mathbf {X}_I\varphi )^r\), and \(\delta ((\mathbf {X}_I \varphi )^r,\sigma ) = x\in I \wedge x.\delta (\varphi ,\sigma )\);

• \(\delta (\overline{\mathbf {X}}_I \varphi ,\sigma )=x.(\overline{\mathbf {X}}_I\varphi )^r\), and \(\delta ((\overline{\mathbf {X}}_I \varphi )^r,\sigma ) = x\notin I \vee x.\delta (\varphi ,\sigma )\).

As already noticed in [11], the OCATA \(\mathcal A_\varphi \) produced from an MITL formula \(\varphi \) is very-weak [19, 26, 29], i.e. it comes with a partial order on its locations such that all locations appearing in \(\delta (\ell ,\sigma )\) are bounded above by \(\ell \) in this order. For an OCATA \(\mathcal A_\varphi \) obtained from an MITL formula \(\varphi \), the order is given by the subformula order: \(\varphi _{init}\) is the greatest element in the order, and a location \(\psi \) is less than \(\chi \) if \(\psi \) is a subformula of \(\chi \). We will also make use of the following properties of \(\delta \): (i) if \(\ell '\) appears in \(\delta (\ell , \sigma )\) then it is preceded by a clock reset if and only if \(\ell '\ne \ell \); and (ii) each \(\ell '\) either has no parent or has a unique parent, i.e. there is a unique \(\ell \ne \ell '\) such that \(\ell '\) appears in \(\delta (\ell , \sigma )\) for some \(\sigma \).

Theorem 2

([11]). For all formulae \(\varphi \) of MITL, \(\llbracket \mathcal A_\varphi \rrbracket =\llbracket \varphi \rrbracket \).

Remark 3

To ease the presentation, we use Boolean formulae over atomic propositions as transition labels. For instance, \(\varSigma \setminus \varSigma _p\) will be written as \(\lnot p\).

The current and next two sections are devoted to explaining the core idea of our construction: simulate the OCATA \(\mathcal A_\varphi \) obtained from an MITL formula \(\varphi \) by the synchronous product of component Büchi timed automata, one for each temporal subformula (i.e. a subformula whose outermost operator is temporal). The very-weakness of \(\mathcal A_\varphi \) is crucial for our construction to work: a run of \(\mathcal A_\varphi \) is accepting if and only if \(\mathcal A_\varphi \) does not get stuck at a non-accepting location in any branch. Therefore, we can keep track of each location with a separate component and simply define a suitable Büchi acceptance condition on each such component.^{Footnote 3} Our compositional construction preserves the structure of the formula, and thus we can hope that the model-checking tool (which is responsible for the composition) takes this into account.^{Footnote 4} At the very least, the model-checking tool can use an on-the-fly approach in composition (as is indeed the case for Uppaal and LTSmin), which is often faster in practice: the explicit construction of the whole product can be avoided when there is an accepting run.

In what follows, let \(\varphi \) be an MITL formula over \(\textsf {AP} \) in negative normal form and \(\mathcal A_\varphi \) be the OCATA obtained from \(\varphi \) with the translation described earlier. For the sake of simplicity, we make the following assumptions:

• \(\mathbf {X}_I\) and \(\overline{\mathbf {X}}_I\) do not appear in \(\varphi \);

• each temporal subformula \(\psi \) of \(\varphi \) appears only once in \(\varphi \).

Let \(\varPhi \) be the set of temporal subformulae of \(\varphi \). We introduce a new atomic proposition \(p_{\psi }\) for each subformula \(\psi \in \varPhi \) (i.e. for each non-initial location of the OCATA \(\mathcal A_\varphi \)) and let \(\textsf {AP} _\varphi \) be the set of these new atomic propositions. For each (not necessarily temporal) subformula \(\psi \) of \(\varphi \), we denote by \(\mathcal {P}_\psi \) the set of atomic propositions \(p_\xi \in \textsf {AP} _\varphi \) such that \(\xi \) is a top-level temporal subformula of \(\psi \), i.e. the outermost operator of \(\xi \) is \(\mathbin {\mathbf {U}}_I\) or \(\mathbin {\mathbf {R}}_I\), yet \(\xi \) does not occur under the scope of another \(\mathbin {\mathbf {U}}_I\) or \(\mathbin {\mathbf {R}}_I\). For instance, \(\mathcal {P}_{p\mathbin {\mathbf {U}}_I q \vee r\mathbin {\mathbf {U}}_I (s\mathbin {\mathbf {R}}t)} = \{p_{p\mathbin {\mathbf {U}}_I q},p_{r\mathbin {\mathbf {U}}_I (s\mathbin {\mathbf {R}}t)}\}\).

Hintikka Sequences and Triggers. A Hintikka sequence of \(\varphi \) is a timed word \(\rho '\) over \(2^{\textsf {AP} \cup \textsf {AP} _\varphi }\). Intuitively, Hintikka sequences can be regarded as an instrumented version of timed words, where the extra atomic propositions from \(\textsf {AP} _\varphi \) are triggers that connect timed words to their runs in the OCATA \(\mathcal A_\varphi \); this is the central notion of our construction which, as we will prove, indeed simulates the runs of \(\mathcal A_\varphi \). Pulling the trigger \(p_\psi \) (i.e. setting \(p_\psi \) to true) at some point means that \(\psi \) is required to hold at this point. However, the absence of a trigger \(p_\xi \) does not mean that subformula \(\xi \) must not be satisfied—its satisfaction is simply not required at this point. We denote by \(\textsf {proj} _\textsf {AP} (\rho ')\) the timed word obtained by hiding all the atomic propositions in \(\textsf {AP} _\varphi \) from \(\rho '\). We also let \(\textsf {proj} _\textsf {AP} (\mathcal {L})=\{\textsf {proj} _\textsf {AP} (\rho ')\mid \rho '\in \mathcal {L}\}\) for a timed language \(\mathcal {L}\) over \(2^{\textsf {AP} \cup \textsf {AP} _\varphi }\).

Formulae Over \(\textsf {AP} \cup \textsf {AP} _\varphi \) . We now introduce some syntactic operations on Boolean combinations of atomic propositions in \(\textsf {AP} \cup \textsf {AP} _\varphi \), that will be used to construct the component Büchi automata later. Specifically, for a subformula \(\psi \) of \(\varphi \), we define formulae \(\overline{\psi }\), \(*\psi \), \({\sim }\psi \), and \(\widehat{\psi }\).

The automata (a) \(\mathcal C_{init}\) and \(\mathcal C_\chi \) for (b) \(\chi = \varphi _1\mathbin {\mathbf {U}}\varphi _2\), and (c) \(\chi = \varphi _1\mathbin {\mathbf {R}}\varphi _2\).

Full size image

The formula \(\overline{\psi }\) is obtained from \(\psi \) by replacing all top-level temporal subformulae by their corresponding triggers. Formally, \(\overline{\psi }\) is defined inductively as follows (where \(p\in \textsf {AP} \cup \textsf {AP} _\varphi \)):

The formula \(*\psi \), read as “do not pull the triggers of \(\psi \)”, will be used to ensure that our component automata only follow the minimal models of the transition function of \(\mathcal A_\varphi \) (we will see in Sect. 6 how crucial it is, for performance, to generate only minimal models). It is the conjunction of negations of all the atomic propositions in \(\mathcal {P}_\psi \). As a concrete example,

The formula \({\sim }\psi \) asserts that \(\overline{\psi }\) is false and none of its triggers are activated: \({\sim }\psi = \lnot \overline{\psi }\wedge *\psi \). Finally, the formula \(\widehat{\psi }\) is defined as \(\textsf {mm} (\overline{\psi })\) where \(\textsf {mm} (\alpha )\) is defined inductively as follows:

Intuitively, \(\textsf {mm} (\alpha )\) is satisfiable if and only if \(\alpha \) is satisfiable, but \(\textsf {mm} (\alpha )\) only permits models of \(\alpha \) that are minimal with respect to the triggers it contains: for \(\textsf {mm} (\alpha _1\vee \alpha _2)\) to be true, either \(\textsf {mm} (\alpha _1)\) is true and \(\alpha _2\) does not hold, or vice versa, or \(\alpha _1\vee \alpha _2\) is indeed true, but not because of any of the triggers it contains.

Component Büchi Automata for LTL. We are now ready to present the construction for the case that \(\varphi \) is an LTL formula. Instead of building a monolithic Büchi automaton \(\mathcal B_\varphi \) directly from the alternating automaton, as in [19], we build small component Büchi automata that are language-equivalent to the automaton \(\mathcal B_\varphi \), once synchronised. There is an initial component \(\mathcal C_{init}\), and a component Büchi automaton \(\mathcal C_\chi \), for each \(\chi \in \varPhi \) (see Fig. 3). Consider, for instance, the case \(\chi =\varphi _1\mathbin {\mathbf {U}}\varphi _2\). Component \(\mathcal C_\chi \) has two locations 0 and 1 with the following intended meaning: \(\mathcal C_\chi \) is in location 1 if and only if the trigger \(p_\chi \) has been pulled in the past by \(\mathcal C_{init}\), in which case \(p_\chi \in \mathcal {P}_\varphi \), or by a unique component \(\mathcal C_{\psi _1 \mathbin {\mathbf {U}}_I \psi _2}\) (or \(\mathcal C_{\psi _1 \mathbin {\mathbf {R}}_I \psi _2}\)) such that \(p_\chi \in \mathcal {P}_{\psi _1}\) or \(p_\chi \in \mathcal {P}_{\psi _2}\), and \(\chi \) has not been satisfied yet. When component \(\mathcal C_\chi \) is in location 1, we say that we have an obligation for \(\chi \). To satisfy this obligation, we must see a letter in the future where \(\varphi _2\) holds. Thus, there is a self-loop on location 1 whose label ensures that \(\varphi _2\) does not hold (because of \({\sim }\varphi _2\)), while \(\varphi _1\) still holds (this is ensured by \(\widehat{\varphi _1}\), which also pulls a minimal set of triggers for \(\varphi _1\) to be satisfied). \(\mathcal C_\chi \) moves back from 1 to 0 when \(\varphi _2\) holds, while no trigger of \(\varphi _1\) should be pulled at this instant (which is translated by \(*\varphi _1\)). From location 0, if we do not read trigger \(p_\chi \), nothing has to be checked and we do not pull any trigger. However, if \(p_\chi \) is pulled, then, either \(\varphi _2\) holds right away and the obligation is fulfilled immediately, or we jump to location 1. The component \(\mathcal C_\chi \) for the case \(\chi =\varphi _1\mathbin {\mathbf {R}}\varphi _2\) is based on a similar reasoning. We state the following proposition without proof as it will be superseded by a stronger proposition in the next section.

Proposition 4

For all LTL formulae \(\varphi \), \(\textsf {proj} _\textsf {AP} (\llbracket \mathcal C_{init}\times \prod _{\chi \in \varPhi }\mathcal C_\chi \rrbracket ) = \llbracket \varphi \rrbracket \).

Example 5

Consider the LTL formula \(\mathbf {G}(p\Rightarrow \mathbf {F}q)\) that can be rewritten into negative normal form as \(\varphi = \bot \mathbin {\mathbf {R}}(\lnot p\vee \top \mathbin {\mathbf {U}}q)\). Then, the three component Büchi automata \(\mathcal C_{init}\), \(\mathcal C_\varphi \) and \(\mathcal C_{\mathbf {F}q}\), after the constraints on the transitions are simplified, are depicted on the top of Fig. 4, The automaton \(\mathcal C=\mathcal C_{init}\times \mathcal C_\varphi \times \mathcal C_{\mathbf {F}q}\) is depicted in the middle of the figure. Once atomic propositions in \(\textsf {AP} _\varphi \) are projected away, one obtains an automaton isomorphic to the one at the bottom of the figure that accepts \(\llbracket \varphi \rrbracket \).

We now describe how to lift the translation we described earlier to the timed operators of \(\textsf {MITL} _{0,\infty }\). The new components for \(\mathbin {\mathbf {U}}_{[0,a]}\), \(\mathbin {\mathbf {R}}_{[0,a]}\), and \(\mathbin {\mathbf {R}}_{[a,\infty )}\) are depicted in Fig. 5. They have the same shape as the components for untimed \(\mathbin {\mathbf {U}}\) and \(\mathbin {\mathbf {R}}\) (see Fig. 3); only the guards are changed to reflect the more involved semantics of the timed operators. Observe that these automata have only one clock. To understand why this is sufficient, consider the formula \(\mathbf {G}(p \Rightarrow \chi )\) with \(\chi = p \mathbin {\mathbf {U}}_{[0,2]} q\). After reading \((\{p\},0) (\{p\},0.4) (\{p\},1)\), the OCATA \(\mathcal A_\varphi \) reaches the configuration \(\{(\varphi ,0), (\chi ,0), (\chi ,0.6),(\chi ,1)\}\), meaning intuitively that, to satisfy the formula, one must fulfil three obligations related to \(\chi \): to see q’s within 2, 1.4, and 1 time units, respectively. Hence, we can store the earliest obligation, corresponding to \((\chi ,1)\), only (as already observed in [11]). Indeed, if the corresponding instance of \(\chi \) is satisfied, it means that there will be a q occurring within less that 1 time unit, which will also satisfy all the other obligations. More generally, for operators \(\mathbin {\mathbf {U}}_{[0,a]}\) and \(\mathbin {\mathbf {R}}_{[a,\infty )}\), it is always the case that only the oldest obligation has to be stored, while for operators \(\mathbin {\mathbf {R}}_{[0,a]}\) and \(\mathbin {\mathbf {U}}_{[a,\infty )}\), only the earliest obligation has to be stored. This is translated in the components by the absence/presence of resets on transitions that leave state 1 (which is reached when an obligation is currently active) and read \(p_\chi \).

(a) Component Büchi automata for the formula \(\varphi = \bot \mathbin {\mathbf {R}}(\lnot p\vee \top \mathbin {\mathbf {U}}q)\); (b) Büchi automaton obtained by the product of the components; (c) Büchi automaton obtained by projecting away \(\textsf {AP} _\varphi \) (and merging two identical locations).

Full size image

One-clock TA for the subformulae: (a) \(\chi = \varphi _1\mathbin {\mathbf {U}}_{[0,a]} \varphi _2\), (b) \(\chi = \varphi _1\mathbin {\mathbf {R}}_{[0,a]} \varphi _2\), and (c) \(\chi = \varphi _1\mathbin {\mathbf {R}}_{[a,\infty )} \varphi _2\).

Full size image

For \(\chi = \varphi _1 \mathbin {\mathbf {U}}_{[a,\infty )}\varphi _2\), the situation is slightly more complicated, although one clock is again sufficient. The corresponding component is in Fig. 6 and has four locations. To understand why, consider the case when there is an obligation for \(\chi \) associated with the current valuation \(v\ge a\) of clock x (\(\mathcal C_\chi \) is in location 1), the current letter contains \(p_\chi \) and satisfies both \(\widehat{\varphi _1}\) and \(\widehat{\varphi _2}\). Since the trigger has been pulled, \(\mathcal C_\chi \) should stay in the non-accepting location 1. On the other hand, the pending obligation has also been fulfilled, and an accepting location should be visited. So, instead of staying in 1, \(\mathcal C_\chi \) moves to \(1'\) in this case: \(1'\) is a copy of 1 as far as transitions are concerned, but it is accepting. The location \(1''\) is used to deal with the situation where \(p_\chi \) is launched infinitely often but no two occurrences of \(p_\chi \) are separated by more than a time units; in this case, we non-deterministically move to \(1''\) and add a new obligation (by resetting x) after the current obligation has been verified. Notice that this problem cannot occur for \(\varphi _1\mathbin {\mathbf {U}}\varphi _2\), or \(\varphi _1\mathbin {\mathbf {U}}_{[0,a]} \varphi _2\): in these cases, the new obligation is immediately fulfilled, and the automaton moves to the initial, accepting, location.

We now present the extension of Proposition 4 to the case of \(\textsf {MITL} _{0,\infty }\). The proof relies on a function that, given a formula \(\gamma = \delta (\ell , \sigma )\) (where \(\delta \) is the transition function of \(\mathcal A_\varphi \), \(\ell \) is a location of \(\mathcal A_\varphi \), and \(\sigma \in \varSigma = 2^{\textsf {AP} }\)) and a minimal model M of \(\gamma \) with respect to a clock valuation \(v\in \mathbb R^+\), recovers the set of triggers activated. Formally, we write \(\textsf {trig}_\varphi (M,\gamma ,v)\) for the subset of \(\textsf {AP} _\varphi \) inductively defined by (the rule for \(x.\gamma \) where \(\gamma = \delta (\ell , \sigma ) \text { for some } \ell \in \varPhi \) has precedence over the rule for \(x.(\gamma _1\wedge \gamma _2)\) and \(x.(\gamma _1\vee \gamma _2)\)):

One-clock TA for the subformula \(\chi = \varphi _1\mathbin {\mathbf {U}}_{[a,\infty )} \varphi _2\).

Full size image

• \(\textsf {trig}_\varphi (M,\gamma _1\wedge \gamma _2,v)=\textsf {trig}_\varphi (M,\gamma _1,v)\cup \textsf {trig}_\varphi (M,\gamma _2,v)\);

• \(\textsf {trig}_\varphi (M,\gamma _1\vee \gamma _2,v)={\left\{ \begin{array}{ll}\textsf {trig}_\varphi (M,\gamma _1,v) &{} \text {if } M\models _v \gamma _1\\ \textsf {trig}_\varphi (M,\gamma _2,v) &{} \text {otherwise;}\end{array}\right. }\)

• \(\textsf {trig}_\varphi (M,x.\gamma ,v)= \{p_\ell \} \cup \textsf {trig}_\varphi (M,\gamma ,0) \text { if } \gamma = \delta (\ell , \sigma ) \text { for some } \ell \in \varPhi \);

• \(\textsf {trig}_\varphi (M,x.(\gamma _1\wedge \gamma _2),v)=\textsf {trig}_\varphi (M,x.\gamma _1,v)\cup \textsf {trig}_\varphi (M,x.\gamma _2,v)\);

• \(\textsf {trig}_\varphi (M,x.(\gamma _1\vee \gamma _2),v)={\left\{ \begin{array}{ll}\textsf {trig}_\varphi (M,x.\gamma _1,v) &{} \text {if } M\models _v x.\gamma _1\\ \textsf {trig}_\varphi (M,x.\gamma _2,v) &{} \text {otherwise;}\end{array}\right. }\)

• \(\textsf {trig}_\varphi (M,\gamma ,v)=\emptyset \) otherwise.

Proposition 6

For all \(\textsf {MITL} _{0,\infty }\) formulae \(\varphi \), \(\textsf {proj} _\textsf {AP} (\llbracket \mathcal C_{init}\times \prod _{\chi \in \varPhi }\mathcal C_\chi \rrbracket ) = \llbracket \varphi \rrbracket \).

Proof

(Sketch). Recall that Theorem 2 states that \(\llbracket \varphi \rrbracket =\llbracket \mathcal A_\varphi \rrbracket \). Therefore, it suffices to relate the accepting runs of the synchronous product of all component Büchi timed automata \(\mathcal C= \mathcal C_{init}\times \prod _{\chi \in \varPhi }\mathcal C_\chi \) with the accepting runs of \(\mathcal A_\varphi \). Let us consider a timed word \(\rho \in \llbracket \mathcal A_\varphi \rrbracket \) and an accepting run \(G=(V,{\rightarrow })\) of \(\mathcal A_\varphi \) over \(\rho \). Let \(K_0,K_1,\dots \) be the sequence of configurations associated with G.

We first construct the instrumented timed word \(\rho '\) over \(2^{\textsf {AP} \cup \textsf {AP} _\varphi }\) from \(\rho \) and G by adding the triggers in \(\textsf {AP} _\varphi \) according to the minimal models selected in G. More precisely, for all \(i\ge 0\), we associate with every state \((\ell ,v)\) of \(K_i\) the pair \((\gamma _{\ell ,v},M_{\ell ,v})\) where \(\gamma _{\ell ,v} = \delta (\ell ,\sigma _{i+1})\) and \(M_{\ell ,v}\) is the minimal model of \(\gamma _{\ell ,v}\) with respect to \(v+\tau _{i+1}-\tau _i\) chosen in G. We then gather all the triggers in \(\mathcal Q_i = \bigcup _{(\ell ,v)\in K_i} \textsf {trig}_\varphi (M_{\ell ,v},\gamma _{\ell ,v},v+\tau _{i+1}-\tau _i)\), and let \(\rho '=(\sigma _1\cup \mathcal Q_1,\tau _1) (\sigma _2\cup \mathcal Q_2,\tau _2)\cdots \). Then, it can be shown that each component has an accepting run over \(\rho '\). By definition, the generalised Büchi acceptance condition on \(\mathcal C\) is fulfilled exactly when the Büchi acceptance condition on each of the components is fulfilled. It follows that \(\mathcal C\) accepts \(\rho '\), and hence \(\rho \in \textsf {proj} _\textsf {AP} (\llbracket \mathcal C\rrbracket )\). The other direction of the proof consists of building an accepting run G of \(\mathcal A_\varphi \) over \(\textsf {proj} _\textsf {AP} (\rho ')\) from an accepting run of \(\mathcal C\) over \(\rho '\in \llbracket \mathcal C\rrbracket \). At each level of G, the truth values of the triggers in \(\rho '\) are used to guide the construction of minimal models.    \(\square \)

How to split cases to satisfy the formula \(\chi =\varphi _1\mathbin {\mathbf {U}}_{[a,b]} \varphi _2\).

Full size image

We can now extend our translation to full MITL, i.e. allowing operators \(\mathbin {\mathbf {U}}_{[a,b]}\) and \(\mathbin {\mathbf {R}}_{[a,b]}\) with \(0<a<b<+\infty \). For these two types of operators, we cannot rely on a single clock in the components anymore. For instance, consider the formula \(\varphi =\mathbf {G}(p\Rightarrow \chi )\) with \(\chi =\mathbf {F}_{[1,2]} q\). Imagine that \(\mathcal A_\varphi \) reads the prefix \((\{p\},0)(\{p\},0.5)\). At this point, its configuration is \(\{(\varphi ,0),(\chi ,0),(\chi ,0.5)\}\). It is not possible, as before, to drop one of the two states in location \(\chi \) as the following futures can happen: if we read \((\{q\},1)\), obligation \((\chi ,0)\) is fulfilled but not \((\chi ,0.5)\); if we read \((\{q\},2.5)\) then the obligation \((\chi ,0.5)\) is fuilfilled but not \((\chi ,0)\). Therefore, we must keep track of the two obligations separately. It is, however, not clear how to find an a priori bound on the number of clocks. This is the role of the interval semantics introduced in [11] for OCATA s resulting from MITL formulae over infinite words. In this interpretation of OCATA s, valuations of the clocks are no longer points but intervals meant to approximate sets of (singular) valuations: \((\ell ,[\alpha ,\beta ])\) means that there are clock copies with valuations \(\alpha \) and \(\beta \) in \(\ell \), yet there could be more copies in \(\ell \) with valuations in \((\alpha ,\beta )\). In this semantics, we can merge non-deterministically two copies \((\ell , [\alpha _1,\beta _1])\) and \((\ell , [\alpha _2,\beta _2])\) into a single copy \((\ell , [\alpha _1,\beta _2])\) (assuming \(\alpha _1\le \beta _2\)), in order to keep the number of clock copies below a fixed threshold, and thus obtain an equivalent TA. It has been shown in [11] that, for the OCATA \(\mathcal A_\varphi \), with \(\varphi \in \textsf {MITL} \), the interval semantics is sufficient to retain the language of the formula, with TA s having at most \(M(\varphi )=|\varphi |\times \max _{I\in \mathcal I_\varphi }(\max (4\times \lceil \inf (I) / |I|\rceil + 2, 2\times \lceil \sup (I) / |I| \rceil +2))\) clocks, where \(\mathcal I_\varphi \) is the set of intervals that appear in \(\varphi \): more precisely, each subformula with topmost operator \(\mathbin {\mathbf {U}}_I\) (respectively, \(\mathbin {\mathbf {R}}_I\)) contributes to \(4\times \lceil \inf (I) / |I|\rceil + 2\) (respectively, \(2\times \lceil \sup (I) / |I| \rceil +2\)) more clocks.

Our solution is twofold in this context: (i) we propose a better approximation by intervals that allows us to cut, up to a factor of two, the number of clock copies we must keep in memory; (ii) instead of a single TA, as in [11], we provide a GBTA, with one component per temporal subformula of \(\varphi \). The component TA are much more involved than for \(\textsf {MITL} _{0,\infty }\), thus we do not give them explicitly, but rather explain the main ideas.

We start by developing our new merging strategy on an example, to explain how it is different from [11]. Consider \(\chi = \varphi _1\mathbin {\mathbf {U}}_{[a,b]} \varphi _2\) with \(0<a<b<+\infty \) and the situation depicted in Fig. 7, where the trigger \(p_\chi \) is pulled at three positions of time stamps \(\tau _1\), \(\tau _2\), and \(\tau _3\). We suppose that \(\varphi _1\) holds at all three positions. The picture presents four different cases corresponding to the four possible situations where the occurrences of \(\varphi _2\) fulfil the three pending obligations. Case 1 is when a position in \([\tau _3+a, \tau _1+b]\) satisfies \(\varphi _2\), hence all three obligations are resolved at once. This case can be checked using only clocks \(x_3\) and \(x_1\). In case 2, the first obligation is resolved by an occurrence of \(\varphi _2\) with time stamp in \([\tau _1+a, \tau _2+a)\), while the two others are resolved by an occurrence in \((\tau _1+b, \tau _2+b]\). Thus, case 2 can be checked using only clocks \(x_1\) and \(x_2\). Now consider the remaining cases: if no occurrences of \(\varphi _2\) appear in \([\tau _1+a, \tau _2+a)\cup [\tau _3+a, \tau _1+b]\), one occurrence of \(\varphi _2\) must necessarily happen in \([\tau _2+a, \tau _3+a)\), while the other should be in \((\tau _1+b, \tau _3+b]\), which can only be checked using three clocks \(x_1\), \(x_2\) and \(x_3\). We avoid this by splitting this case into two further cases (cases 3 and 4) that can be checked with only two clocks. Specifically, case 3 can be checked using only clocks \(x_2\) and \(x_3\); and case 4 using only clocks \(x_2\) and \(x_1\).

Observe that these cases can be categorised into two groups: one where \(\varphi _2\) should occur in a single interval whose endpoints use two distinct clocks (case 1), another where \(\varphi _2\) should occur in two half-open intervals whose both endpoints use the same two distinct clocks (cases 2, 3 and 4). In each of the two groups, it must be understood how a new obligation (added by pulling the trigger \(p_\chi \)) modifies the situation. With only one interval, if a new obligation for \(\varphi _2\) appear as a new interval \([\tau +a,\tau +b]\), either the new obligation is implied by the current one, in which case we are done, or the two intervals intersect and we do a further split (non-deterministically) into cases 1, 3 and 4, or they are disjoint and we keep both intervals in memory. The latter situation cannot happen too often since intervals are non-singular; more precisely, this will happen at most \(\lceil (\inf (I)/|I|) + 1\rceil \) times (\(I = [a, b]\)). With two intervals, either the new obligation is already implied by current obligations, or \([\tau +a,\tau +b]\) is not implied by the current obligations and we add this new interval in memory as before (again, this cannot happen more than \(\lceil (\inf (I)/|I|) + 1\rceil \) times).

In the end, following the same lines as [11], we can build a component \(\mathcal C_\chi \) for each subformula \(\chi =\varphi _1\mathbin {\mathbf {U}}_{[a,b]}\varphi _2\) with \(N(\chi )=2\times \lceil (\inf (I)/|I|) + 1\rceil +2\) clocks (the two additional clocks are used to deal easily with some special cases), which is roughly half of the previous bound on the number of clocks [11]. In the locations, we can handle the clocks in pairs and use a queue of size \(N(\chi )/2\) to keep track of which case we fall into and which clocks are used to represent the endpoints of intervals. It follows that the number of locations is exponential in \(N(\chi )\). A similar construction, using \(2\times \lceil (\inf (I)/|I|) + 1\rceil \) clocks, builds a component \(\mathcal C_\chi \) for each subformula \(\chi = \varphi _1\mathbin {\mathbf {R}}_{[a,b]}\varphi _2\). In this case, we have to consider unions of intervals, which are easier to deal with.

Theorem 7

For all \(\textsf {MITL} \) formulae \(\varphi \), \(\textsf {proj} _\textsf {AP} (\llbracket \mathcal C_{init}\times \prod _{\chi \in \varPhi }\mathcal C_\chi \rrbracket ) = \llbracket \varphi \rrbracket \).

Proof

(Sketch). We follow the same lines of the proof of Proposition 6, i.e. relating the accepting runs of \(\mathcal A_\varphi \) with the accepting runs of \(\mathcal C=\mathcal C_{init}\times \prod _{\chi \in \varPhi }\mathcal C_\chi \). To show that \(\llbracket \mathcal A_\varphi \rrbracket \subseteq \textsf {proj} _\textsf {AP} (\llbracket \mathcal C\rrbracket )\), we use the same construction of the Hintikka sequence over \(2^{\textsf {AP} \cup \textsf {AP} _\varphi }\). Note that we have the accepting run G, so that we know in advance how each obligation is to be fulfilled in the future. In particular, we use this knowledge to resolve the non-determinism in components of the form \(\mathcal C_{\varphi _1\mathbin {\mathbf {U}}_{[a,b]}\varphi _2}\) or \(\mathcal C_{\varphi _1\mathbin {\mathbf {R}}_{[a,b]}\varphi _2}\). The other direction is also similar.    \(\square \)

We have implemented our translation from MITL formulae to generalised Büchi timed automata in a tool called MightyL, written in OCaml. From a formula \(\varphi \), it produces the GBTA \(\mathcal C\), described in previous sections, in the xml format used by Uppaal, as well as the generalised Büchi condition written as a very simple LTL formula. When the input formula is in \(\textsf {MITL} _{0,\infty }\), the translation can be done in polynomial time. For the general case, it runs in exponential time (assuming a succinct encoding of constants, as is the case here). We can then use Uppaal [27] to check the satisfiability of \(\varphi \) over finite timed words, or LTSmin [24] with opaal front-end to check satisfiability over infinite timed words. To maximise compatibility with model-checking tools, we use several helper variables in the output xml file, e.g. a Boolean variable for each atomic proposition and a loc variable in each component for the current location. The synchronisation is done in a round-robin fashion with a counter variable N: initially, N is set to 0, allowing the model (to be model-checked) to take a transition and set the truth values of the atomic propositions. Then, N loops from 1 to the number of components of \(\mathcal C\), allowing each component to read the atomic propositions and take a corresponding transition. Finally, N is set back to 0 and we start over again. For the finite-word case, this also enables to check that all components have been synchronised properly (\(\texttt {N} = 0\)) while in the final location. Our tool is publicly available, and can even be executed directly on the website

http://www.ulb.ac.be/di/verif/mightyl

Compared to the simplified version we studied in this article, MightyL also allows for (semi-)open intervals. Since it can also deal with next and dual-next operators, we can verify formulae like \(\lnot \mathbf {X}_{[1,2)} p\). All the following tests have been performed on a MacBook Pro 2.7 GHz with 8Go RAM.

We check the satisfiability of MITL formulae on examples, inspired by the benchmarks of [11, 19]. For \(k\in \mathbb N\) and an interval I, we consider the satisfiable formulae: \(F(k,I) = \textstyle {\bigwedge _{i=1}^k}\mathbf {F}_I p_i\), \(G(k,I) = \textstyle {\bigwedge _{i=1}^k} \mathbf {G}_I p_i\), \(U(k,I) = (\cdots (p_1 \mathbin {\mathbf {U}}_I p_2)\mathbin {\mathbf {U}}_I \cdots )\mathbin {\mathbf {U}}_I p_k\), \(R(k,I) = (\cdots (p_1 \mathbin {\mathbf {R}}_I p_2)\mathbin {\mathbf {R}}_I \cdots )\mathbin {\mathbf {R}}_I p_k\), and \(\theta (k,I) = \lnot ((\textstyle {\bigwedge _{i=1}^k}\mathbf {G}\mathbf {F}p_i)\Rightarrow \mathbf {G}(q\Rightarrow \mathbf {F}_I r))\). We also consider an example inspired from motion planning problems via MITL specifications as in [25, 31]. In this benchmark, a robot must visit some target points \(t_1, t_2, t_3, \dots , t_k\) within given time frames (in our case, \(t_i\) must be seen in time frame \([3(i-1), 3i]\)), while enforcing a safety condition \(\mathbf {G}\lnot p\). This specification is modelled by the satisfiable MITL formula \(\mu (k) = \textstyle {\bigwedge _{i=1}^k} \mathbf {F}_{[3(i-1),3i]} t_i \wedge \mathbf {G}\lnot p\). In Table 1, we report on the time taken by the execution of MightyL; LTSmin (split into the time taken by opaal front-end to translate the model into C++ code, the compilation time of the resulting C++ code, and the time taken by LTSmin for the actual model-checking); and Uppaal, on all these examples (for the motion planning, only finite words are relevant, hence we report only on the Uppaal running time).

We also report on the benchmarks found in [16], where the debugging of formal specifications of cyber-physical systems is reduced to MITL non-satisfiability. More precisely, we check formulae for validity and redundancy. In [16], a formula \(\varphi \) is called valid (with respect to a specification goal) if \(\varphi \) is neither unsatisfiable nor a tautology, i.e. \(\varphi \) and \(\lnot \varphi \) are both satisfiable. A conjunct \(\varphi _1\) of formula \(\varphi =\bigwedge _{i=1}^k\varphi _i\) is redundant if and only if \(\bigwedge _{i=2}^k \varphi _i\) implies \(\varphi _1\). This is true if and only if \(\psi =\bigwedge _{i=2}^k\varphi _i \Rightarrow \varphi _1\) is valid, i.e. if and only if \(\lnot \psi \) is not satisfiable. For instance, \(\mathbf {F}_{[0,30]} p\) is redundant in \(\mathbf {F}_{[0,30]} p\wedge \mathbf {F}_{[0,20]} p\), and \(\mathbf {G}_{[0,20]}\mathbf {F}_{[0,20]} p\) is redundant in \(\mathbf {G}_{[0,20]}\mathbf {F}_{[0,20]} p\wedge \mathbf {G}_{[0,40]}p \wedge \mathbf {F}_{[20,40]} \top \). We check the validity and redundancy of several formulae considered in [16] and report the results in Table 2. For reference, we copy the execution time reported in [16] for these checks.^{Footnote 5} We also consider some new formulae specific to our pointwise semantics.

Finally, recall that one technical part of the constructions of component Büchi timed automata is the minimal model simplification \(\textsf {mm} (\varphi )\). Our components remain correct if we replace everywhere \(\textsf {mm} (\varphi )\) by \(\varphi \) (i.e. \(\widehat{\varphi }\) simply becomes \(\overline{\varphi }\)). On some instances of the previous benchmarks, the influence on the execution time of the satisfiability checks is tremendous (differences on the execution time of MightyL negligible, since the tool always answers in less than a second). For instance, over \(F(5,[0,\infty ))\), LTSmin shows a \(17\%\) overhead. For F(5, [0, 2]), LTSmin experiences a \(5\%\) overhead, while Uppaal has a \(12\%\) overhead. For formulae \(F(5,[2,\infty ))\), F(3, [1, 2]), F(5, [1, 2]), the situation is even worse since Uppaal stops responding before the timeout of fifteen minutes. LTSmin also hangs on F(3, [1, 2]) before the timeout. On the motion planning example, the overhead is also significant for Uppaal, e.g. \(80\%\) for \(\mu _2\), and, for \(\mu _3\) and \(\mu _4\), Uppaal does not respond anymore before the timeout. Finally, on the two unsatisfiable examples of the redundancy check, LTSmin and Uppaal have overheads of \(70\%\)/\(3\%\) and \(630\%\)/\(230\%\), respectively.

In this work, we proposed a new compositional construction from MITL to timed automata which we implemented the tool MightyL, enabling easy automata-based model-checking of full MITL. For future work, since the structure of the formula is preserved in our construction, we want to investigate antichain-based heuristics to allow more performance boost. For MightyL, we plan to add native support for ECL [33] operators which eases the writing of specifications, as well as past operators and counting operators [23].