Efficient controller synthesis for a fragment of $\hbox {MTL}_{0, \infty }$

Abstract

In this paper we offer an efficient controller synthesis algorithm for assume-guarantee specifications of the form $\varphi _1 \wedge \varphi _2 \wedge \cdots \wedge \varphi _n \rightarrow \psi _1 \wedge \psi _2 \wedge \cdots \wedge \psi _m$. Here, $\{\varphi _i,\psi _j\}$ are all safety-MTL$_{0, \infty }$ properties, where the sub-formulas $\{\varphi _i\}$ are supposed to specify assumptions of the environment and the sub-formulas $\{\psi _j\}$ are specifying requirements to be guaranteed by the controller. Our synthesis method exploits the engine of Uppaal-Tiga and the novel translation of safety- and co-safety-MTL$_{0, \infty }$ properties into under-approximating, deterministic timed automata. Our approach avoids determinization of Büchi automata, which is the main obstacle for the practical applicability of controller synthesis for linear-time specifications. The experiments demonstrate that the chosen specification formalism is expressive enough to specify complex behaviors. The proposed approach is sound but not complete. However, it successfully produced solutions for all the experiments. Additionally we compared our tool with Acacia+ and Unbeast, state-of-the-art LTL synthesis tools; and our tool demonstrated better timing results, when we applied both tools to the analogous specifications.

1 Introduction

Automatic controller synthesis is concerned with the algorithmic construction of a control strategy, that will ensure a given behavioural specification to be satisfied regardless of the input provided by an environment. This problem was first stated in a discrete time setting by Church in 1962 in [14] and then theoretically solved for various specification formalisms in [11] and later works [10, 19, 24, 28, 31, 32].

The synthesis problem is computationally harder for linear time logics than the satisfiability and model-checking problems, and has for this reason been considered to be intractable for a long time. The main problem was that the first synthesis approaches involve the determinization of Büchi automata, which is a computationally hard problem. However, the synthesis problem has recently gained in practical performance with the development of the so-called Safraless synthesis algorithms [23] that avoid the Büchi determinization phase. This approach has been strengthened by using the bounded synthesis [33] and the antichain-based algorithm in [20] that have resulted in the tools Acacia and Acacia+ that demonstrate good performance for the reasonable sized formulas arising in practice [21]. Another direction of research tries to restrict the specification formalisms so that the synthesis problem will be easier to solve [7, 30]. We combine both directions, i.e. restrict ourselves to a formalism that does not require Safra’s procedure.

In the current paper we study the synthesis problem in a real-time setting. We focus our attention to the Metric Interval Temporal Logic (MITL) [3], a formalism which has proved to be useful for specifying real-time systems [1]. Unfortunately, the MITL synthesis problem is undecidable in general [17], but there are sub-classes that render the synthesis problem to be decidable [10, 26]. The main challenge for the real-time controller synthesis is that the Safraless approach is not always applicable for the timed case since determinization is not possible in general. Thus it makes sense to completely avoid the automata determinization phase.

In the current paper we push the boundaries of MITL synthesis forward to an important class of assume-guarantee properties, i.e. properties of the form $\Psi =\varphi _1 \wedge \varphi _2 \wedge \cdots \wedge \varphi _n \rightarrow \psi _1 \wedge \psi _2 \wedge \cdots \wedge \psi _m$. Here the implicants $\{\varphi _i\}$ are typically used to specify assumptions of the behaviour of an environment, and the implied part $\{\psi _j\}$ is used to specify the requirements to the controller. We assume that every $\varphi _i$ and $\psi _j$ belong to safety-MTL$_{0, \infty }$, being the positive fragment of MITL where all until operators should have only upper bounds, and all release operators can have either upper or lower bound. Still, the safety-MTL$_{0,\infty }$ fragment allows us to express important bounded-response properties, e.g. $\Box (a \rightarrow \Diamond _{\le 1}b)$ that tells that every $a$ should be followed by $b$ within $1$ time unit.

As we show in a number of case-studies such assume-guarantee properties can be used to express many useful real-time specifications; and our implementation can handle these specifications. At the same time this formalism lives close to the edge of undecidability, as e.g. allowing the lower bounds for the until operator makes the synthesis problem undecidable [10]. However, we believe that our approach can be extended to the specifications being arbitrary Boolean combinations of safety-MTL$_{0,\infty }$ formulas (not only implications).

Our approach translates the overall specification $\Psi$ to a network of timed game automata—one automaton for every requirement $\psi _j$ and one automaton for the negation of every assumption $\varphi _i$. A central contribution is the extension of the translation presented in [12], with the advantage that the resulting automata contain no Büchi acceptance conditions and are deterministic by construction. Hence, there is no need for a determinization phase. However, it is not always possible to translate MTL$_{0,\infty }$ properties into language-equivalent deterministic automata,¹ and in this case we produce a deterministic under-approximation. Thus our approach is sound but not complete, i.e. it may fail to generate a strategy even if the specification is realizable. As we shall see, this theoretical incompleteness does not show up in our case studies.

It now remains to use Uppaal-Tiga [5] to synthesize a control strategy for the resulting timed game fulfilling all the requirements $\{\psi _j\}$ or violating at least one of the assumptions $\{\varphi _i\}$. Additionally, the synthesized strategy should avoid generating Zeno behaviour (playing infinite number of actions in a finite amount of time). We do this by either forcing Uppaal-Tigato generate non-Zeno strategy using Büchi winning condition; or by proving that no Zeno strategy will be winning for the controller. Finally, having synthesized a winning strategy, it may be transformed into executable code.

As an illustration, consider the specification:²

$$\begin{aligned} \Box (req \rightarrow \widehat{\Box }_{< 5}\lnot req) \rightarrow \Box (grant \rightarrow \widehat{\Box }_{< 5}\lnot grant) \wedge \Box (req \rightarrow (\lnot req) \widehat{\mathrm{U}}_{\le 5} (grant) ) \end{aligned}$$

This specification says that every request ($req$) should be served ($grant$) within $5$ time-units under the assumption that the environment does not make repeated requests with less than a separation of $5$ time-units. Also, the specification forbids grants to be issued too frequently—again a minimum time-separation of $5$ time-units is required. Figure 1 contains the network of deterministic timed game automata generated by our approach for this specification, together with a winning strategy for this network synthesized by Uppaal-Tiga. Here, the dashed transitions are uncontrollable, and in the strategy the controller always proposes to take the earliest enabled controllable transition. Although some formulas are defined over single actions, the corresponding automata use both actions since $\lnot req$ renders to $grant$ (and the other way round) under the assumption that only these two actions are available.

Fig. 1

Deterministic monitors for $\lnot \Box (req \rightarrow \widehat{\Box }_{< 5}\lnot req), \Box (grant \rightarrow \widehat{\Box }_{< 5}\lnot grant)$ and $\Box (req \rightarrow \lnot req \widehat{\mathrm{U}}_{\le 5} grant)$, and the winning strategy (from left to right)

1.1 Related work

The paper [27] is the first work that proposed the algorithms for the controller synthesis based on timed games. In this work the game rules (i.e. what controller and environment can potentially do) were defined as timed game automata. The winning goals (i.e. what controller should achieve) were expressed as Rabin conditions. This differs from our setup since we use linear-time specifications to define both parts. Later the authors of [13] restricted their attention to timed games with reachability and safety properties. They proposed an efficient symbolic on-the-fly algorithm that has been implemented in the Uppaal-Tiga  tool [5].

The paper [26] was the first work that studied the controller synthesis problem for the case when the specification itself is given as a linear-time temporal formula and a system works in real time. This work proposes an algorithm for the synthesis of the properties of the form $\Box \varphi$, where $\varphi$ is a safety-MITL$_\le$ property that can also contain past formulas. Our approach works well for assume-guarantee properties and it might be hard to fit such properties into the logic of [26]. Additionally, [26] makes the bounded variability assumption, i.e. it assumes that the number of times a signal changes per one time unit is bounded by some known constant $k$. This might be too strict in the dense time setting and we do not make this assumption.

The paper [10] and [17] present a series of decidability and undecidability results for the synthesis and realizability for different fragments of real-time logics MTL, ECL and LTL$_\lhd$. However it is an open question whether the synthesis problem for our fragment of MTL is decidable or not. If we limit the resources of the controller (i.e. the number of clocks it can have and the maximum constants), then the problem is decidable according to [10].

The paper [16] proposes the Safraless procedure for the synthesis of LTL$_\lhd$ properties.

The translation procedure of [16] involves the solution of a timed game with $k^{2^{|\varphi |}}$ locations, where $k$ depends on the specification itself and can be relatively large.

Outline. The rest of the paper is organized as following. Section 2 provides all the necessary definitions. In Sect. 3 we formally state the problem being solved. Section 4 describes the novel translation of safety- and co-safety-MTL$_{0, \infty }$ properties into exact non-deterministic monitoring Timed Automata and under-approximation deterministic Timed Automata. Section 5 describes how we use Uppaal-Tiga  to solve the synthesis games. Section 6 contains the case studies.

2 Definitions and problem statement

2.1 Timed words and $\hbox {MTL}_{0, \infty }$ logic

A timed word over a finite set of actions $\Sigma$ is a finite or infinite sequence of time points and actions $(t_1, a_1)(t_2, a_2)(t_3, a_3)\ldots$, where for every $i$ we have $a_i \in \Sigma , t_i \in \mathbb {R}_{\ge 0}$ and for any non-last $i$ we have $t_{i+1} \ge t_i$. Let $Runs(\Sigma )$ denote the set of all finite timed words over $\Sigma$ and $InfRuns(\Sigma )$ the set of all infinite timed words over $\Sigma$.

A timed word is called Zeno iff it contains infinitely many discrete actions during a finite amount of time. Certainly, the controllers that produce Zeno timed words are not implementable in real life. In our modeling formalism Zeno behavior can also be forced by the environment (if it emits uncontrollable actions infinitely often). In order to distinguish these two situations we define Zeno behavior over sets of actions. A timed word $(t_1, a_1)(t_2, a_2)(t_3, a_3)\ldots$ is called Zeno for $\Sigma ' \subseteq \Sigma$, if it is time-bounded (i.e. $t_i < t$ for some $t$ and for all $i$) and there are infinitely many actions from $\Sigma '$ in it (i.e. for any $j$ there exists $i>j$ such that $a_i \in \Sigma '$). Let $Zeno(\Sigma ')$ denote the set of all infinite timed words that are Zeno for $\Sigma '$.

Definition 1

An MTL$_{0, \infty }$ formula $\varphi$ over actions $\Sigma$ is defined by the grammar

$$\begin{aligned} \varphi {::}= true \,|\, a \,|\,\lnot \varphi \,|\,\varphi _1 \wedge \varphi _2 \,|\, {\bigcirc }\varphi \,|\, \varphi _1 \mathrm{U}_{\sim d}\, \varphi _2 \,|\, \varphi _1 \widehat{\mathrm{U}}_{\sim d}\, \varphi _2 \end{aligned}$$

where $a \in \Sigma , \sim \in \{<, \le , \ge , >\}$ and $d\in \mathbb {N}$.

The common abbreviations are: $false\,=\lnot true, \varphi _1\vee \varphi _2 = \lnot (\lnot \varphi _1 \wedge \lnot \varphi _2), \varphi _1\rightarrow \varphi _2 = (\lnot \varphi _1)\vee \varphi _2, \varphi _1 \mathrm{R}_{\sim d} \,\varphi _2 = \lnot (\lnot \varphi _1 \mathrm{U}_{\sim d} \,\lnot \varphi _2), \varphi _1 \widehat{\mathrm{R}}_{\sim d} \,\varphi _2 = \lnot (\lnot \varphi _1 \widehat{\mathrm{U}}_{\sim d} \,\lnot \varphi _2), \Diamond _{\sim d}\,\varphi = true\,\mathrm{U}_{\sim d} \, \varphi , \widehat{\Diamond }_{\sim d}\,\varphi = true\, \widehat{\mathrm{U}}_{\sim d} \, \varphi , \Box _{\sim d}\,\varphi = false\,\mathrm{R}_{\sim d}\, \varphi$, and $\widehat{\Box }_{\sim d}\,\varphi = false\, \widehat{\mathrm{R}}_{\sim d}\, \varphi$.

The temporal operators $\mathrm{R}$ and $\widehat{\mathrm{R}}$ are called release operators, and $\mathrm{U}$ and $\widehat{\mathrm{U}}$ are called until operators. The release and until operators are called bounded if they have a bound “$< d$” or “$\le d$”, otherwise unbounded. We will omit writing a bound when the bound is “$\ge 0$” (e.g. write $\varphi _1 \mathrm{U}\varphi _2$ instead of $\varphi _1 \mathrm{U}_{\ge 0} \,\varphi _2$).

Safety-MTL$_{0, \infty }$ (co-safety-MTL$_{0, \infty }$) is the fragment of MTL$_{0, \infty }$ that consists of all the formulas in the positive normal form that do not use unbounded until (release, correspondingly) operator [29]. For instance, $\Box \, \Diamond _{\le 1} a$ is in safety-MTL$_{0, \infty }, \Diamond \, \Box _{\le 1} a$ is in co-safety-MTL$_{0, \infty }, \Box _{\le 1}\, \Diamond _{\le 1} a$ is both in safety- and co-safety-MTL$_{0, \infty }, \Box \Diamond a$ is in none of them. It is easy to see that an MTL$_{0, \infty }$-formula $\varphi$ is in safety-MTL$_{0, \infty }$ iff its negation is in co-safety-MTL$_{0, \infty }$.

The semantics of MTL$_{0, \infty }$ is defined over infinite timed words. Let $w^i$ be the $i$-th suffix of the timed word $w$. For a given infinite timed word $w=(t_1, a_1)(t_2, a_2)(t_3, a_3) \ldots$ and an MTL$_{0, \infty }$ formula $\varphi$, the satisfaction relation $w^i\models \varphi$ is defined inductively:

• 1. $w^i \models true$

• 2. $w^i \models a$ iff $a_i = a$

• 3. $w^i \models \lnot \varphi$ iff $w^i \nvDash \varphi$

• 4. $w^i \models {\bigcirc }\varphi$ iff $w^{i+1} \models \varphi$

• 5. $w^i \models \varphi _1 \wedge \varphi _2$ iff $w^i \models \varphi _1$ and $w^i \models \varphi _2$

• 6. $w^i\models \varphi _1 \mathrm{U}_{\sim d}\, \varphi _2$ where $\sim \in \{<, \le , \ge , >\}$ iff there exists $j$ such that $j\ge i, w^j\models \varphi _2, t_j-t_i \sim d$, and $w^k\models \varphi _1$ for all $k$ with $i\le k <j$

• 7. $w^i\models \varphi _1 \widehat{\mathrm{U}}_{\sim d} \,\varphi _2$ where $\sim \in \{<, \le , \ge , >\}$ iff there exists $j$ such that $j > i, w^j\models \varphi _2, t_j-t_i \sim d$, and $w^k\models \varphi _1$ for all $k$ with $i < k <j$

An infinite timed word $w$ satisfies an MTL$_{0, \infty }$-formula $\varphi$ iff $w^1 \models \varphi$. The language ${\mathcal {L}}(\varphi )$ of $\varphi$ is the set of all infinite timed words that satisfy $\varphi$.

2.2 $\hbox {MTL}_{0, \infty }$ synthesis problem

A synthesis problem is defined by a triple $(\varphi , \Sigma _c, \Sigma _u)$, where $\Sigma _c$ and $\Sigma _u$ are disjoint sets of elements (that are called controllable and uncontrollable actions), and $\varphi$ is an MTL$_{0, \infty }$ formula over $\Sigma _c \cup \Sigma _u$. This triple defines the rules of the game between the controller and the environment. The game is played in rounds, and at each round the controller proposes to play some controllable action after some delay, and then the environment can let the controller do this, or it can overtake the controller’s choice with a smaller or equal delay and some uncontrollable action. The behavior of the controller is determined by a strategy, a function that during the course of the game constantly gives information as to what the controller should do in order to satisfy the specification.

More formally, a strategy of the controller in $(\varphi , \Sigma _c, \Sigma _u)$ is a function $f$ that maps the finite timed words from $Runs(\Sigma _c \cup \Sigma _u)$ to the pairs $(\tau , a)$, where $\tau \in \mathbb {R}_{\ge 0}$ and $a \in \Sigma _c$. An infinite timed word $(t_1, a_1)(t_2, a_2)(t_3, a_3)\ldots$ is consistent with the strategy $f$, if for any $i$, if $f((t_1, a_1)(t_2, a_2)\ldots (t_i, a_i)) = (\tau , a)$, then either $(\tau , a) = (t_{i+1}-t_i, a_{i+1})$, or $a_{i+1} \in \Sigma _u$ and $t_{i+1} - t_i \le \tau$. Let $Outcomes(f, \Sigma _c, \Sigma _u) \subseteq InfRuns(\Sigma _c \cup \Sigma _u)$ be the set of all infinite timed words over $\Sigma _c \cup \Sigma _u$ that are consistent with the strategy $f$.

Since the synthesis games are played in dense real time, we should prevent the controller from blocking time by using the Zeno strategies. We assume that a Zeno run is losing for the controller iff there are infinitely many uncontrollable actions among it (i.e. the controller does not block time by itself). This means that if the environment emits infinitely many actions among a finite amount of time, then it loses even if the controller also emits infinitely many actions.

We come to the following definition:

Definition 2

A controller’s strategy $f$ is called a solution for the synthesis problem $(\varphi , \Sigma _c, \Sigma _u)$, iff for any run $\omega \in Outcomes(f, \Sigma _c, \Sigma _u){\setminus } Zeno(\Sigma _u)$ we have $\omega \in ({\mathcal {L}}(\varphi ){\setminus } Zeno(\Sigma _c))$

Obviously, for the practical application of the automatic synthesis method, a controller’s strategy should be implementable and thus it should have a finite representation. In the current paper we assume that a strategy in the synthesis problem is defined by a deterministic Timed Automata, i.e. a controller has finitely many clocks that can record time passed since some events, and finitely many control states that define the reaction to the input events.

2.3 Timed automata

Let $X$ be a set of real-valued variables called clocks. A clock bound over $X$ has the form $x \sim n$ where $x \in X, \sim \in \{<,\le ,\ge , >\}$ and $n \in \mathbb {Z}_{\ge 0}$. We denote the set of all possible clock bounds over $X$ by $\mathcal {B}(X)$, and $\mathcal {F}(X)$ is the set of all Boolean formulas over $\mathcal {B}(X)$ (including conjunctions and disjunctions). A valuation over $X$ is a an element of $\mathbb {R}^X_{\ge 0}$, i.e. it is a function $v: X \rightarrow \mathbb {R}_{\ge 0}$. We let $\overline{0}$ be the valuation that assigns $0$ to any clock from $X$. For a given valuation $v$, clock set $Y \subseteq X$ and real number $\tau \in \mathbb {R}_{\ge 0}$ we let $v+\tau$ to be the valuation such that $(v+\tau )(x) = v(x) + \tau$ for every clock $x \in X$; and $v[Y]$ is equal to the valuation such that $v[Y](x) = 0$ if $x \in Y$ and $v[Y](x) = v(x)$ otherwise.

Definition 3

[2] A Timed Automaton (TA) over actions $\Sigma$ is a tuple $(L, l_0, X, E)$ where:

• $L$ is a finite set of locations,

• $l_0$ is the initial location,

• $X$ is a finite set of clocks,

• $E \subseteq L \times \Sigma \times \mathcal {F}(X) \times 2^{|X|} \times L$ is the finite set of edges.

The semantics of TA is defined by Labeled Transition System (LTS) $(S, s_0, \rightarrow )$. A set of states $L \times \mathbb {R}^X_{\ge 0}$ of a TA consists of pairs of locations and valuations over $X$. The initial state is $(l_0, \overline{0})$. There exists a delay transition $(l, v_1) \xrightarrow {\tau } (l, v_2)$, iff $\tau \in \mathbb {R}_{\ge 0}$ and $v_2 = v_1 + \tau$. There exists a discrete transition $(l_1, v_1) \xrightarrow {a} (l_2, v_2)$ if there exists a transition $(l_1, a, g, Y, l_2)$ such that $v_1 \models g$ and $v_2 = v_1[Y]$. In the latter case we say that a transition $e$ is enabled in the state $(l_1, v_1)$.

A TA is called total for a set of actions $\Sigma ' \subseteq \Sigma$ if for any action $a \in \Sigma '$ and for any state $s \in S$ there exists at least one state $s'$ such that $s \xrightarrow {a} s'$. A TA is called deterministic iff not more than one such state $s'$ exists for any pair of $s$ and $a$.

A run of a TA is an infinite sequence of alternating delay and discrete transitions $s_0 \xrightarrow {\tau _1} s_1 \xrightarrow {a_1} s_2 \xrightarrow {\tau _2} \cdots$.

A timed word $w=(t_1, a_1)(t_2, a_2)(t_3, a_3) \ldots$ over $\Sigma$ is accepted by timed automaton $A$ iff there is an infinite sequence of states $s_0,s_1, s_2, \ldots$ such that $s_0$ is the initial state of $A$ and $s_0 \xrightarrow {\tau _1} s_1 \xrightarrow {a_1} s_2 \xrightarrow {\tau _2} \ldots$ is a run of $A$, where $\tau _i = t_i - t_{i-1}$ for every $i>1$ and $t_1 = \tau _1$. We use ${\mathcal {L}}(A)$ to denote the set of all timed words that are accepted by $A$.

We use TA to define synthesis game arenas (where both players have freedom to choose time delays and actions); and to define the controller’s winning strategies in which the controller always takes the earliest enabled controllable transition. The latter TA define winning strategies in the synthesis problems as the following:

Definition 4

Let $(\varphi , \Sigma _c, \Sigma _u)$ be a synthesis problem and let $A$ be a total for $\Sigma _u$ and deterministic TA. We say that $A$ implements the strategy $f_A$ in $(\varphi , \Sigma _c, \Sigma _u)$ defined in the following way. Let $\omega =(t_1, a_1)(t_2, a_2) \ldots (t_n, a_n)$ be an arbitrary finite timed word over $\Sigma _c \cup \Sigma _u$. Let $s_0 \xrightarrow {\tau _1} s_1 \xrightarrow {a_1} s_2 \ldots s_{2n}$ be a unique run of $A$ on $\omega$. Let $\tau _{n+1}$ be the minimal delay such that there exist transitions $s_{2n} \xrightarrow {\tau _{n+1}} s_{2n+1}$ and $s_{2n+1} \xrightarrow {a_{n+1}} s_{2n+2}$ for some controllable action $a_{n+1} \in \Sigma _c$. Then we define the value of the strategy $f_A$ on $\omega$ as $f_A(\omega ) = (\tau _{n+1}, a_{n+1})$.

3 Problem statement

Consider the sets $\Sigma _c$ and $\Sigma _u$ of controllable and uncontrollable actions. Consider an MTL$_{0, \infty }$ property $\varphi$ over $\Sigma _c \cup \Sigma _u$ such that

$$\begin{aligned} \Psi \equiv \varphi _1 \wedge \varphi _2 \wedge \cdots \wedge \varphi _n \rightarrow \psi _1 \wedge \psi _2 \wedge \cdots \wedge \psi _m \end{aligned}$$

where all $\varphi _i$ and $\psi _j$ are safety-MTL$_{0, \infty }$ properties. Our goal is to construct a TA $A$ such that $A$ implements a solution $f_A$ for the synthesis problem $(\Psi , \Sigma _c, \Sigma _u)$.

4 From safety- and co-safety-$\hbox {MTL}_{0, \infty }$ to Timed Automata

In our paper [12] we presented a procedure to translate MITL$_\le$ formulas, the bounded fragment of MTL$_{0, \infty }$, into Timed Automata. For a given formula, the procedure can build language-equivalent nondeterministic timed automata, as well as deterministic under- and over-approximations.

In the current work we will extend the procedure of [12] to the case of safety and co-safety MTL$_{0, \infty }$. Basically, we use the classical tableau-based translation from linear-time temporal formulas into Büchi automata, with two important modifications. First, we avoid using Büchi acceptance condition because we consider safety and co-safety fragments of MTL$_{0, \infty }$ on non-Zeno runs only (e.g. we cannot express $\Box \Diamond a$ that certainly needs Büchi acceptance condition). Second, in order to handle timed properties, we introduce an auxiliary clock for each subformula of the form $\varphi _1 \mathrm{U}_{\sim d} \,\varphi _2, \varphi _1 \mathrm{R}_{\sim d} \,\varphi _2, \varphi _1 \widehat{{\mathrm{U}}}_{\sim d} \,\varphi _2$ or $\varphi _1 \widehat{{\mathrm{R}}}_{\sim d} \,\varphi _2$(where $\sim \in \{<, \le , \ge , >\}$ and ${\sim }d$ is not $\ge 0$). When a timed formula, for example, $\varphi _1 \mathrm{U}_{\le d} \,\varphi _2$ is expected to be satisfied, the automaton will reset the corresponding clock $x$, rewrite this formula into $\varphi _1 \mathrm{U}_{\le d-x} \, \varphi _2$ and in future observations compare the value of $x$ with $d$, and check if the promise $\varphi _1 \mathrm{U}_{\le d-x} \,\varphi _2$ has been fulfilled within the time bound.

In the rest of this section, we assume that $\varphi$ is an MTL$_{0, \infty }$ formula over $\Sigma$ and has been transformed into positive normal form, where the negation operator ($\lnot$) is not allowed ($\lnot true$ is replaced by $false$ and $\lnot a$ is replaced by $\bigvee _{b\in \Sigma {\setminus }\{a\}} b$ when $a$ is an action in $\Sigma$). For the sake of simplicity, we also make an assumption that all temporal operators occurring in $\varphi$ are included in $\{\mathrm{U}_{\le d}, \mathrm{R}_{\le d}, \mathrm{U}_{\ge d},\mathrm{R}_{\ge d}\}$.

4.1 Closures and extended formulas

We use Sub($\varphi$) to denote all the sub-formulas of $\varphi$. For each $\varphi _1 \mathrm{U}_{\le d} \,\varphi _2 \in$ Sub($\varphi$), we assign a clock $x_{(\varphi _1 \mathrm{U}_{\le d} \,\varphi _2)}$ to it. Let $X_{U\le }$ be the set of all $\mathrm{U}_{\le d}$-clocks, i.e. $\{x_{(\varphi _1 \mathrm{U}_{\le d} \varphi _2)}$ $|$ $\varphi _1 \mathrm{U}_{\le d} \,\varphi _2 \in \hbox {Sub}(\varphi )\}$. Similarly we assign the clocks to the other until and release operators, and define $X_{U\ge }, X_{R\le }$ and $X_{R\ge }$. We do not assign clocks to formulas $\varphi _1\mathrm{U}\varphi _2$ and $\varphi _1\mathrm{R}\varphi _2$, therefore we always assume that $d>0$ when we write $\mathrm{U}_{\ge d}$ or $\mathrm{R}_{\ge d}$ in this section.

The set of basic formulas for $\varphi$, written as BF($\varphi$), is a finite set defined by the following rules:

• 1. If ${\bigcirc }\varphi _1 \in$ Sub($\varphi$), then $\varphi _1 \in$ BF($\varphi$)

• 2. If $\varphi _1 \mathrm{U}\varphi _2 \in$ Sub($\varphi$) or $\varphi _1 \mathrm{U}_{\ge d} \,\varphi _2 \in$ Sub($\varphi$), then $\varphi _1 \mathrm{U}\varphi _2 \in$ BF($\varphi$)

• 3. If $\varphi _1 \mathrm{R}\varphi _2 \in$ Sub($\varphi$) or $\varphi _1 \mathrm{R}_{\ge d} \, \varphi _2 \in$ Sub($\varphi$), then $\varphi _1 \mathrm{R}\varphi _2 \in$ BF($\varphi$)

• 4. If $\varphi _1 \mathrm{U}_{\sim d} \,\varphi _2 \in$ Sub($\varphi$) and $x$ is the clock assigned to $\varphi _1 \mathrm{U}_{\sim d} \,\varphi _2$, then $\varphi _1 \mathrm{U}_{\sim d-x} \,\varphi _2, x \sim d \in$ BF($\varphi$), where $\sim \in \{\le , \ge \}$.

• 5. If $\varphi _1 \mathrm{R}_{\sim d} \, \varphi _2 \in$ Sub($\varphi$) and $x$ is the clock assigned to $\varphi _1 \mathrm{R}_{\sim d} \,\varphi _2$, then $\varphi _1 \mathrm{R}_{\sim d-x} \,\varphi _2, \overline{x \sim d} \in$ BF($\varphi$), where $\sim \in \{\le , \ge \}$ and $\overline{x \sim d}$ is the negation of $x \sim d$ (for example, $\overline{x \le d}= x>d$ and $\overline{x \ge d}= x<d$)

The meaning of $\mathrm{U}_{\le d-x}, \mathrm{U}_{\le d-x}, \mathrm{R}_{\le d-x}$ and $\mathrm{R}_{\ge d-x}$ will be given in Definition 5.

Since a conjunction of basic formulas can be regarded as a subset of BF($\varphi$), for simplicity, we use $2^{\hbox {BF}(\varphi )}$ for the set of all subsets of BF($\varphi$) as well as the set of all conjunctive formulas over BF($\varphi$). Because a conjunction with zero conjuncts is true, so $true\in 2^{\hbox {BF}(\varphi )}$.

We define CL($\varphi$), the closure of $\varphi$, to be the set of all positive Boolean combinations (i.e., without negation) over BF($\varphi$). Obviously, CL($\varphi$) has only finitely many different non-equivalent formulas.

For a clock $x \in X_{\mathrm{U}\ge }\cup X_{\mathrm{R}\le }$, we use rst $(x)$ to represent that $x$ will be reset at the current step. Similarly, for $x \in X_{\mathrm{U}\le }\cup X_{\mathrm{R}\ge }$, we use unch $(x)$ to represent that $x$ will not be reset at the current step. Now we defined Ext($\varphi$), the set of extended formulas for $\varphi$, with the following rules:

• 1. Sub($\varphi$) $\subseteq$ Ext($\varphi$)

• 2. If $\phi \in$ CL($\varphi$), then $\phi , {\bigcirc }\phi \in$ Ext($\varphi$)

• 3. If $x \in X_{\mathrm{U}\le }$ or $x \in X_{\mathrm{R}\ge }$, then $unch(x) \in$ Ext($\varphi$)

• 4. If $x \in X_{\mathrm{U}\ge }$ or $x \in X_{\mathrm{R}\le }$, then $rst(x) \in$ Ext($\varphi$)

• 5. If $x\sim d \in$ BF($\varphi$), then $\overline{x \sim d} \in$ Ext($\varphi$)

• 6. If $\varPhi _1, \varPhi _2 \in$ Ext($\varphi$), then $\varPhi _1 \wedge \varPhi _2, \varPhi _1 \vee \varPhi _2 \in$ Ext($\varphi$)

Extended formulas can be interpreted over extended timed words. An extended timed word $\omega = ( t_1,a_1, v_1 )( t_2,a_2, v_2)(t_3,a_3, v_3) \ldots$ is a sequence where $w\!=\!( t_1,a_1),( t_2,a_2)(t_3,a_3) \ldots$ is a timed word over $\Sigma$, and for every $i \in \mathbb {N}, v_i$ is a clock valuation over $X$=$X_{U\le } \cup X_{U\ge }\cup X_{R\le }\cup X_{R\ge }$ such that for each $x\in X$, either $v_{i+1}(x)=v_{i}(x)+t_{i+1}-t_{i}$ or $v_{i+1}(x)=t_{i+1}-t_{i}$.

The semantics for extended formulas is naturally induced by the semantics of MTL$_{0, \infty }$ formulas:

Definition 5

Let $\omega = ( t_1,a_1, v_1 )( t_2,a_2, v_2)(t_3,a_3, v_3) \ldots$ be an extended timed word and $\varPhi \in$ Ext($\varphi$). The satisfaction relation $\omega ^i\models _e \varPhi$ is inductively defined as follows:

• 1. $\omega ^i \models _e x\sim d$ iff $v_i(x)\sim d$, where $\sim \in \{<, \le , >, \ge \}$.

• 2. $\omega ^i \models _e rst(x)$ iff $v_{i+1}(x)=t_{i+1}-t_{i}$

• 3. $\omega ^i \models _e unch(x)$ iff $v_{i+1}(x)=v_{i}(x)+t_{i+1}-t_{i}$

• 4. $\omega ^i \models _e \phi$ iff $w^i\models \phi$, if $\phi \in$ Sub($\varphi$)

• 5. $\omega ^i \models _e \varphi _1 \mathrm{U}_{\sim d-x} \varphi _2$ iff there exists $j$ such that $j\ge i, w^j\models \varphi _2, t_j-t_i \sim d-v_{i}(x)$, and $w^k\models \varphi _1$ for all $k$ with $i\le k <j$, where $\sim \in \{\le , \ge \}$.

• 6. $\omega ^i \models _e \varphi _1 \mathrm{R}_{\sim d-x} \varphi _2$ iff for all $j\ge i$ such that $t_j-t_i \sim d-v_{i}(x)$, either $w^j\models \varphi _2$ or there exists $k$ with $i \le k <j$ and $w^k\models \varphi _1$, where $\sim \in \{\le , \ge \}$.

• 7. $\omega ^i \models _e \varPhi _1 \wedge \varPhi _2$ iff $\omega ^i \models _e \varPhi _1$ and $\omega ^i \models _e \varPhi _2$

• 8. $\omega ^i \models _e \varPhi _1 \vee \varPhi _2$ iff $\omega ^i \models _e \varPhi _1$ or $\omega ^i \models _e \varPhi _2$

• 9. $\omega ^i \models _e {\bigcirc }\varPhi$ iff $\omega ^{i+1} \models _e \varPhi$

$\omega ^i$ is a model of $\varPhi$ if $\omega ^i \models _e \varPhi$. Two extended formulas are said to be equivalent if they have exactly the same models.

4.2 Constructing non-deterministic automata

Let us show how we construct a timed automaton $\mathbb {A}_\varphi =(L, l_0, X, \mathbb {E})$ for $\varphi$. $L$ is defined to be $\{\varphi \}\cup 2^{\hbox {BF}(\varphi )}, l_0$ is $\varphi$, and $X$ is $X_{\mathrm{U}\le } \cup X_{\mathrm{U}\ge }\cup X_{\mathrm{R}\le }\cup X_{\mathrm{R}\ge }$.

For each $\psi \in L$, we will define how to compute the set of outgoing transitions from $\psi$. The core of the computation is a rewriting function $\beta$ that tells what formula should be satisfied in the next observation and which clocks should be reset when we see this observation. $\beta$ is defined inductively for all formulas in Sub$(\varphi )\cup \hbox {CL}\,(\varphi$), as follows.

• 1. $\beta (\varphi _1\, \mathrm{U}\, \varphi _2) = \beta (\varphi _2) \vee (\beta (\varphi _1) \wedge {\bigcirc }( \varphi _1 \,\mathrm{U}\, \varphi _2 ))$

• 2. $\beta (\varphi _1\, \mathrm{U}_{\le d}\, \varphi _2)$ = $\beta (\varphi _2) \vee (\beta (\varphi _1) \wedge {\bigcirc }( (x \le d) \wedge (\varphi _1 \,\mathrm{U}_{\le d-x} \,\varphi _2 )))$, where $x$ is the clock assigned to $\varphi _1 \,\mathrm{U}_{\le d} \,\varphi _2$

• 3. $\beta (\varphi _1\, \mathrm{U}_{\le d-x}\, \varphi _2)$ = $\beta (\varphi _2) \vee (\beta (\varphi _1) \wedge unch(x) \wedge {\bigcirc }((x \le d) \wedge (\varphi _1 \,U_{\le d-x} \,\varphi _2 )))$

• 4. $\beta (\varphi _1\, \mathrm{U}_{\ge d} \,\varphi _2)$ = $\beta (\varphi _1) \wedge rst(x) \wedge {\bigcirc }( ( \varphi _1 \,\mathrm{U}_{\ge d-x} \,\varphi _2 ) \vee ((x \ge d) \wedge (\varphi _1\, \mathrm{U}\, \varphi _2)))$, where $x$ is the clock assigned to $\varphi _1 \,\mathrm{U}_{\ge d} \,\varphi _2$

• 5. $\beta (\varphi _1\, \mathrm{U}_{\ge d-x}\, \varphi _2)$ = $\beta (\varphi _1)\wedge {\bigcirc }( ( \varphi _1 \mathrm{U}_{\ge d-x} \,\varphi _2 ) \vee ((x \ge d) \wedge (\varphi _1 \mathrm{U}\, \varphi _2)))$

• 6. $\beta (\varphi _1 \,\mathrm{R}\,\varphi _2)$= $\beta (\varphi _2) \wedge ( \beta (\varphi _1) \vee {\bigcirc }( \varphi _1 \,\mathrm{R}\,\varphi _2))$

• 7. $\beta (\varphi _1 \,\mathrm{R}_{\le d} \,\varphi _2)= \beta (\varphi _2) \wedge ( \beta (\varphi _1) \vee \hbox {rst}(x) \wedge {\bigcirc }( ( \varphi _1 \,\mathrm{R}_{\le d-x} \,\varphi _2) \vee (x > d)))$ , where $x$ is the clock assigned to $\varphi _1 \,\mathrm{R}_{\le d} \,\varphi _2$

• 8. $\beta (\varphi _1 \,\mathrm{R}_{\le d-x} \,\varphi _2)= \beta (\varphi _2) \wedge ( \beta (\varphi _1) \vee {\bigcirc }(( \varphi _1 \,\mathrm{R}_{\le d-x} \, \varphi _2) \vee (x > d)))$

• 9. $\beta (\varphi _1\, \mathrm{R}_{\ge d}\, \varphi _2)$ = $\beta (\varphi _1) \vee {\bigcirc }(((x < d) \wedge (\varphi _1 \,\mathrm{R}_{\ge d-x} \,\varphi _2)) \vee (\varphi _1 \,\mathrm{R}\,\varphi _2))$, where $x$ is the clock assigned to $\varphi _1 \mathrm{R}_{\ge d} \,\varphi _2$

• 10. $\beta (\varphi _1\, \mathrm{R}_{\ge d-x}\, \varphi _2)$ = $\beta (\varphi _1) \vee ( unch(x) \wedge {\bigcirc }(((x < d) \wedge (\varphi _1 \,\mathrm{R}_{\ge d-x} \,\varphi _2)) \vee ( \varphi _1 \,\mathrm{R}\,\varphi _2)))$

• 11. $\beta (\varphi _1 \wedge \varphi _2) = \beta (\varphi _1) \wedge \beta (\varphi _2)$

• 12. $\beta (\varphi _1 \vee \varphi _2) = \beta (\varphi _1) \vee \beta (\varphi _2)$

• 13. $\beta ({\bigcirc }\varphi _1)= {\bigcirc }(\varphi _1)$

• 14. $\beta (\varphi _1) = \varphi _1$, if $\varphi _1$ is an action or a clock bound

• 15. $\beta (true) = true$

• 16. $\beta (false) = false$.

It is obvious that $\beta (\psi )$ is an extended formula in Ext($\varphi$).

From the semantics given in Sect. 2 for MTL$_{0, \infty }$, we know that $(\bigvee _{a\in \Sigma } a) \equiv true$ and for any $a, b \in \Sigma$, if $a\ne b$, then $a \wedge b \equiv false$. Using these facts and that ${\bigcirc }$ distributes over disjunction and conjunction, we can show by induction that $\beta (\psi )$ can be transformed equivalently into a disjunction of the following form:

$$\begin{aligned} \bigvee ^k_{j=1} \big ( a_j \wedge g_j \wedge rst(X_j) \wedge unch(Y_j) \wedge {\bigcirc }(\psi _j)\big ) \end{aligned}$$

where for every $j$ between 1 and $k$: $a_j\in \Sigma$ is an action, $g_j$ is a conjunction of clock bounds, $X_j \subseteq (X_{\mathrm{U}\ge }\cup \,X_{\mathrm{R}\le })$ and $Y_j \subseteq (X_{\mathrm{U}\le }\cup \, X_{\mathrm{R}\ge }), \psi _j \in 2^{\mathrm{BF}(\varphi )}, rst(X_j)$ is the abbreviation of $\bigwedge _{x \in X_j}rst(x)$ and $unch(Y_j)$ is the abbreviation of $\bigwedge _{x \in Y_j}unch(x)$.

We call each $a_j \wedge g_j \wedge rst(X_j) \wedge unch(Y_j) \wedge {\bigcirc }(\psi _j)$ a basic conjunction of $\beta (\psi )$.

From each basic conjunction $a_j \wedge g_j \wedge rst(X_j) \wedge unch(Y_j) \wedge {\bigcirc }(\psi _j)$, we can define a group of transitions from $\psi$ to $\psi _j$:

$$\begin{aligned} (\psi , a_j, g_j, r, \psi _j) \in \mathbb {E}\quad \,\, iff \, X_j \subseteq r \subseteq (X {\setminus } Y_j) \end{aligned}$$

Theorem 1

Let $\varphi$ be a safety MTL$_{0, \infty }$ formula over $\Sigma$, and $\mathbb {A}_\varphi$ be a TA for $\varphi$ built according to the procedure given above. Then ${\mathcal {L}}(\mathbb {A}_\varphi ){\setminus } Zeno(\Sigma ) = {\mathcal {L}}(\varphi ){\setminus }Zeno(\Sigma )$.

Theorem 2

Let $\varphi$ be a co-safety MTL$_{0, \infty }$ formula over $\Sigma$, and $\mathbb {A}_\varphi$ be a TA for $\varphi$ built according to the procedure given above. Then ${\mathcal {L}}_{reach}(\mathbb {A}_\varphi , \{ true \}){\setminus }Zeno(\Sigma ) = {\mathcal {L}}(\varphi ){\setminus }Zeno(\Sigma )$, where ${\mathcal {L}}_{reach}(\mathbb {A}_\varphi , \{ true \})$ denotes the timed words that are accepted by a run that eventually reaches the location $true$(that is, the empty subset of $\hbox {BF}(\varphi ))$.

4.3 Proofs for Theorem 1 and Theorem 2

In this subsection we will provide proofs for Theorem 1 and Theorem 2. The following two lemmas proves the validity of the rewrite rules.

Lemma 1

Let $\omega$ be an extended timed word and $\psi \in Sub(\varphi ) \cup CL(\varphi )$. If $\omega \models _e \beta (\psi )$, then $\omega \models _e \psi$.

Proof

We prove this by induction on the structure of $\psi$.

• 1. If $\psi$ is an action or a clock bound, then $\beta (\psi )=\psi$ and the conclusion is true.

• 2. Assume that the conclusion is true for all sub-formulas of $\psi$.

• Case 1. $\psi =\psi _1 \wedge \psi _2$: Since $\beta (\psi )=\beta (\psi _1) \wedge \beta (\psi _2)$, it is easy to see that the conclusion is true for $\psi$.

• Case 2. $\psi =\varphi _1 U_{\le d} \,\varphi _2$:

• 1. If $\omega \models _e \beta (\varphi _2)$, then $\omega \models _e \varphi _2$, and so $\omega \models _e \varphi _1 U_{\le d} \, \varphi _2$.

• 2. If $\omega \nvDash _e \beta (\varphi _2)$, then from $\omega \models _e \beta (\psi )$ and $\beta (\psi )$= $\beta (\varphi _2) \vee (\beta (\varphi _1) \wedge {\bigcirc }( (x \le d) \wedge (\varphi _1 \,\mathrm{U}_{\le d-x} \,\varphi _2 )))$, we know that $\omega \models _e \beta (\varphi _1) \wedge {\bigcirc }( (x \le d) \wedge (\varphi _1 \,\mathrm{U}_{\le d-x} \, \varphi _2 ))$. Hence $\omega \models _e \beta (\varphi _1)$ and $\omega \models _e {\bigcirc }( (x \le d) \wedge (\varphi _1 \,\mathrm{U}_{\le d-x} \,\varphi _2 ))$. From the induction assumption we get that $\omega \models _e \varphi _1$. From $\omega \models _e \varphi _1$ and $\omega \models _e {\bigcirc }( (x \le d) \wedge (\varphi _1 \,\mathrm{U}_{\le d-x} \, \varphi _2 )))$ we then get the conclusion that $\omega \models _e \varphi _1 U_{\le d} \,\varphi _2$.

The proofs for the rest of the cases are similar and are omitted here. $\square$

Definition 6

Given a timed word $w=(t_1,a_1),( t_2,a_2)(t_3,a_3) \ldots$ and a clock valuation $v_1=\overline{0}$, an extended timed word $\overline{w}=( t_1,a_1, v_1 )( t_2,a_2, v_2)(t_3,a_3, v_3)\ldots$ can be defined inductively as follows:

• 1. If $x$ is the clock assigned to $\varphi _1\mathrm{U}_{\le d}\,\varphi _2 \in$ Sub($\varphi$), then

  $$\begin{aligned} v_{i+1}(x)= {\left\{ \begin{array}{ll} v_i(x)+t_{i+1}-t_i, &{}\text {if}\, v_i(x)\le d, w^i \models \varphi _1 \mathrm{U}_{\le d-v_i(x)}\,\varphi _2\hbox { and }w^i \nvDash \varphi _2;\\ t_{i+1}-t_i, &{}\text {otherwise.} \end{array}\right. } \end{aligned}$$

• 2. If $x$ is the clock assigned to $\varphi _1\mathrm{U}_{\ge d}\,\varphi _2 \in$ Sub($\varphi$), then

  $$\begin{aligned} v_{i+1}(x)= {\left\{ \begin{array}{ll} t_{i+1}-t_i, &{}\text {if}\, w^i \models \varphi _1 \mathrm{U}_{\ge d}\,\varphi _2;\\ v_i(x)+t_{i+1}-t_i, &{}\text {otherwise.} \end{array}\right. } \end{aligned}$$

• 3. If $x$ is the clock assigned to $\varphi _1\mathrm{R}_{\le d}\,\varphi _2 \in$ Sub($\varphi$), then

  $$\begin{aligned} v_{i+1}(x)= {\left\{ \begin{array}{ll} t_{i+1}-t_i, &{}\text {if} w^i \models \varphi _1 \mathrm{R}_{\le d}\,\varphi _2\hbox { and }w^i\nvDash \varphi _1;\\ v_i(x)+t_{i+1}-t_i, &{}\text {otherwise.} \end{array}\right. } \end{aligned}$$

• 4. If $x$ is the clock assigned to $\varphi _1\mathrm{R}_{\ge d}\,\varphi _2 \in$ Sub($\varphi$), then

  $$\begin{aligned} v_{i+1}(x)= {\left\{ \begin{array}{ll} v_i(x)+t_{i+1}-t_i, &{}\text {if}\, v_i(x)<d, w^i \models \varphi _1 \mathrm{R}_{\ge d-v_i(x)}\,\varphi _2 \hbox { and }w^i \nvDash \varphi _1;\\ t_{i+1}-t_i, &{}\text {otherwise.} \end{array}\right. } \end{aligned}$$

Lemma 2

Let $w$ be a timed word, and $\overline{w}$ be the extended timed word defined in Definition 6, then for every $\psi \in Sub(\varphi )\cup CL(\varphi )$, if $\overline{w} \models _e \psi$ then $\overline{w} \models _e \beta (\psi )$.

Proof

By induction on $\psi$. $\square$

Lemma 3

For each $\psi \in Sub(\varphi ) \cup CL(\varphi ), \beta (\psi )$ can be transformed equivalently into a disjunction of basic conjunctions:

$$\begin{aligned} \bigvee ^k_{j=1} \big ( a_j \wedge g_j \wedge rst(X_j) \wedge unch(Y_j) \wedge {\bigcirc }(\psi _j)\big ) \end{aligned}$$

where for each $j$ between 1 and $k: a_j\in \Sigma , g_j$ is a conjunction of clock bounds, $X_j \subseteq (X_{\mathrm{U}\ge }\cup \, X_{\mathrm{R}\le }), Y_j \subseteq (X_{\mathrm{U}\le }\cup \, X_{\mathrm{R}\ge })$, and $\psi _j \in 2^{\mathrm{BF}(\varphi )}$.

Proof

We first define Length($\psi$) for each $\psi \in Sub(\varphi ) \cup CL(\varphi )$ as follows.

• 1. Length$(true)=0$;

• 2. Length$(false)=0$;

• 3. Length$(\psi _1)=0$, if $\psi _1$ is an action or a clock bound;

• 4. Length$({\bigcirc }\psi _1)=0$;

• 5. Length$(\psi _1 op \psi _2)=$ Length$(\psi _1)$+ Length$(\psi _2)+1$, where $op$ is an operator in the set $\{ \wedge , \vee , \mathrm{U}, \mathrm{U}_{\le d}, \mathrm{U}_{\ge d}, \mathrm{U}_{\le d-x}, \mathrm{U}_{\ge d-x}, \mathrm{R}, \mathrm{R}_{\le d}, \mathrm{R}_{\ge d}, \mathrm{R}_{\le d-x}, \mathrm{R}_{\ge d-x} \}$.

Now we prove the conclusion by induction on Length($\psi$).

• 1. Since $\beta (true)$ = $true \equiv \bigvee _{a\in \Sigma } a \equiv \bigvee _{a\in \Sigma } \big ( a \wedge {\bigcirc }(true) \big )$, the conclusion is true for the case of $\psi =true$.

• 2. Since $\beta (false)$ = $false$ is the disjunction of zero disjuncts, the conclusion is also true for the case of $\psi =false$.

• 3. If $\psi =a$, and $a$ is an action, then $\beta (\psi )$ = $a \,\equiv \, (a \wedge {\bigcirc }(true) )$, and the conclusion is true for the case of $\psi =a$.

• 4. If $\psi$ is a clock bound $x\sim d$, then $\beta (\psi )$ = $(x\sim d)\,\equiv \, \bigvee _{a\in \Sigma } \big ( a \wedge (x\sim d) \wedge {\bigcirc }(true) \big )$. So the conclusion is true for $\psi$ = $(x\sim d)$.

• 5. If $\psi ={\bigcirc }\psi _1$, then $\beta (\psi )$ = ${\bigcirc }(\psi _1) \,\equiv \, \bigvee _{a\in \Sigma } \big ( a \wedge {\bigcirc }(\psi _1) \big )$. So the conclusion is true for this case.

• 6. If $\psi =\varphi _1 \wedge \varphi _2$, then $\beta (\psi ) = \beta (\varphi _1) \wedge \beta (\varphi _2)$. By the induction assumption, we have that

  $$\begin{aligned} \beta (\varphi _1)\equiv \bigvee ^{k_1}_{i=1} \big ( a'_i \wedge g'_i \wedge rst(X'_i) \wedge unch(Y'_i) \wedge {\bigcirc }(\psi '_i)\big ) \end{aligned}$$

  and

  $$\begin{aligned} \beta (\varphi _2) \equiv \bigvee ^{k_2}_{j=1} \big ( a''_j \wedge g''_j \wedge rst(X''_j) \wedge unch(Y''_j) \wedge {\bigcirc }(\psi ''_j)\big ), \end{aligned}$$

  then

  $$\begin{aligned} \beta (\psi ) \equiv \bigvee ^{k_1}_{i=1} \bigvee ^{k_2}_{j=1} \big ( (a'_i \wedge a''_j)\!\wedge \!(g'_i \!\wedge \! g''_j ) \wedge rst(X'_i\cup X''_j) \wedge unch(Y'_i \cup Y''_j) \!\wedge \! {\bigcirc }(\psi '_i\!\wedge \!\psi ''_j) \big ) \end{aligned}$$

  Since $a'_i \wedge a''_j$ is either equals to $a'_i$ or $false$, it can be concluded that the conclusion is true for the case of $\psi =\varphi _1 \wedge \varphi _2$.

• 7. The other cases can be proved similarly. $\square$

Now let us begin to prove the Theorem 1.

Proof of Theorem 1

1. ${\mathcal {L}}(\mathbb {A}_\varphi ){\setminus }Zeno(\Sigma ) \subseteq {\mathcal {L}}(\varphi ){\setminus }Zeno(\Sigma )$.

Let $w=(t_1,a_1),( t_2,a_2),(t_3,a_3) \ldots$ be a non-Zeno timed word in ${\mathcal {L}}(\mathbb {A}_\varphi )$, then there exist $\psi _1, \psi _2, \psi _3, \ldots \in L, (\psi _1, a_1, g_1, r_1, \psi _2), (\psi _2, a_2, g_2, r_2, \psi _3), \ldots \in \mathbb {E}$ and $v_1, v_2, v_3, \ldots \in \mathbb {R}^X_{\ge 0}$ such that $\psi _1=\varphi$, and for each $i\ge 1$: there are $X_i \subseteq (X_{\mathrm{U}\ge }\cup \,X_{\mathrm{R}\le })$ and $Y_i \subseteq (X_{\mathrm{U}\le }\cup \, X_{\mathrm{R}\ge } )$ such that $a_i \wedge g_i \wedge rst (X_i) \wedge unch(Y_i)\wedge {\bigcirc }(\psi _{i+1})$ is a basic conjunction of $\beta (\psi _i), X_i \subseteq r_i \subseteq (X{\setminus }Y_i), v_i\models g_i$, and $v_{i+1}=(v_i[r_i]) + (t_{i+1}-t_i)$.

Then we get an extended timed word $\omega = (t_1,a_1,v_1), (t_2,a_2,v_2), (t_3,a_3,v_3),\ldots$, and $\omega ^i \models _e$ $a_i \wedge g_i \wedge rst (X_i) \wedge unch(Y_i)$.

For each $i\ge 1$, using $\omega ^i$ and $\psi _{i+1}$, we can define an assignment $\mu _i(\psi )\in \{true, false\}$ for all extended formulas in Ext($\varphi$) as follows.

• 1. For each $a\in \Sigma , \mu _i(a)=true$ iff $a=a_i$

• 2. $\mu _i(x\sim d)=true$ iff $v_i(x) \sim d$

• 3. $\mu _i(rst(x))=true$ iff $v_{i+1}(x)=t_{i+1}-t_{i}$.

• 4. $\mu _i(unch(x))=true$ iff $v_{i+1}(x)=v_{i}(x)+t_{i+1}-t_{i}$

• 5. For each $\varphi _1\in \hbox {BF}(\varphi ), \mu _i({\bigcirc }(\varphi _1))=true$ iff $\varphi _1 \in \psi _{i+1}$ ( please noted that $\psi _{i+1}$ is a subset of BF($\varphi$))

• 6. $\mu _i(\varphi _1 \wedge \varphi _2 )=\mu _i(\varphi _1 ) \wedge \mu _i(\varphi _2 )$

• 7. $\mu _i(\varphi _1 \vee \varphi _2 )=\mu _i(\varphi _1 ) \vee \mu _i(\varphi _2 )$

• 8. $\mu _i(\varphi _1\, \mathrm{R}\, \varphi _2)$= $\mu _i(\varphi _2) \wedge ( \mu _i(\varphi _1) \vee \mu _i( {\bigcirc }( \varphi _1 \,\mathrm{R}\,\varphi _2)))$

• 9. $\mu _i(\varphi _1 \,\mathrm{R}_{\le d} \,\varphi _2)$ = $\mu _i(\varphi _2) \wedge ( \mu _i(\varphi _1) \vee \mu _i( \hbox {rst}(x)) \wedge ( \mu _i ({\bigcirc }(\varphi _1 \,\mathrm{R}_{\le d-x} \varphi _2)) \vee \mu _i({\bigcirc }(x > d))))$, where $x$ is the clock assigned to $\varphi _1 \,\mathrm{R}_{\le d} \,\varphi _2$

• 10. The other cases for $\mu _i(\varphi _1\, \mathrm{U}_{\le d}\, \varphi _2), \mu _i(\varphi _1\, \mathrm{U}_{\le d-x}\, \varphi _2), \mu _i(\varphi _1\, \mathrm{R}_{\le d-x}\, \varphi _2)$ can be defined similarly, accordig to the rewriting rules in Sect. 4.2.

It is easy to show that if $a\wedge g \wedge \text {rst}(X_1)\wedge \text {unch}(Y_1)\wedge {\bigcirc }(\psi ')$ is a basic conjunction of $\beta (\psi )$, and $\mu _i(a\wedge g \wedge \text {rst}(X_1)\wedge \text {unch}(Y_1)\wedge {\bigcirc }(\psi '))$ is true, then $\mu _i(\psi )$ is true.

Thus for each $i\ge 1$, we get that $\mu _i(\psi _i)=true$, and furthermore, for each basic formula $\psi \in \psi _i$, we have $\mu _i(\psi )=true$.

Now we show that for each $\psi \in$ Sub($\varphi$)$\cup$ CL($\varphi$), if $\mu _i(\psi )=true$, then $\omega ^i \models _e \psi$.

• 1. If $\psi$ is an action or a clock bound, the conclusion is obviously true.

• 2. If $\psi ={\bigcirc }(\phi )$, and $\mu _i(\psi )=true$,

  then $\phi \in \psi _{i+1}$, and $\mu _{i+1}(\phi )=true$.

  By induction, we get that $\omega ^{i+1} \models _e \phi$. So $\omega ^{i} \models _e {\bigcirc }(\phi )$.

• 3. If $\psi =\phi _1 \wedge \phi _2$ and $\mu _i(\psi )=true$, then $\mu _i(\phi _1)=\mu _i(\phi _2)=true$. By induction, we get that $\omega ^i \models _e \phi _1$ and $\omega ^i \models _e \phi _2$. Thus we get the conclusion that $\omega ^i \models _e \phi _1 \wedge \phi _2$.

• 4. If $\psi =\phi _1 \vee \phi _2$ and $\mu _i(\psi )=true$, then $\mu _i(\phi _1)=true$ or $\mu _i(\phi _2)=true$. By induction, we get that $\omega ^i \models _e \phi _1$ or $\omega ^i \models _e \phi _2$. Thus $\omega ^i \models _e \phi _1 \vee \phi _2$.

• 5. If $\psi =\phi _1 \mathrm{R}\phi _2$ and $\mu _i(\psi )=true$, then $\mu _i(\varphi _2) \wedge ( \mu _i(\varphi _1) \vee \mu _i( {\bigcirc }( \varphi _1 \,\mathrm{R}\,\varphi _2)))$ is true.

Thus we get that $\mu _i(\varphi _2)=true$, and that $\mu _i(\varphi _1)=true$ or $\varphi _1 \,\mathrm{R}\,\varphi _2 \in \psi _{i+1}$.

By induction, we get that $\omega ^i \models _e \varphi _2, \omega ^i \models _e \varphi _1$ or $\varphi _1 \,\mathrm{R}\,\varphi _2 \in \psi _{i+1}$.

• Case 1. If $\omega ^i \models _e \varphi _2$ and $\omega ^i \models _e \varphi _1$, then $\omega ^i \models _e \phi _1 \mathrm{R}\phi _2$, and the conclusion is true.

• Case 2. If $\omega ^i \models _e \varphi _2$ and $\varphi _1 \,\mathrm{R}\,\varphi _2 \in \psi _{i+1}$, then from $\varphi _1 \,\mathrm{R}\,\varphi _2 \in \psi _{i+1}$ we know that $\mu _{i+1}(\varphi _1 \,\mathrm{R}\,\varphi _2)=true$, thus $\mu _{i+1}(\varphi _2)=true$, and $\mu _{i+1}(\varphi _1)=true$ or $\varphi _1 \,\mathrm{R}\,\varphi _2 \in \psi _{i+2}$.

By induction, we have that $\omega ^{i+1} \models _e \varphi _2, \omega ^{i+1} \models _e \varphi _1$ or $\varphi _1 \,\mathrm{R}\,\varphi _2 \in \psi _{i+2}$.

• (2.1) If $\omega ^{i+1} \models _e \varphi _2$ and $\omega ^{i+1} \models _e \varphi _1$, then from the fact that $\omega ^i \models _e \varphi _2$, we know that $\omega ^i \models _e \phi _1 \mathrm{R}\phi _2$. So the conclusion is true.

• (2.2) If $\omega ^{i+1} \models _e \varphi _2$ and $\varphi _1 \,\mathrm{R}\,\varphi _2 \in \psi _{i+2}$, then we know that $\mu _{i+2}(\varphi _1 \,\mathrm{R}\,\varphi _2)=true$.

Thus $\mu _{i+2}(\varphi _2)=true$, and $\mu _{i+2}(\varphi _1)=true$ or $\varphi _1 \,\mathrm{R}\,\varphi _2 \in \psi _{i+3}$.

By induction, we get that $\omega ^{i+2} \models _e \varphi _2, \omega ^{i+2} \models _e \varphi _1$ or $\varphi _1 \,\mathrm{R}\,\varphi _2 \in \psi _{i+3}$.

This procedure can stop or proceed infinitely; in both case, we could get that $\omega ^i \models _e \phi _1 \mathrm{R}\phi _2$.

• 6. We omit the proofs for the other cases.

Since $\mu _1(\varphi )=true$, from the above conclusion we get that $\omega ^1 \models _e \varphi$, thus we finish the proof for ${\mathcal {L}}(\mathbb {A}_\varphi ){\setminus }Zeno(\Sigma ) \subseteq {\mathcal {L}}(\varphi ){\setminus }Zeno(\Sigma )$.

2. ${\mathcal {L}}(\varphi ){\setminus }Zeno(\Sigma )\subseteq {\mathcal {L}}(\mathbb {A}_\varphi ){\setminus }Zeno(\Sigma )$.

Let $w=(t_1,a_1),( t_2,a_2),(t_3,a_3) \ldots$ be a non-Zeno timed word in ${\mathcal {L}}(\varphi )$ and $\overline{w}$=$( t_1,a_1, v_1 )( t_2,a_2, v_2)(t_3,a_3, v_3)\ldots$ be the extended timed word defined in Definition 6.

From $w \in {\mathcal {L}}(\varphi )$, we know that $\overline{w}\models _e \varphi$.

Let $\varphi _{1}=\varphi$, then by Lemma 2, we get that $\overline{w}\models _e \beta (\varphi _{1})$. Since $\beta (\varphi _{1})$ can be written as a disjunction of some basic conjunctions, so there is a basic conjunction $\alpha _1 \wedge g_1 \wedge rst (X_1) \wedge unch(Y_1)\wedge {\bigcirc }(\varphi _{2})$ of $\varphi _1$ such that $\overline{w}\models _e \alpha _1 \wedge g_1 \wedge rst (X_1) \wedge unch(Y_1)\wedge {\bigcirc }(\varphi _{2})$.

Thus $\alpha _1=a_1, v_1 \models g_1$, and $\overline{w}\models _e rst (X_1) \wedge unch(Y_1)$, and $\overline{w^2}\models _e \varphi _{2}$.

Let $r_1$=$\{x\, |\, x \in X{\setminus }Y_1, and v_2(x)=t_{2}-t_1 \}$, then $X_1 \subseteq r_1 \subseteq (X{\setminus }Y_1)$.

So from the construction in Sect. 4.2, $(\varphi _1, a_1, g_1, r_1, \varphi _2) \in \mathbb {E}$ is a transition of $\mathbb {A}_\varphi , \overline{w}^2 \models \varphi _{2}$, and $v_2=v_1[r_1]+(t_2-t_1)$.

Similarly, from $\overline{w}^2 \models _e \varphi _{2}$, by Lemma 2, we know that there is a basic conjunction $\alpha _2 \wedge g_2 \wedge rst (X_2) \wedge unch(Y_2)\wedge {\bigcirc }(\varphi _{3})$ of $\varphi _2$ such that $\overline{w^2}\models _e \alpha _2 \wedge g_2 \wedge rst (X_2) \wedge unch(Y_2)\wedge {\bigcirc }(\varphi _{3})$.

Thus $\alpha _2=a_2, v_2 \models g_2$, and $\overline{w^2}\models _e rst (X_2) \wedge unch(Y_2)$, and $\overline{w^3}\models _e \varphi _{3}$.

Let $r_2$=$\{x\, |\, x \in X{\setminus }Y_2$, and $v_3(x)=t_{3}-t_2 \}$, then $X_2 \subseteq r_2 \subseteq (X{\setminus }Y_2)$.

Thus $(\varphi _2,a_2, g_2, r_2,\varphi _3 )\in \mathbb {E}$ is a transition of $\mathbb {A}_\varphi , \overline{w}^3 \models _e \varphi _{3}$, and $v_3=v_2[r_2]+(t_3-t_2)$.

By repeating above reasoning, we can get a run of $\mathbb {A}_\varphi$ that accepts $w=(t_1,a_1),( t_2,a_2),$ $(t_3,a_3) \ldots$. This completes our proof for Theorem 1. $\square$

Now we turn to the proof for Theorem 2.

Proof of Theorem 2

1. ${\mathcal {L}}_{reach}(\mathbb {A}_\varphi , \{true\}){\setminus }Zeno(\Sigma ) \subseteq {\mathcal {L}}(\varphi ){\setminus }Zeno(\Sigma )$

Let $w=(t_1,a_1), ( t_2,a_2), (t_3,a_3) \ldots$ be a non-Zeno timed word in ${\mathcal {L}}_{reach}(\mathbb {A}_\varphi , \{true\})$, then there are $\psi _1, \psi _2, \psi _3, \ldots \in L$ and $v_1, v_2, v_3, \ldots \in \mathbb {R}^X_{\ge 0}$ such that $\psi _1=\varphi , (\psi _i,a_i, g_i, r_i,\psi _{i+1} ) \in \mathbb {E}$ is a transition of $\mathbb {A}_\varphi$, and $a_i \wedge g_i \wedge rst (X_i) \wedge unch(Y_i)\wedge {\bigcirc }(\psi _{i+1})$ is a basic conjunction of $\beta (\psi _i), X_i \subseteq r_i \subseteq (X {\setminus }Y_i), v_i\models g_i$, and $v_{i+1}=(v_i[r_i]) + (t_{i+1}-t_i)$.

Then we get an extended timed word $\omega = (t_1,a_1,v_1), (t_2,a_2,v_2), (t_3,a_3,v_3),\ldots$, and $\omega ^i \models _e$ $a_i \wedge g_i \wedge rst (X_i) \wedge unch(Y_i)$.

Because $\psi _1, \psi _2, \psi _3, \ldots$ could reach the location $true$, we can assume that $\psi _n = true$.

Now we prove by induction that for all $i\le n$: $\omega ^i\models _e \psi _i$.

• 1. If $i=n$, then $\psi _n=true$ and $\omega ^n\models _e \psi _n$.

• 2. Assume $\omega ^i \models _e \psi _i$ is true for all $i\ge k+1$, now we show that $\omega ^k\models _e \psi _k$ is true. From $(\psi _k,a_k, g_k, r_k, \psi _{k+1}) \in \mathbb {E}$, we know that $\omega ^k \models _e a_k \wedge g_k \wedge rst (X_k) \wedge unch(Y_k)\wedge {\bigcirc }(\psi _{k+1})$, so $\omega ^k \models _e \beta (\psi _k)$.

Then from Lemma 1, we get the conclusion that $\omega ^k \models _e \psi _k$.

2. ${\mathcal {L}}(\varphi ){\setminus }Zeno(\Sigma ) \subseteq {\mathcal {L}}_{reach}(\mathbb {A}_\varphi , \{true\}){\setminus }Zeno(\Sigma )$.

Let $w=(t_1,a_1),( t_2,a_2),(t_3,a_3) \ldots$ be a non-Zeno timed word in ${\mathcal {L}}(\varphi )$ and $\overline{w}$=$( t_1,a_1, v_1 )( t_2,a_2, v_2)(t_3,a_3, v_3)\ldots$ be the extended timed word defined in Definition 6.

From $w \in {\mathcal {L}}(\varphi )$, we know that $\overline{w}\models _e \varphi$.

Let $\varphi _{1}=\varphi$, there is a basic conjunction $\alpha _1 \wedge g_1 \wedge rst (X_1) \wedge unch(Y_1)\wedge {\bigcirc }(\varphi _{2})$ of $\varphi _1$ such that $\overline{w}\models \alpha _1 \wedge g_1 \wedge rst (X_1) \wedge unch(Y_1)\wedge {\bigcirc }(\varphi _{2})$.

Then $\alpha _1=a_1, v_1 \models g_1$, and $\overline{w}\models rst (X_1) \wedge unch(Y_1)$, and $\overline{w}^2\models \varphi _{2}$.

Let $r_1$=$\{x\, |\, x \in (X{\setminus }Y_1), and v_2(x)=t_{2}-t_1 \}$, then $X_1 \subseteq r_1 \subseteq (X{\setminus }Y_1)$.

So from the construction in Section 3.2, $(\varphi _1,a_1, g_1, r_1,\varphi _2)\in \mathbb {E}$ is a transition of $\mathbb {A}_\varphi , \overline{w}^2 \models \varphi _{2}$, and $v_{2}=(v_1[r_1]) + (t_2-t_1)$.

Similarly, we can get a sequence $\varphi _2,\varphi _{3},\varphi _{4}, \ldots$ of formulas from $2^{\mathrm{BF}(\varphi )}$ such that $(\varphi _i, a_i, g_i, r_i, \varphi _{i+1}) \in \mathbb {E}$ is a transition of $\mathbb {A}_\varphi$ and $\overline{w}_i\models a_i \wedge g_i \wedge rst (X_i) \wedge unch(Y_i)\wedge {\bigcirc }(\varphi _{i+1})$ for all $i\in N$.

Now, it suffices to prove that there exists some $k$ such that $\varphi _{k}=true$.

To do this, we define the depth dep($\phi$) for formulas in Sub($\varphi$)$\cup 2^{\mathrm{BF}(\varphi )}$.

• 1. $\hbox {dep}(a)$ = $\hbox {dep}(x\sim d)$ = $\hbox {dep}(true)$ = $0$;

• 2. $\hbox {dep}(\phi _1 \vee \phi _2 )$ = $\hbox {dep}(\phi _1 \wedge \phi _2 )$ = $\hbox {max} \{ \hbox {dep}(\phi _1), \hbox {dep}(\phi _2) \}$;

• 3. $\hbox {dep}({\bigcirc }\phi )$ = $\hbox {dep}(\phi _1)+1$;

• 4. $\hbox {dep}(\phi _1\, \mathrm{U}_{\le d}\,\phi _2)$ = $\hbox {dep}(\phi _1\, \mathrm{R}_{\le d}\, \phi _2)$ = $\hbox {max}\{\hbox {dep}(\phi _1), \hbox {dep}(\phi _2)\}+2$;

• 5. $\hbox {dep}(\phi _1\, \mathrm{U}_{\ge d}\,\phi _2)$ = $\hbox {max}\{\hbox {dep}(\phi _1),\hbox {dep}(\phi _2)\}+3$;

• 6. $\hbox {dep}(\phi _1\, \mathrm{U}_{\ge d-x}\,\phi _2)$ = $\hbox {max}\{\hbox {dep}(\phi _1), \hbox {dep}(\phi _2)\}+2$;

• 7. $\hbox {dep}(\phi _1\, \mathrm{U}\,\phi _2)$ = $\hbox {max}\{\hbox {dep}(\phi _1), \hbox {dep}(\phi _2)\}+1$;

• 8. $\hbox {dep}(\phi _1\, \mathrm{U}_{\le d-x}\,\phi _2)$ = $\hbox {dep}(\phi _1\, \mathrm{R}_{\le d-x}\,\phi _2)$ = $\hbox {max}\{\hbox {dep}(\phi _1), \hbox {dep}(\phi _2)\}+1$.

Then dep($\varphi _1$) $\ge$ dep($\varphi _2$) $\ge$ dep($\varphi _3)\ge \ldots$, and there exists $N$ such that for all $i\ge N$: dep($\varphi _i$) $=$ dep($\varphi _N$).

If dep($\varphi _N$) $>0$, then some $\phi _1\, \mathrm{U}_{\le d-x}\,\phi _2$ , $\phi _1\, \mathrm{R}_{\le d-x}\,\phi _2, \phi _1\, \mathrm{U}_{\ge d-x}\,\phi _2$ or $\phi _1\, \mathrm{U}\,\phi _2$ will remain in $\varphi _i$ for all $i\ge N$.

• 1. If $\phi _1\, \mathrm{U}_{\le d-x}\,\phi _2$, or $\phi _1\, \mathrm{R}_{\le d-x}\,\phi _2$, or $\phi _1\, \mathrm{U}_{\ge d-x}$ is remain in $\varphi _i$ for all $i\ge N$, then we get that $x$ will not be reset and will not exceed $d$. This is not possible, because the extended timed word $\overline{w}$ is assumed to be non-Zeno.

• 2. If $\phi _1\, \mathrm{U}\,\phi _2$ is remain in $\varphi _i$ for all $i\ge N$, then $\overline{w}^i\models \phi _1\, \mathrm{U}\,\phi _2$ will be true for all $i\ge N$, and $\overline{w}^i\models \phi _2$ is false for all $i\ge N$. This is also not possible!

Thus dep($\varphi _N$) must be zero, so $\varphi _{N+1}=true$ and $w \in {\mathcal {L}}_{reach}(\mathbb {A}_\varphi , \{true\}){\setminus } Zeno(\Sigma )$.   $\square$

4.4 Reducing the transitions in $\mathbb {A}_\varphi$

Given a basic conjunction $a \wedge g \wedge rst(X_1) \wedge unch(Y_1) \wedge {\bigcirc }(\psi _1)$, its sub-formula $rst(X_1)\wedge unch(Y_1)$ tells us that the clocks in $X_1$ should be reset and the clocks in $Y_1$ should not be reset. It does not tell us the other clocks in $X{\setminus }(X_1\cup Y_1)$ should be reset or not be reset. So in the construction of Sect. 4.2 we enumerate all the possible situations for clocks in $X{\setminus }(X_1\cup Y_1)$, and thus we get a group of transitions from a basic conjunction. In this subsection, we will show that it is not necessary to enumerate all possible combinations for clocks in $X{\setminus }(X_1\cup Y_1)$, there exists a best choice, that is, to reset all clocks in $(X_{\mathrm{U}\le }\cup \, X_{\mathrm{R}\ge }){\setminus }Y_1$ to zero and keep all clocks in $(X_{\mathrm{U}\ge }\cup \,X_{\mathrm{R}\le }){\setminus }X_1$ unchanged. The idea behind this choice is that each clock $x \in (X_{\mathrm{U}\le }\cup \, X_{\mathrm{R}\ge })$ should be reset to zero unless $unch(x)$ is asked to be true, and each clock $x \in (X_{\mathrm{U}\ge }\cup \,X_{\mathrm{R}\le })$ should not be reset unless $rst(x)$ is asked to be true. In this way, for a given basic conjunction $a \wedge g \wedge rst(X_1) \wedge unch(Y_1) \wedge {\bigcirc }(\psi _1)$ of $\beta (\psi )$, then transition $(\psi , a, g, \lambda , \psi _1)$ with $\lambda =(X_1\cup ((X_{U\le }\cup \, X_{R\ge }){\setminus }Y_1))$ will be the unique transition from $\psi$ to $\psi _1$ in the following construction.

Definition 7

Let $\varphi$ be an MTL$_{0, \infty }$ formula over $\Sigma$, we can define a timed automaton $\mathcal {A}_\varphi$= $(L, l_0, X, E )$ for $\varphi$ as follows.

• $L$ = $\{\varphi \}\cup 2^{\mathrm{BF}(\varphi )}$ is the set of locations, and $l_0=\varphi$ is the initial location;

• $X$ = $X_{\mathrm{U}\le } \cup X_{\mathrm{U}\ge }\cup X_{\mathrm{R}\le }\cup X_{\mathrm{R}\ge }$ is the set of all clocks.

• $(\psi _1, a, g, \lambda , \psi _2)\in E$ iff there exist $X_1 \subseteq X_{\mathrm{U}\ge }\cup X_{\mathrm{R}\le }$ and $Y_1 \subseteq X_{\mathrm{U}\le }\cup X_{\mathrm{R}\ge }$ such that $a \wedge g \wedge rst(X_1) \wedge unch(Y_1) \wedge {\bigcirc }(\psi _2)$ is a basic conjunction of $\beta (\psi _1)$ and $\lambda =(X_1\cup ((X_{U\le }\cup X_{R\ge }){\setminus }Y_1))$.

Theorem 3

Let $\varphi$ be a safety MTL$_{0, \infty }$ formula over $\Sigma$, then ${\mathcal {L}}(\mathcal {A}_\varphi ){\setminus }Zeno(\Sigma ) = {\mathcal {L}}(\mathbb {A}_\varphi ){\setminus }Zeno(\Sigma )$.

Proof

It suffices to prove that ${\mathcal {L}}(\mathbb {A}_\varphi ){\setminus } Zeno(\Sigma ) \subseteq {\mathcal {L}}(\mathcal {A}_\varphi ){\setminus } Zeno(\Sigma )$.

Let $w=(t_1,a_1),( t_2,a_2),(t_3,a_3) \ldots$ be a non-Zeno timed word in ${\mathcal {L}}(\mathbb {A}_\varphi )$, then there exist $\psi _1, \psi _2, \psi _3, \ldots \in L, (\psi _1, a_1, g_1, r_1, \psi _2), (\psi _2, a_2, g_2, r_2, \psi _3),\ldots \in \mathbb {E}$ and $v_1, v_2, v_3, \ldots \in \mathbb {R}^X_{\ge 0}$ such that $\psi _1=\varphi$, and for each $i\ge 1$: there are $X_i \subseteq X_{\mathrm{U}\ge }\cup X_{\mathrm{R}\le }$ and $Y_i \subseteq X_{\mathrm{U}\le }\cup X_{\mathrm{R}\ge }$ such that $a_i \wedge g_i \wedge rst (X_i) \wedge unch(Y_i)\wedge {\bigcirc }(\psi _{i+1})$ is a basic conjunction of $\beta (\psi _i), X_i \subseteq r_i \subseteq X{\setminus }Y_i, v_i\models g_i$, and $v_{i+1}=(v_i[r_i]) + (t_{i+1}-t_i)$.

For each $i\ge 1$, let $\lambda _i=(X_i\cup ((X_{U\le }\cup X_{R\ge }){\setminus }Y_i))$, then $(\psi _i, a_i, g_i, \lambda _i, \psi _{i+1})\in E$ is a transition in $\mathcal {A}_\varphi$.

We define $v'_1, v'_2, v'_3, \ldots \in \mathbb {R}^X_{\ge 0}$ inductively as follows:

$v'_1=v_1, v'_2=v'_1[\lambda _1] +(t_2-t_1), \ldots , v'_{i+1}= (v'_i[\lambda _i]) + (t_{i+1}-t_i),\ldots$.

Then by induction on $i$ we can prove that the following Assertion 1 is true. $\square$

Assertion 1

For each $i\ge 1$ and $x\in X$, if $x\in X_{\mathrm{U}\ge }\cup X_{\mathrm{R}\le }$ then $v_i(x)\le v'_i(x)$; otherwise, $v_i(x)\ge v'_i(x)$.

From the rewrite rules in Sect. 4.2, it is easy to find that the following Assertion 2 is also true.

Assertion 2

For each $x\in X$, if $x\in X_{\mathrm{U}\ge }\cup X_{\mathrm{R}\le }$, then $x>d$ and $x\ge d$ will not occur in $g_i$; otherwise, $x<d$ and $x\le d$ will not occur in $g_i$.

From Assertion 1, Assertion 2 and $v_i\models g_i$, we can conclude that $v'_i\models g_i$. Thus $(\psi _1, \overline{0})\xrightarrow {t_1}(\psi _1, v'_1)\xrightarrow {a_1}(\psi _2, v'_1[\lambda _1])\xrightarrow {t_2-t_1} (\psi _2, v'_2) \xrightarrow {a_2}(\psi _3, v'_2[\lambda _2])\xrightarrow {t_3-t_2} (\psi _3, v'_3)\ldots$ will be a run of $\mathcal {A}_\varphi$ that accepts the timed word $w=(t_1,a_1), ( t_2,a_2), (t_3,a_3) \ldots$. This completes our proof.

Theorem 4

Let $\varphi$ be a co-safety MTL$_{0, \infty }$ formula over $\Sigma$, then ${\mathcal {L}}_{reach}(\mathcal {A}_\varphi , \{true\}){\setminus } Zeno(\Sigma )$ $= {\mathcal {L}}_{reach}(\mathbb {A}_\varphi , \{true\}){\setminus } Zeno(\Sigma )$.

Theorem 4 can be proved similarly as Theorem 3.

Example. Let $\Sigma =\{a, b\}$ and $F=(\Diamond _{\ge 1} a) \vee \Box _{\le 2}b$, then

$$\begin{aligned} \beta (F)&= (rst(x_0) \wedge {\bigcirc }(F_1 \vee F_2 )) \vee (b \wedge rst(x_1)\wedge {\bigcirc }(F_3 \vee F_4) )\\&= (a\wedge rst(x_0) \wedge {\bigcirc }F_1 ) \vee (a\wedge rst(x_0) \wedge {\bigcirc }F_2) \\&\vee (b\wedge rst(x_0) \wedge {\bigcirc }F_1) \vee (b\wedge rst(x_0) \wedge {\bigcirc }F_2) \\&\vee (b \wedge rst(x_1)\wedge {\bigcirc }F_3) \vee (b \wedge rst(x_1)\wedge {\bigcirc }F_4 ), \end{aligned}$$

where $F_1=\Diamond _{\ge 1-x_0}a, F_2=(x_0\ge 1) \wedge \Diamond a, F_3=(\Box _{\le 2-x_1}b )$ and $F_4=(x_1>2)$.

So $F$ has 6 outgoing transitions: $(F, a, true, \{x_0\}, F_1)$, $(F, a, true, \{x_0\}, F_2)$, $(F, b, true,$ $\{x_0\}, F_1), (F, b, true, \{x_0\}, F_2), (F, b, true, \{x_1\}, F_3), (F, b, true, \{x_1\}, F_4)$. Similarly, we can continues compute the outgoing transitions for $F_1, F_2$, etc. The whole timed automaton constructed for $F$ is presented in Fig. 2.

Fig. 2

A timed automaton for $(\Diamond _{\ge 1} a) \vee \Box _{\le 2}b$

4.5 Constructing deterministic under-approximation automata

The construction in Definition 7 might produce non-deterministic automata. In fact, as stated earlier, there exist MTL$_{0, \infty }$-formulas for which no equivalent deterministic timed automaton exists. However, if $\varphi$ is a safety or co-safety MTL $_{0, \infty }$-formula, then we can construct a deterministic under-approximation timed automaton $\mathcal {A}^u_\varphi$ for $\varphi$ with the construction that we already presented in [12].

The basic idea behind this construction is the classical subset construction from NFA to DFA. The deterministic timed automaton $\mathcal {A}^u_\varphi$ is constructed from non-deterministic automaton $\mathbb {A}_\varphi$ (Sect. 4.2) with the subset-construction technique. Each state in $\mathcal {A}^u_\varphi$ is a subset of the states in $\mathbb {A}_\varphi$, and each transition of $\mathcal {A}^u_\varphi$ can be regarded as a collection of several transitions from $\mathbb {A}_\varphi$.

• 1. The initial location of $\mathcal {A}^u_\varphi$ is $\varphi$, the other locations of $\mathcal {A}^u_\varphi$ are formulas from CL($\varphi$).

• 2. The actions of $\mathcal {A}^u_\varphi$ are same as that of $\varphi$.

• 3. The clocks of $\mathcal {A}^u_\varphi$ are the set $X$ defined for $\varphi$ in Sect. 4.1.

• 4. Let $\psi$ be a formula in $\{\varphi \}\cup \hbox {CL}(\varphi )$. To define the outgoing transitions from $\psi$, we further translate $\beta (\psi )$ in disjunctive form into the following deterministic form by repeated use of the logical equivalence $p \Leftrightarrow (p\wedge q) \vee (p\wedge \lnot q)$.

  $$\begin{aligned} F_\psi = \bigvee _{i=1}^n \big ( a_i \wedge g_i \wedge \bigvee _{k=1}^{m_i} (rst(X_{ik}) \wedge unch(Y_{ik}) \wedge {\bigcirc }(\psi _{ik}) ) \big ) \end{aligned}$$

where for all $i\in \{1,\ldots , n\}$: $a_i\in \Sigma$ is an action, $g_i$ is a conjunction of clock bounds, $m_i$ is a positive integer, $X_{ik} \subseteq X_{U\ge }\cup X_{R\le }$ and $Y_{ik} \subseteq X_{U\le }\cup X_{R\ge }$ are sets of clocks, $\psi _{ik} \in$ CL($\varphi$), and for all $i\ne j$: $a_i\ne a_j$ or $g_i \wedge g_j$ is false.

Using the facts that ${\bigcirc }$ distributes over $\vee$, and $rst(Y)$ and $unch(Y)$ are monotonic in $Y$, the following formula $F^u_\psi$ is an under-approximation of $F_\psi$:

$$\begin{aligned} F^u_\psi&= \bigvee _{i=1}^n \big ( a_i \wedge g_i \wedge rst(\bigcup _{k=1}^{m_i} X_{ik}) \wedge unch(\bigcup _{k=1}^{m_i} Y_{ik}) \wedge {\bigcirc }(\bigvee _{k=1}^{m_i} \psi _{ik}) \big ) \end{aligned}$$

Then $\psi$ has $n$ outgoing transitions in $\mathcal {A}^u_\varphi$, that is, $\{ (\psi , a_i, g_i, (\bigcup _{k=1}^{m_i} X_{ik}) \cup ((X_{U\le }\cup X_{R\ge }){\setminus }(\bigcup _{k=1}^{m_i} Y_{ik} ) ) , \bigvee _{k=1}^{m_i}\psi _{ik} ) \,\, |\, \, 1\le i\le n \}$. We use Tran($\mathcal {A}^u_\varphi$) to denote the set of all transitions in $\mathcal {A}^u_\varphi$.

Please noted that each $a_i \wedge g_i \wedge rst(X_{ik}) \wedge unch(Y_{ik}) \wedge {\bigcirc }(\psi _{ik})$ is a basic conjunction of $\beta (\psi )$, so each transition in $\mathcal {A}^u_\varphi$ can be considered as a collection of several transitions from the automaton $\mathbb {A}_\varphi$ (Sect. 4.2). Now we show that every timed word accepted by $\mathcal {A}^u_\varphi$ is also accepted by $\mathbb {A}_\varphi$.

Theorem 5

Let $\varphi$ be a safety MTL$_{0, \infty }$ formula over $\Sigma$, then ${\mathcal {L}}(\mathcal {A}^u_\varphi ){\setminus }Zeno(\Sigma ) \subseteq {\mathcal {L}}(\mathbb {A}_\varphi ){\setminus }Zeno(\Sigma )$.

Proof

Let $w=(t_1,a_1),( t_2,a_2),(t_3,a_3) \ldots$ be a non-Zeno timed word in ${\mathcal {L}}(\mathcal {A}^u_\varphi )$, then there exist $\psi _1, \psi _2, \psi _3, \ldots \in \{\varphi \}\cup \hbox {CL}(\varphi ), (\psi _1, a_1, g_1, r_1, \psi _2), (\psi _2, a_2, g_2, r_2, \psi _3),\ldots \in \,$Tran($\mathcal {A}^u_\varphi$), and $v_1, v_2, v_3, \ldots \in \mathbb {R}^X_{\ge 0}$ such that $\psi _1=\varphi$, and for each $i\ge 1$: $v_i\models g_i$, and $v_{i+1}=(v_i[r_i]) + (t_{i+1}-t_i)$.

For each $i\ge 1$, since $(\psi _i, a_i, g_i, r_i, \psi _{i+1})$ is a transition of $\mathcal {A}^u_\varphi$, there exist $X_{i1}, X_{i2}, \ldots , X_{im_i} \in 2^{X_{U\ge }\cup X_{R\le }}, Y_{i1}, Y_{i2}, \ldots , Y_{im_i} \in 2^{X_{U\le }\cup X_{R\ge }}$, and $\psi _{i1}, \psi _{i2}, \ldots , \psi _{im_i} \in 2^{\mathrm{BF}(\varphi )}$ such that

$r_i=(\bigcup _{k=1}^{m_i} X_{ik}) \cup ((X_{U\le }\cup X_{R\ge }){\setminus }(\bigcup _{k=1}^{m_i} Y_{ik} )), \psi _{i+1}=\bigvee _{k=1}^{m_i}\psi _{ik}$, and for every $k\in \{1, 2, \ldots , m_i \}$: $a_i \wedge g_i \wedge rst(X_{ik}) \wedge unch(Y_{ik}) \wedge {\bigcirc }(\psi _{ik})$ is a basic conjunction of $\beta (\psi _{i})$.

Now we can defined an infinite tree $\mathcal {T}$ using the formulas from $\{\varphi \}\cup 2^{\mathrm{BF}(\varphi )}$ as follows.

• 1. $(0,\varphi )$ is the root of $\mathcal {T}$.

• 2. For each $i\ge 1$ and $k\in \{1, 2, \ldots , m_i \}, (i,\psi _{ik} )$ is a node at level $i$.

• 3. For each $i\ge 2$ and $k\in \{1, 2, \ldots , m_i \}$, since $a_i \wedge g_i \wedge rst(X_{ik}) \wedge unch(Y_{ik}) \wedge {\bigcirc }(\psi _{ik})$ is a basic conjunction of $\beta (\psi _{i})$ and $\psi _{i}=\bigvee _{k=1}^{m_{(i-1)}}\psi _{(i-1)k}$, then there exists a $n_i$ such that $1\le n_i \le m_{(i-1)}$ and $a_i \wedge g_i \wedge rst(X_{ik}) \wedge unch(Y_{ik}) \wedge {\bigcirc }(\psi _{ik})$ is a basic conjunction of $\beta (\psi _{(i-1)n_i})$. We define $(i-1, \psi _{(i-1)n_i})$ to be the only parent of $(i, \psi _{ik})$.

Since $\mathcal {T}$ is an infinite tree, by König’s Lemma, $\mathcal {T}$ has an infinite branch $(0,\varphi )$ $(1,\psi _{1l_1})$ $(2,\psi _{2l_2})$ $\ldots$. Because $a_i \wedge g_i \wedge rst(X_{il_i}) \wedge unch(Y_{il_i}) \wedge {\bigcirc }(\psi _{il_i})$ is a basic conjunction of $\beta (\psi _{(i-1)l_{(i-1)}})$ and $X_{il_i} \subseteq r_i \subseteq (X{\setminus }Y_{il_i})$, thus $(\psi _{(i-1)l_{(i-1)}}, a_i, g_i, r_i, \psi _{il_i} )$ is a transition of $\mathbb {A}_\varphi$. Then from the fact that $v_i\models g_i$ and $v_{i+1}=(v_i[r_i]) + (t_{i+1}-t_i)$, we know that $(\varphi , \overline{0}) \xrightarrow {t_1} (\varphi , v_1)\xrightarrow {a_1} (\psi _{1l_1}, v_1[r_1]) \xrightarrow {t_2-t_1} (\psi _{1l_1}, v_2 ) \xrightarrow {a_2} (\psi _{2l_2}, v_2[r_2]) \xrightarrow {t_3-t_2} (\psi _{2l_2}, v_3) \xrightarrow {a_3} (\psi _{3l_3}, v_3[r_3]) \ldots$ is a run of $\mathbb {A}_\varphi$ that accepts $w=(t_1,a_1), ( t_2,a_2), (t_3,a_3), \ldots$. $\square$

Theorem 6

Let $\varphi$ be a co-safety MTL$_{0, \infty }$ formula over $\Sigma$, then ${\mathcal {L}}_{reach}(\mathcal {A}^u_\varphi , \{true\}) {\setminus } Zeno(\Sigma )$ $\subseteq {\mathcal {L}}_{reach}(\mathbb {A}_\varphi , \{true\}){\setminus }Zeno(\Sigma )$.

Theorem 6 can be proved similarly as Theorem 5.

Example. The automaton in Fig. 3 is a deterministic under-approximation timed automaton for $\psi =(\Diamond _{\ge 1} a) \vee \Box _{\le 2}b$.

Fig. 3

Under-approximation automaton for $(\Diamond _{\ge 1} a) \vee \Box _{\le 2}b$

5 Finding a winning strategy using Uppaal-Tiga

Let us first consider that the specification contains exactly one requirement and one assumption, i.e. we are solving the synthesis problem $(\varphi \rightarrow \psi , \Sigma _c, \Sigma _u)$, where $\varphi$ and $\psi$ are safety-MTL$_{0, \infty }$ formulas over $\Sigma _c \cup \Sigma _u$.

The negation $\lnot \varphi$ is in co-safety-MTL$_{0, \infty }$ and we apply the algorithm described in the previous section to build the deterministic TA $A_{\lnot \varphi }$ such that ${\mathcal {L}}_{reach}(A_{\lnot \varphi }, \{true\}){\setminus }Zeno(\Sigma _c \cup \Sigma _u) \subseteq {\mathcal {L}}(\lnot \varphi )$. $\psi$ is in safety-MTL$_{0, \infty }$ and we build deterministic TA $A_{\psi }$ such that ${\mathcal {L}}(A_{\psi }){\setminus }Zeno(\Sigma _c \cup \Sigma _u) \subseteq {\mathcal {L}}(\psi )$. Next we add a location $false$ to both $A_{\lnot \varphi }$ and $A_{\psi }$ and add the transitions to it that are enabled when none of other outgoing transitions from the current location is enabled. In other words, we make $A_{\psi }$ and $A_{\lnot \varphi }$ complete so that they end up in $false$ if they cannot accept the input word. This syntactic transformation can be done in linear time in the automaton size. In the rest of this section we describe how we apply Uppaal-Tiga  to $A_{\lnot \varphi }$ and $A_{\psi }$ to generate a solution for the synthesis problem.

Uppaal-Tiga [5] is a tool that checks whether there exists a strategy for the controller to satisfy the given reachability or safety winning condition for all uncontrollable moves of the opponent player. Such a strategy can be syntactically represented by a timed automaton $S$ derived from the input timed automata $A$ where the guards of the controllable transitions are restricted. The semantics of strategy TA $S$ is urgent for the controller, i.e. a controller always proposes to take the earliest enabled controllable transition. Thus this semantics is essentially the same as we gave in definition 4 when we described how a timed automaton implements a strategy for a synthesis problem.

Thus if $A$ is deterministic and complete, and together with the winning condition it encodes the input specification $\varphi \rightarrow \psi$, then the winning strategy generated by Uppaal-Tiga  implements a solution for the synthesis problem $(\varphi \rightarrow \psi , \Sigma _c, \Sigma _u)$.

We construct such $A$ by forming a parallel composition of $A_{\lnot \varphi }$ and $A_{\psi }$, i.e. $A \equiv A_{\lnot \varphi } || A_{\psi }$. This parallel composition is synchronized on actions and time delays, i.e. a transition $(s_1, s_2) \xrightarrow {d} (s_1', s_2')$ exists in $A$ for some $d \in \mathbb {R}_{\ge 0} \cup \Sigma _c \cup \Sigma _u$ iff there exists a transition $s_1 \xrightarrow {d} s_1'$ in $A_{\lnot \varphi }$ and there exists a transition $s_2 \xrightarrow {d} s_2'$ in $A_\psi$. Let $L^{\lnot \varphi }_{true}$ be the set of locations of this parallel composition such that $A_{\lnot \varphi }$ is in its location $true$, and let $L^{\psi }_{false}$ be the set of locations such that $A_{\psi }$ is in its location $false$.

The goal of the controller in $A_{\lnot \varphi } || A_{\psi }$ in Uppaal-Tiga  is to:

• violate the assumption $\varphi$ by visiting a location from $L^{\lnot \varphi }_{true}$, or

• satisfy the requirement $\psi$ by avoiding visiting the locations from $L^{\psi }_{false}$.

Unfortunately Uppaal-Tiga  does not support winning conditions of the form $\Diamond (L^{\lnot \varphi }_{true}) \vee \Box (\lnot L^{\psi }_{false})$. Thus we use a stricter winning condition of $(L^{\varphi }_{true}) \mathrm{R}(\lnot L^{\psi }_{false})$, that is more hard to control for the controller. Such variations of the winning condition was previously proposed in [8] where the authors study “strict realizability of the implication” ($\Diamond (L^{\lnot \varphi }_{true}) \vee \Box (\lnot L^\psi _{false})$) and “realizability of the implication” ($(L^\varphi _{true}) \mathrm{R}(\lnot L^\psi _{false})$) for GR(1).

If the input specification contains more than one assumption and/or requirement, i.e it is of the form $\varphi _1 \wedge \varphi _2 \wedge \cdots \wedge \varphi _n \rightarrow \psi _1 \wedge \psi _2 \wedge \cdots \wedge \psi _m$, then we can still consider $\varphi = \varphi _1 \wedge \varphi _2 \wedge \cdots \wedge \varphi _n$ as a single assumption and $\psi = \psi _1 \wedge \psi _2 \wedge \cdots \wedge \psi _m$ as a single requirement (since safety-MTL$_{0, \infty }$ is closed under conjunction). However, in our implementation we construct a separate automaton for every formula, and search for a winning strategy in the parallel composition $A_{\lnot \varphi _1} || \cdots || A_{\lnot \varphi _n} || A_{\psi _1} || \cdots || A_{\psi _m}$. It is more efficient since we can avoid the full exploration of the game state space thanks to the on-the-fly game solving algorithm used by Uppaal-Tiga.

Additionally, we have to make sure that the generated strategy of Uppaal-Tiga  is non-Zeno (otherwise, we cannot guarantee that monitoring TA approximates the specification due to Theorems 1 and 2). We do this in either of two different ways.

The first way is to try to prove that all Zeno strategies are losing for the controller. We do this by adapting the construction of [22]. And second, we can force Uppaal-Tiga  to generate a non-Zeno strategy by using a Büchi acceptance condition [15]. The second way requires a more expensive algorithm for the solution of timed games with Büchi objectives, thus it is advisable to try the first way first. We describe both approaches in details in the next subsection.

5.1 Avoiding and detecting Zeno loops in Uppaal-Tiga

Our goal is to avoid generating strategies that can produce the timed words from $Zeno(\Sigma _c){\setminus }Zeno(\Sigma _u)$, we call such strategies non-Zeno.

Let us first describe the way of proving that all Zeno strategies are losing for the controller. We say that there is a controllable Zeno loop in $A_{\lnot \varphi } || A_{\psi }$ iff there exists a run $s_0 \xrightarrow {\tau _1} s_1 \xrightarrow {a_1} s_2 \dots$ such that this run is Zeno, all its actions are controllable starting from some point, and the run does not visit locations from $L^{\psi }_{false}$. It is easy to see that if there are no controllable Zeno loops in $A_{\lnot \varphi } || A_{\psi }$, then there are also no winning Zeno strategies in it. In order to detect controllable Zeno loops, we put $A_{\lnot \varphi } || A_{\psi }$ in parallel with a test automaton depicted in Fig. 4 (we consider here that $\Sigma _u = \{\mathbf{a1}, \mathbf{a2}, \mathbf{a3} \}$). This test automaton $A_Z$ has two locations L1 and L2, and location L2 is urgent (see [6]), i.e. automaton arrives in location L2, it should leave it at the next transition without time being elapsed. Additionally, the location L1 has an invariant $x \le 1$ which states that the TA should leave this location as soon as the value of $x$ reaches $1$. We use Uppaal (basic version) to check that $A_{\lnot \varphi } || A_{\psi } || A_Z$ satisfies property $\Box (L1 \rightarrow \Diamond L2)$, that can be expressed as L1 –> L2 in Uppaal. It is easy to see that there exists a controllable Zeno loop in $A_{\lnot \varphi } || A_{\psi }$ iff this property is not satisfied by $A_{\lnot \varphi } || A_{\psi } || A_Z$.

Fig. 4

A test automaton $A_Z$ for the detection and forcing of non-Zeno behavior

If there exists a controllable Zeno loop in $A_{\lnot \varphi } || A_{\psi }$, then we prevent the controller from playing a Zeno strategy by adding a requirement that the time should always progress. We do this by again considering a parallel composition $A_{\lnot \varphi } || A_{\psi } || A_Z$ and asking Uppaal-Tiga  to find a winning strategy for the winning condition $((L^{\varphi }_{true}) \mathrm{R}(\lnot L^{\psi }_{false})) \wedge \Box \Diamond L2$ (see  [15]).

6 Case studies

We present three case studies, and for some of them we compare the performance of our tool to the performance of Acacia+ [9] and Unbeast [18] that are state-of-the art synthesis tools for LTL. The comparison with Unbeast is of special interest because it is designed for the assume-guarantee properties, just like our approach. Acacia+ is especially efficient for the compositional specifications being of the form $\bigwedge _i \phi$, thus we use the compositional synthesis in Acacia+ and transform the specifications $\varphi _1 \wedge \cdots \wedge \varphi _n \rightarrow \psi _1 \wedge \cdots \wedge \psi _m$ into $(\varphi _1 \wedge \cdots \wedge \varphi _n \rightarrow \psi _1) \wedge \cdots \wedge (\varphi _1 \wedge \cdots \wedge \varphi _n \rightarrow \psi _m)$. We experimentally checked that Acacia+ is more efficient in this case, even if the input specification is larger. For Acacia+ and Unbeast we use the LTL3BA tool [4] as it gives smaller automata for our specifications than the LTL2BA tool.

For all the case studies our implementation managed to produce exact monitoring Timed Automata for the input specifications. Additionally, our implementation detected for all the specifications that there are no winning Zeno strategies (the timing results include this check). However, for the comparison reasons we also present the results for the Büchi-based approach. We report the number of rules (transitions) of a strategy graph as a strategy size.

The experiments were held in Amazon Elastic Cloud on a High-Memory Quadruple Extra Large Instance (64 GB of memory, processor power equivalent to 3.25 GHz 2007 Xeon processor). The timeout is fixed to 1 h.

6.1 Job scheduling problem

Consider the following online job scheduling problem. There are $N$ computational units, and computation of a job on a single unit takes $T$ time units. New jobs can arrive sporadically, and we assume that the minimal time between the arrivals of two jobs is $1$ time unit.

The goal of the scheduler is to assign new jobs to the computational units, so no two jobs overlap in time on the same computational unit. We require that this assignment should happen immediately after a job arrives, and jobs cannot be moved from one computational unit to another.

Obviously, the problem has a solution iff $N \ge T$. We study the borderline case of $N=T$. Our specification is defined over a set of uncontrollable actions $\Sigma _u = \{job\}$ and a set of controllable actions $\Sigma _c = \{u_1, u_2, \ldots , u_N\}$. The environment triggers action $job$, when a new job arrives, and the controller can assign a computation unit $i$ to it by triggering $u_i$. The specification is $\varphi _{{1}} \rightarrow \psi _{{1}} \wedge \psi _{{2}} \wedge \psi _{{3}}$, where the components are defined in Table 1. The time results are given in Table 2. This specification is essentially based on time, thus we didn’t apply Acacia+ and Unbeast to it. The strategy sizes are equal for the two ways of avoiding Zeno behavior in our implementation (although we don’t prove that it is true in general).

Table 1 Specification for the job scheduling problem

Table 2 Results for the job scheduling problem

Figure 5 contains solution for the $N=2$. For simplicity, we removed one extra clock whose value is always equal to the value of $x$.

Fig. 5

Synthesized strategy for the jobs scheduling problem for $N=2$

6.2 Dining Philosophers problem

Consider that there are $N$ philosophers (that are a part of the environment). A philosopher may indicate that he is hungry (event $hungry_i$ for philosopher $i$). The controller can tell a philosopher to take his left or right fork, or tell him to start eating (events $lfork_i, rfork_i$ and $eat_i$ for philosopher $i$). A philosopher may indicate that he finished eating (event $finish_i$), and at the same time he puts both forks on the table. Thus the set of uncontrollable actions is $\Sigma _u = \{hungry_1, \ldots , hungry_N, finish_1, \ldots , finish_N \}$, and the set of controllable actions is $\Sigma _c = \{lfork_1, \ldots , lfork_N, rfork_1, \ldots , rfork_N, eat_1, \ldots , eat_N \}$.

We also transformed this MTL$_{0, \infty }$ specification into the untimed LTL specifications for Acacia+ and Unbeast (basically, we removed all the timing constraints from the formula). As it can been seen from Table 6, Acacia+ and Unbeast scaled only up to $N=2$, while our tool scaled up to $N=4$. One can argue that the LTL specification for certainly requires Büchi acceptance condition, while our MTL$_{0, \infty }$ specification is a Boolean combination of safety formulas. Therefore we made another LTL specification for Acacia+ and Unbeast where we discretized time (i.e. assumed bounded variability), and this specification does not contain until operators and thus does not require Büchi acceptance condition. For this specification Acacia+ can also handle only the case of $N=2$ with the maximal time granularity of $2$, and Unbeast can additionally handle $N=2$ and time granularity $3$. We do not report strategy sizes for Unbeast because we were not able to extract them.

Our specification is given in Table 3, and the experimental results are presented in Table 6. The Acacia+ and Unbeast LTL specifications for the Dining Philosophers problem are described in details in the next two subsections.

Table 3 Specification for the dining philosophers problem

6.2.1 Dining Philosophers specification for Acacia+ and Unbeast: LTL specification

The synthesis game in Acacia+ and Unbeast is played in rounds, and in each round one player (i.e. controller or environment) always plays first, and the other (second) player plays second. In each round the first player proposes some subset $\Sigma _1$ of his propositions, and the second player observes $\Sigma _1$ and proposes some subset $\Sigma _2$ of his propositions. Thus together they produce the next element of a run that is $\Sigma _1 \cup \Sigma _2$.

Thus in total we face three imprecisions when we translate our Dining philosophers specification from MTL$_{0, \infty }$ into LTL:

• Our tool supports time constraints, while Acacia+ and Unbeast do not. Thus we drop all the timing constraints in the LTL specification. Additionally, in LTL we are not available to specify the fact that a philosopher cannot say $hungry$ too often (assumption $\varphi _\mathbf{1 }$). Thus instead of saying this we use an assumption that a philosopher cannot say $hungry$ twice without being eating in between. We also consistently change $\varphi _\mathbf{2 }$ and $\psi _\mathbf{1 }$ to reflect this fact.

• At each round in LTL synthesis game each player can propose a set of propositions, not just a single action. Although we can force each player propose not more than one proposition at a time (by adding additional requirements and assumptions), it will make it more difficult for Acacia+ and Unbeast to synthesize a controller due to its algorithm that counts the number of times an automaton visits the Büchi acceptance locations. Thus we let each player to propose several propositions at once (e.g. tell two different philosophers to start eating). However, we do not allow a philosopher to say that he is hungry and say that he finished eating at the same time slot, since the order of these events is crucial and it is unspecified in this case (assumption $\varphi _\mathbf{4 }$). Similarly, a controller cannot tell a philosopher to start eating and to take a fork at the same time (requirement $\psi _\mathbf{5 }$). Additionally, we have to modify the requirement $\psi _\mathbf{2 }$ to prevent the controller from giving the same fork simultaneously to two neighboring philosophers.

• The notion of the next state in our turn-based semantics is different for the first and the second players. We assume that at each round the environment is making the first move (by using the option “-p 1” of Acacia+). We also modify $\varphi _\mathbf{3 }$ to handle the fact that in the semantics of Acacia+ and Unbeast the propositions of the controller and the environment are mixed together at each round.

Table 4 Untimed LTL specification for the dining philosophers problem

LTL specification for the Dining Philosophers problem is given in Table 4.

6.2.2 Dining Philosophers specification in LTL using time discretization

We define a discretized version of Until operator:

$$\begin{aligned} \varphi \text {U}^*_{\le d} \psi \equiv \psi \vee (\varphi \wedge {\bigcirc }\psi ) \vee \cdots \vee (\varphi \wedge {\bigcirc }\varphi \wedge \cdots \wedge \underbrace{{\bigcirc }\dots {\bigcirc }}_{d-1} \varphi \wedge \underbrace{{\bigcirc }\dots {\bigcirc }}_{d} \psi ). \end{aligned}$$

We define $\Diamond ^*_{\le d} \varphi$ to be equal to $true \text {U}^*_{\le d} \phi$, and $\Box _{\le d}^* \varphi$ to be equal to $\lnot \Diamond ^*_{\le d} \lnot \varphi$.

Like in the previous (untimed) specification, in our LTL specification for fixed time granularity we also assume that at each slot(round) the environment plays first. Thus we use $\varphi _\mathbf{4 }$ and $\psi _\mathbf{5 }$ from the previous untimed specification.

Table 5 LTL specification for the dining philosophers problem with discretized time

Table 6 Results for the dining philosophers problem

Let us fix an integer $k$ being a time granularity (i.e. a number of times a signal can change during one time unit). Our LTL specification for the Dining Philosophers problem with discretized time is given in Table 5.

6.3 Generalized buffer controller

The generalized buffer controller synthesis problem has been first studied in [7] for Generalized Reactivity (1). In [21] the authors reformulate this problem in LTL and apply Acacia+ to it. This specification describes a system that contains several senders and receivers with a buffer in-between them. The specification is of the form $(\varphi _s \rightarrow \psi _s) \wedge (\varphi _r \rightarrow \psi _r)$, where $\varphi _s$ ($\varphi _r$, correspondingly) is the assumption over the behavior of the senders (receivers) and $\psi _s$ ($\psi _r$, correspondingly) is the requirements over the behavior of the controller with respect to senders (receivers). We transformed the specification into $(\varphi _s \wedge \varphi _r) \rightarrow (\psi _s \wedge \psi _r)$, since the former specification $(\varphi _s \rightarrow \psi _s) \wedge (\varphi _r \rightarrow \psi _r)$ is not supported by our tool. Thus in the experiments for our tool we study a weaker specification than Acacia+’s, and our MTL$_{0,\infty }$ specification requires the buffer to behave correctly only if both senders and receivers follow their assumptions.

Consider that there are $N$ senders and $M$ receivers. Acacia+ specification is defined over controllable signals $\{b2s\_ack\_i\}$ and $\{b2r\_req\_j\}$ and uncontrollable signals $\{s2b\_req\_i\}$ and $\{r2b\_ack\_j\}$ where $i$ ranges in $1\ldots N$ and $j$ ranges in $1\ldots M$. $\{b2r\_req\_j\}$ and $\{s2b\_req\_i\}$ are dealt as continuous signals that can be turned on for some duration of time. Thus in the specification for our tool we model each of these signals with two actions, one for the start of a signal and one for its end, i.e. we defined the actions $b2r\_req\_j\_on, b2r\_req\_j\_\text { off}$ and $s2b\_req\_i\_on, s2b\_req\_i\_\text { off}$. The signal $b2r\_req\_j$ ($s2b\_req\_i$) is assumed to be turned on in between the actions $b2r\_req\_j\_on$ and $b2r\_req\_j\_\text { off}$ ($s2b\_req\_i\_on$ and $s2b\_req\_i\_\text { off}$). $\{b2s\_ack\_i\}$ and $\{r2b\_ack\_j\}$ are instantaneous signals, thus we leave them as actions as it is.

The goal of this case study is to demonstrate that our tool can be applied to a specification already used with another tool. Thus we do not translate the formula in the format of Unbeast and also use only the specifications sizes provided in the Acacia+ distribution.

Our specification is given in Table 7. Basically, we added time constraints to the unbounded “eventually” operators, so that the specification fits the format supported by our tool.

Table 7 MTL$_{0,\infty }$ specification for the generalized buffer controller problem of [21]

Table 8 contains the experimental results for this problem.

Table 8 Results for the generalized buffer specification

7 Conclusions

We present an algorithm for the synthesis of the specifications of the form $\varphi _1 \wedge \varphi _2 \wedge \cdots \wedge \varphi _n \rightarrow \psi _1 \wedge \psi _2 \wedge \cdots \wedge \psi _m$, where all $\varphi _i$ and $\psi _j$ are safety-MTL$_{0,\infty }$ formulas. The algorithm is based on a novel translation procedure from safety and co-safety MTL$_{0,\infty }$ into under-approximation deterministic timed automata. This allows our approach to scale well to large specifications, and have a comparable or better performance to the state-of-the-art synthesis tools Acacia+ and Unbeast (the specifications are not precisely the same, but have been modified for a timed setting). We believe that our approach can be extended to the specifications being arbitrary Boolean combinations of safety-MTL$_{0,\infty }$ properties.

Our approach is sound but not complete. This incompleteness comes from the fact that the generated monitoring TA can be non-exact (under-approximates the input specification). Additionally we use the winning condition $(L^{\varphi }_{true}) \mathrm{R}(\lnot L^{\psi }_{false})$ in Uppaal-Tiga  that is stronger than the minimally required $\Diamond (L^{\lnot \varphi }_{true}) \vee \Box (\lnot L^{\psi }_{false})$. However, our tool managed to produce the solutions for all the specifications we studied. In the future work we may address the decidability of the original problem (i.e. is it possible to provide a complete algorithm), and provide an algorithm with better coverage.