1 Introduction↩︎

Metric Temporal Logic [1] is an extension of Linear Temporal Logic (LTL) to reason about timing constraints between events. Syntactically, it is obtained by adding intervals to the temporal operators, for instance the Until operator \(\mathcal{U}\) of LTL becomes \(\mathcal{U}_I\) in MTL, with \(I\) being an interval over the reals that is bounded by natural numbers or \(\infty\). MTL can be interpreted over timed words (pointwise semantics), or over timed signals (continuous semantics). For comparisons between these semantics we refer the reader to [2], [3]. In this work, we will consider only the pointwise semantics.

Over the years, it has been established that MTL satisfiablity is undecidable over infinite words [4], whereas it is decidable over finite words, albeit with non-primitive recursive complexity [5], [6]. A restriction of MTL, called Metric Interval Temporal Logic (MITL) limits the syntax by disallowing singleton intervals, i.e., intervals of the form \([l,l]\). In a fundamental work [7] it was shown that MITL satisfiability is EXPSPACE-complete for both finite and infinite words. This positive result has led to several improvements and the development of tools for MITL satisfiability and model-checking [8]–[13].

Satisfiability procedures typically involve a translation of MITL to some form of automata: the very first work [7] translates MITL formulas to equivalent timed automata [14]; subsequent work [8] and its extensions translate MITL to a model of 1-clock alternating timed automata, which are then compiled to a network of timed automata; the recent work [12] translates MITL to generalized timed automata [15]. A common perception in this line of work is that the translations can be difficult to understand, as they require a careful case analysis and/or rely on sophisticated machinery. This is particularly the case for the Until operator \(\mathcal{U}_I\) when \(I\) is a two-sided interval, with none of the end-points being \(0\) or \(\infty\).

In this paper, we present a new technique for MITL satisfiability, which incidentally does not go via an automaton translation. We believe our technique is simpler to understand as it does not require any intricate transformation or heavy machinery. Our approach stays close to mimicking the semantics of satisfaction of formulas. To assert whether a formula is true at a point in the word, one can generate an obligation which needs to be settled along the word. For instance, the LTL formula \(a~\mathcal{U}~b\) (with strict Until semantics) is true at position \(i\) if either \(b\) or the set \(\{a, a~\mathcal{U}~b\}\) is true at \(i+1\): put in other words, the obligation \(a~\mathcal{U}~b\) at position \(i\) generates either an obligation \(b\) or a set of obligations \(\{a, a~\mathcal{U}~b\}\) at position \(i+1\). We enrich this notion of obligations by storing some kind of timing information and build a transition system whose accepting runs precisely capture the set of timed words satisfying the formula (Section 4). Furthermore, for MITL, we prove that it is sufficient to maintain a bounded set of obligations at each point in the word: the key contrast w.r.t. the existing approaches is the fact that we arrive to this bound by simple rules to merge or eliminate redundant obligations (Section 5). Finally, we develop a region-abstraction over these obligations which leads to a symbolic algorithm for MITL satisfiability (Section 6). After recalling preliminaries in Section 2, we present in Section 3 a detailed overview of the existing approaches followed by a brief introduction to our approach.

2 Preliminaries↩︎

Let \(\Sigma\) be a finite alphabet. Let \(\mathbb{N}\) and \(\mathbb{R}_{\geq 0}\) denote the set of natural numbers (including \(0\)) and non-negative reals, respectively. A timed word is an infinite sequence \(w = (a_1,\tau_1)(a_2,\tau_2)\dots\) where \(a_i \in \Sigma\) for each \(i \in \mathbb{N}\), and \(\tau_i \in \mathbb{R}_{\geq 0}\) with \(\tau_i \le \tau_{i+1}\) for all \(i \in \mathbb{N}\). The number \(\tau_i\) denotes the timestamp of occurrence of the action \(a_i\). A timed word is non-Zeno if the sequence \(\{\tau_i\}_{i \ge 1}\) of timestamps is diverging. Therefore, in a non-Zeno timed word, every unit interval contains only finitely many actions.

Metric Temporal Logic (MTL). The syntax of MTL is described using the grammar: \[\begin{align} \varphi:= \top \mid \bot \mid a \mid \lnot a \mid \varphi \land \varphi \mid \varphi \lor \varphi \mid \lnot \varphi \mid \varphi ~\mathcal{U}_{I}~ \varphi \mid \varphi ~\widetilde{\mathcal{U}}_{I}~\varphi \end{align}\] where \(a \in \Sigma\), \(I \subseteq\mathbb{R}_{\geq 0}\) is a closed, open or half-closed interval with endpoints in \(\mathbb{N}\cup \{\infty\}\); \(\mathcal{U}\) is called the Until operator, and \(\widetilde{\mathcal{U}}\) is called the dual Until operator. Given a timed word \(w = (a_1,\tau_1)(a_2,\tau_2)\dots\), a position \(i \ge 1\) and an MTL formula \(\varphi\), we define when \(w\) satisfies \(\varphi\) at position \(i\), written as \((w,i) \models\varphi\), as follows:

• \((w, i) \models\top\), \((w, i) \not \models\bot\)

• \((w, i) \models a\) if \(a_{i} = a\), and \((w,i) \models\lnot a\) if \(a_{i} \neq a\)

• \((w,i) \models\varphi_{1} \land \varphi_{2}\) if \((w,i) \models\varphi_{1}\) and \((w,i) \models\varphi_{2}\)

• \((w,i) \models\varphi_{1} \lor \varphi_{2}\) if \((w,i) \models\varphi_{1}\) or \((w,i) \models\varphi_{2}\)

• \((w,i) \models\lnot \varphi\) if \((w,i) \not\models\varphi\)

• \((w,i) \models\varphi_1 ~\mathcal{U}_{I}~ \varphi_{2}\) if there is some \(j > i\) such that \((w,j) \models\varphi_{2}\), \(\tau_j - \tau_i \in I\) and for all \(i < k < j\), we have \((w,k) \models\varphi_1\)

• \((w,i) \models\varphi_1 ~\widetilde{\mathcal{U}}_I~ \varphi_2\) if for all \(j\) s.t. \(j > i\) and \(\tau_j - \tau_i \in I\), either \((w,j) \models\varphi_{2}\), or there is some \(k\) with \(i < k < j\) with \((w,k) \models\varphi_{1}\)

Observe that we make use of a strict semantics for the \(\mathcal{U}_I\) operator as in [5], [11], [16]: we say \(j > i\) (strictly greater) and \(i < k < j\). The weak semantics (with \(j \ge i\) and \(i \le k < j\)) can be recovered using the strict Until operator. For example, writing \(\mathcal{WU}\) for the until operator with a non-strict semantics, we see that \((a ~\mathcal{WU}_{[0,5]}~ b) = b \lor (a \land (a~\mathcal{U}_{[0, 5]}~b))\).

Notice from the semantics that: \(\neg (\varphi_1~\mathcal{U}_I~\varphi_2) = (\neg \varphi_1)~\widetilde{\mathcal{U}}_I~(\neg \varphi_2)\), and \(\neg (\varphi_1~\widetilde{\mathcal{U}}_I~\varphi_2) = (\neg \varphi_1)~\mathcal{U}_I~(\neg \varphi_2)\). Hence any formula of the form \(\neg \varphi\) can be converted into a negation normal form where all the negations appear at the atomic level and whose size is linear in the size of the original formula. From now on, we assume formulas are in negation normal form wlog. Here are some derived operators for convenience [5]: constrained next time operator \(\mathbf{X}_I\varphi \equiv \bot~\mathcal{U}_I~\varphi\), constrained eventually \(\mathbf{F}_I \varphi \equiv \top \mathcal{U}_I \varphi\), and constrained always \(\mathbf{G}_I \varphi \equiv \neg (\top ~\mathcal{U}_I~\varphi) \equiv \bot~\widetilde{\mathcal{U}}_I~(\neg \varphi)\). Furthermore, if \(I\) is \(\mathbb{R}_{\geq 0}\), we might omit the subscript.

The satisfiability question for MTL is as follows: given an MTL formula \(\varphi\) does there exist a non-Zeno timed word \(w\) such that \(w \models\varphi\). This problem is known to be undecidable [4].

Metric Interval Temporal Logic (MITL). An interval \(I\) is said to be singular if it contains a single point, i.e., it is of the form \([l,l]\) for some \(l \in \mathbb{N}\). MITL is a restriction of MTL where all intervals used are nonsingular: for e.g., \(a ~\mathcal{U}_{[2,2]} b\) is not an MITL formula. For MITL, the satisfiablity problem was shown to be EXPSPACE-complete in [7]. Their algorithm converts an MITL formula into an equivalent timed automaton, equipped with a generalized Büchi condition. Although the procedure is described for the continuous semantics (that uses timed state sequences instead of timed words), it is mentioned in [7] that the result also holds for the pointwise semantics (that uses timed words as we do in this paper).

3 Existing constructions for MITL and overview of our approach↩︎

Let us start with the untimed LTL formula of the form \(\varphi_1 \mathcal{U}\varphi_2\), and an untimed word \(a_1 a_2 \cdots\). To assert \(\varphi_1 \mathcal{U}\varphi_2\) at position \(i\), the procedure needs to check if there exists a \(j > i\) that satisfies \(\varphi_2\) and \(\varphi_1\) holds at all positions \(k\) such that \(i < k < j\) (recall we are using strict semantics for Until). Automata constructions typically maintain the formula \(\varphi_1 \mathcal{U}\varphi_2\) as an obligation in the state or configuration that reads \(a_i\). During the transition on \(a_i\), the obligation \(\varphi_1 \mathcal{U}\varphi_2\) at \(i\) is transformed into one of two possible ways at \(i+1\) non-deterministically: it either becomes an obligation \(\varphi_2\) or a set of obligations \(\{ \varphi_1, \varphi_1 \mathcal{U}\varphi_2 \}\). This construction is continued, leading to a set of obligations being maintained at each configuration along the word. Since the obligations are simply subformulas of the main formula being checked, and since there is no need to maintain multiple copies of the same subformula in a configuration, the state-space thus generated is finite and leads to an automaton construction.

Let us now see what happens in the timed case. We consider the case \(\varphi_1 \mathcal{U}_I \varphi_2\) where \(I\) is a bounded interval of the form \([l, u]\), as this is the most complex case. Timing information needs to be encoded into the configurations maintaining the obligations. Let \(w = (a_1, \tau_1) (a_2, \tau_2) \cdots\) be a timed word. Once again, we assume we need to assert \(\varphi_1 \mathcal{U}_I \varphi_2\) at position \(i\).

The 1-ATA method [6].

A method using 1-clock alternating timed automata (1-ATA) was proposed in [6]. On reading the letter \(a_i\), the automaton generates an obligation of the form \((\varphi_1 \mathcal{U}_I \varphi_2, 0)\), where \(0\) denotes the time since the obligation has been generated. On reading \(a_{i+1}\) at the next position \(i+1\), the obligation is non-determinitically transformed to either \((\varphi_2, 0)\) provided \(\tau_{i+1} - \tau_i \in I\), or a set \(\{(\varphi_1, 0), (\varphi_1 \mathcal{U}_I \varphi_2, \tau_{i+1} - \tau_i ) \}\). In the second case, notice that there is a fresh obligation on \(\varphi_1\) that is generated. When these transition rules are continued further down the run, more obligations on \(\varphi_1\), with varying values of the associated timing component could be generated. Hence the configurations generated have unbounded “width”: there is no bound on the number of obligations generated inside a configuration. A region-like abstraction was proposed in [6] and it was shown that for finite timed words, the abstraction along with a suitable entailment relation leads to a finite transition system. This was proposed in the context of full Metric Temporal Logic, and no customization for MITL was studied.

The MightyL approach [8]–[10].

Later methods concentrated on controlling the number of obligations generated per subformula when the logic is restricted to the MITL fragment. The first line of work in this direction is [8] which developed an idea of 1-clock alternating timed automata with an interval semantics. Intuitively, the interval semantics was used to abstract a set of obligations by considering the earliest and latest generated within that set. While [8] was restricted to finite words, it was extended to infinite words in [9]. These works laid the foundation for the tool MightyL [10] which presented a full conversion from MITL to a network of timed automata, going via the abstraction described above. However, the number of discrete states generated for an until formula \(\varphi_1 \mathcal{U}_I \varphi_2\) was exponential in a constant \(\kappa = 1 + \lceil \dfrac{l}{u - l}\rceil\). A follow-up to MightyL, avoiding this blow-up, is the very recent work that we describe next.

The MightyPPL approach [11].

This is a different approach to MightyL where the novelty lies in encoding \(\varphi_1 \mathcal{U}_I \varphi_2\) using a “Pnueli operator” \(\mathsf{Pn}\): a formula \(\mathsf{Pn}_I(\phi_1, \phi_2, \dots, \phi_n)\) holds at position \(i\) if there exist \(i < j_1 < j_2 < \cdots < j_n\) such that for each \(1\le m \le n\), \(\tau_{j_m} - \tau_i \in I\) and \((w, j_m) \models \phi_m\). Such a formula cannot be written in plain MITL. It is argued that \(\varphi_1 \mathcal{U}_{(k, k+1)} \varphi_2\) is equivalent to the following formula (see Lemma 3 of [11], Lemma 9 of [17]):

where \(\phi^{\ge 1} = \varphi_2 \land (\neg \varphi_2 \mathcal{U}_{[1, \infty]} \varphi_2)\). The above observation extends to intervals of the form \([l, u]\). Subsequently, the Pnueli operator \(\mathsf{Pn}(\phi_1, \dots, \phi_n)\) is translated into a network of timed automata. Careful optimizations ensure that the additional blowup as in MightyL is avoided.

The TEMPORA approach [13], [18].

Another recent approach to MITL satisfiability uses the model of Generalized Timed Automata (GTA) [15]. The novelty in this approach is the use of future clocks (called timers here) to guess times to certain good witnesses. Intuitively, a timer is assigned (non-deterministically) a non-negative value and then decreases towards \(0\); technically and equivalently, a timer can be assigned a non-positive value and made to increase towards \(0\) as in [15]. When the timer hits \(0\), we say it times out. To assert \(\varphi_1 \mathcal{U}_I \varphi_2\) at position \(i\), this approach makes two guesses (their approach uses a weak Until semantics, which we reformulate for the strict semantics):

• the last position \(j\) in the interval \(\tau_i + I\) such that \(\varphi_2\) is true at \(j\), and \(\varphi_1\) holds at all positions between \(i+1\) and \(j-1\); the time to this position \(j\) from \(i\), i.e., \(\tau_j - \tau_i\) is stored in a future \(x_1\).

• the first position \(j'\) after \(\tau_i + I\) such that \(\varphi_2\) is true at \(j'\) and \(\varphi_1\) is true at all positions between \(i+1\) and \(j'-1\); the time to \(j'\), i.e., \(\tau_{j'} - \tau_{i}\) is stored in a future \(y_1\).

If such a position does not exist, the corresponding clock is undefined. Let us restrict to the case when both positions exist. As time elapses, the absolute values of these future clocks decrease. As long as \(y_1\) has not timed out, it is shown that no new obligation needs to be generated, since for each intermediate position, either \(j\) or \(j'\) acts as a witness, or it can be ascertained that \(\varphi_1 \mathcal{U}_I \varphi_2\) is not true at that encountered intermediate position. By construction, \(y_1\) is initially set to a value greater that \(I\). Therefore, the time elapse between its initial origin until its timeout is at least \(|I|\). Hence, for \(|I|\) time units, no new obligation needs to be generated. After that, fresh guesses \(x_2, y_2\) in the same spirit as above are made. Hence, at any point of time during the run, there could be future clocks \(x_1, y_1, x_2, y_2, \dots, x_i, y_i\) maintaining the time remaining to suitably guessed witnesses. Moreover, the number of such guesses is bounded. When these future clocks time out, or between the timeouts, the appropriate guesses need to be verified. For instance, between the timeout of each \(x_j\) and \(y_j\), formula \(\varphi_1\) needs to be true, but \(\varphi_2\) needs to be false. Secondly, there are subtleties arising due to witnesses coinciding: for example, the witness corresponding to \(y_i\) may be the same as the one maintained by \(x_{i+1}\). The final GTA carefully incorporates the guesses, the verification and the various subtle cases (Algorithm 2 in [18], Algorithm 1 in [12]).

Our approach.

We roll back in spirit to the 1-ATA approach that maintains obligations of the form \((\varphi, 0)\), but in addition, we make use of the ability of timers from the GTA approach. In order to check if \((w, i) \models \varphi_1 \mathcal{U}_I \varphi_2\), while reading \(a_i\) we make a guess that \(\varphi_1 \mathcal{U}_I \varphi_2\) is true at \(i\) by generating an obligation as follows: \[\begin{align} (\varphi_1 \mathcal{U}_I \varphi_2, 0, t) \end{align}\] where the first component denotes the formula that needs to be true, the second component denotes the age of the obligation, i.e., the time since the obligation was generated and finally the third and most important component gives a waiting time \(t\) predicting the time left to witness a position \(j\) that satisfies \(\varphi_2\). As expected, we require \(t\) to be in the interval \(I\).

On a time elapse of \(\delta\) units, the obligation becomes: \[\begin{align} (\varphi_1 \mathcal{U}_I \varphi_2, \delta, t - \delta) \end{align}\] The time elapse \(\delta\) gets added to the age, and gets subtracted from the waiting time, as long as \(\delta \le t\). Suppose the next letter \(a_{i+1}\) occurs at this point \(t_i + \delta\), the obligation changes as follows: if \(t - \delta > 0\) (guessed position has not arrived yet), then the obligation continues to remain and alongside it generates an obligation for \(\varphi_1\); if \(t - \delta = 0\) (that is, waiting time is \(0\)), then there is a non-deterministic choice, either the current obligation is discharged and an obligation for \(\varphi_2\) is generated denoting that a witness for \(\varphi_2\) has been identified, or it continues to remain as it is, and generate one for \(\varphi_1\). In the latter case, there can be no time elapse until the original \(\varphi_1 \mathcal{U}_I \varphi_2\) obligation is discharged.

Figure 1 (left) gives an illustration: position \(i\) is represented by the red dot, and position \(j\) by the green dot. At \(i\) an obligation \(\theta_{\varphi}\) is generated which continues to remain until point \(j\) where it is discharged, and a new obligation \(\theta_{\varphi_2}\) is generated. At all intermediate positions where \(\theta_{\varphi}\) is alive, an obligation for \(\varphi_1\) is generated.

For Dual Until formulas, the role of obligations is different, mimicking the semantics. Consider a Dual Until formula \(\varphi = \varphi_1 \widetilde{\mathcal{U}}_I \varphi_2\), with \(I = [l, u]\) (say). To check if \((w, i) \models \varphi\), an obligation of the following form is generated: \[\begin{align} (\varphi_1\widetilde{\mathcal{U}}_I\varphi_2, 0, u) \end{align}\] where the first two components are the same as before; and the third component simply maintains time until when this obligation needs to be alive. In Figure 1 (right), an obligation is shown to be generated at position \(i\). The green dots inside the interval \([\tau_i + l, \tau_i + u]\) are the positions where the dual Until condition needs be checked. These positions can be identified by looking at the age of the obligation: when age is \(\ge l\) we are inside the interval.

On a time elapse of \(\delta\), the Dual until obligation transforms to \((\varphi_1 \widetilde{\mathcal{U}}_I \varphi_2, \delta, u - \delta)\) if \(\delta \le u\). When \(\delta > u\), a time elapse of \(\delta\) simply makes the obligation vanish. This is in sharp contrast with Until obligations, where time was not allowed to elapse beyond the waiting time that was initially guessed. For Until formulas, the obligation is guessing an event that should happen at \(t\) time units and hence it is “obliged” to witness it, else it deadlocks. For Dual Until, the role is to ensure that upto a certain time, some events should happen. Beyond that, the obligation is useless and hence can be removed.

In a nutshell: on each letter, an obligation is potentially generated, with a specific role, until it is discharged. When it is alive, the obligation may spawn more obligations depending on its role. In Section 4 we will present a formal definition of a transition system made up of obligations, whose accepting runs are precisely the words where the formula is true. Notice that we do not predict special kinds of witnesses as in the GTA approach. Instead we just guess some witness. The key question is how do we obtain an upper bound on the number of generated obligations with these mundane guesses. Section 5 discusses simple rules to reduce obligations that results in a uniform bound on the number of obligations that are stored.

4 Obligations↩︎

Before we proceed further, we remark that in previous works on this subject, the word “obligation” has been used in its natural language sense to mean an assertion that should be checked. Moreover, obligations meant different things in different works. In our work, we consider another kind of obligations for which we provide a formal definition (Definition 1). We distinguish between bounded and unbounded intervals: an interval is bounded if its right endpoint is in \(\mathbb{N}\), and is unbounded when it is \(\infty\). For formulas with unbounded intervals, we make the third component inactive in the obligations. This ensures that all waiting times that we use are globally bounded by a constant determined by the formula. This fact crucially helps in the symbolic computation explained in Section 6.

Fix an MTL formula \(\varphi\) for the rest of this section. Indeed, all the results we develop in this section work for the full class of MTL.

The initiation of an obligation depends on the form of \(\varphi\). For instance consider \((a ~\mathcal{U}_{[1, 4]}~ b) \land ((\mathbf{F}_{[5, 10]} c)~\mathcal{U}_{[3,5]}~ d)\). There are two top-level Until operators \(\mathcal{U}_{[1,4]}\) and \(\mathcal{U}_{[3,5]}\). The initiation involves guessing witnesses for each of these two operators. Here is a possible guess \(\{ (a~\mathcal{U}_{[1,4]}~b, 0, 3.7), ~((\mathbf{F}_{[5,10]} c)~\mathcal{U}_{[3,5]}~ d, 0, 4.8) \}\); another possible guess could have been \(\{ (a~\mathcal{U}_{[1,4]}~b, 0, 1.5), ~((\mathbf{F}_{[5,10]} c)~\mathcal{U}_{[3,5]}~ d, 0, 3.3) \}\). The next definition formalizes this idea by associating to each formula \(\varphi\) and a letter \(a\), an initial set of possible obligation-sets, denoted as \(\mathcal{O}_{\varphi, a}\). We require to make a distinction between a formula (like \(\top\)) which holds without any obligations, versus a formula (like \(\bot\)) which cannot be satisfied at all. When \(\varphi\) cannot be satisfied, we leave \(\mathcal{O}_{\varphi, a}\) undefined. When \(\varphi\) is satisfied without any obligations, we define \(\mathcal{O}_{\varphi,a}\) to be an empty set denoting that no obligations are needed. When we write \(\Theta \in \mathcal{O}_{\varphi,a}\) we intrinsically assume that \(\mathcal{O}_{\varphi,a}\) is defined.

Intuitively, each element of \(\mathcal{O}_{\varphi,a}\) is a guess for why \(\varphi\) is true at the position which reads \(a\). As time evolves and more actions appear, the transitions are defined to verify this guess (or deadlock in case of wrong guesses). We now formalize how obligations evolve as time progresses and more letters are seen. Each individual obligation may result in an obligation-set when a new letter is seen. Hence we first define transitions as a function from an obligation to an obligation-set, and then define how this extends as a function from an obligation-set to an obligation-set.

The delays behave differently for \(\mathcal{U}_I\) and \(\widetilde{\mathcal{U}}_I\) obligations: \(\mathcal{U}_I\) obligations cannot elapse more than their waiting time, whereas \(\widetilde{\mathcal{U}}_I\) obligations simply vanish when time elapses more than their waiting time, and hence do not block time from elapsing.

Notice the difference in the delay semantics between \(\mathcal{U}\) and \(\widetilde{\mathcal{U}}\).

We move on to discrete transitions, starting with \(\mathcal{U}\) obligations. As illustrated in Figure 1 (left), the role of an Until obligation for \(\varphi = \varphi_1 \mathcal{U}_I \varphi_2\) is to keep generating obligations for \(\varphi_1\), until its waiting time becomes \(0\) when it non-deterministically decides to lance an obligation for \(\varphi_2\) or keep continuing to check \(\varphi_1\) without elapsing time. Lancing an obligation for a formula \(\psi\) amounts to guessing an initial obligation-set for \(\psi\).

When some \(\mathcal{O}_{\psi,a}\) is not defined, the transition that involves obligation-sets from \(\mathcal{O}_{\psi,a}\) is also not defined. Also notice that the transitions defined below are non-deterministic: not only because of the multiple transitions possible when the waiting time \(t = 0\), but also because we are non-deterministically picking an obligation-set from initial obligation-sets when applicable.

For the Dual Until, let us refer to Figure 1 (right). For all the green points inside the interval the obligation needs to check that either \(\varphi_2\) is true, or there is an earlier point where \(\varphi_1\) is true. We can decompose this reasoning as follows:

• either \(\varphi_1\) is guessed to be true already before the interval begins (the blue rectangles in the figure), in which case the obligation can be discharged after generating one for \(\varphi_1\),

• or the obligation has entered the interval and starts to check \(\varphi_2\) at each position; if additionally, \(\varphi_1\) is guessed to be true at some position inside the interval, then the obligation can be discharged.

We use the notation \(x < I\) to mean the value of \(x\) is strictly less than every point in the interval. Let \(l\) be the left end-point of \(I\). We will write \(l \triangleleft_I x\) to indicate that \(l \le x\) when \(I\) is left-closed, and \(l < x\) when \(I\) is left open (essentially, the lower bound of \(I\) is satisfied by \(x\)).

For an obligation \(\theta\), we will write \(\theta \xrightarrow{\delta, a} \Theta'\) in short for a sequence of a delay followed by action: \(\theta \xrightarrow{\delta} \{\theta'\}\) and \(\theta' \xrightarrow{a} \Theta'\). We now extend the definition of transitions to obligation-sets.

Minimal extensions ensure that the resulting obligation-sets do not contain two different guesses at a position for the same formula. This motivates us the following definition which generalizes this idea.

These definitions lead us to the final transition system of obligations. Nodes in this transition system contain well-formed obligation-sets. Infinite runs in this transition system correspond to infinite words, and the node visited after position \(i\) in the word represents the obligations at \(i\). Figure 2 depicts two formulas and a run of the obligation graph for each of them. Example 2 in Appendix 8 gives a more detailed description.

Accepting runs are those where every Until obligation that is generated is eventually discharged. To implement this accepting condition, we add identifiers to every Until obligation and define a generalized Büchi acceptance condition based on these identifiers. In Figure 2, obligations for formulas \(\varphi\), \(\varphi_1\), and \(\psi\) are annotated below with the formula followed by a number. These are the identifiers of the respective obligations. The journey of an obligation can be conveniently tracked using its identifier. For example, we can see that \(\varphi_1 \cdot 1\) is created at position \(2\) of the word, and travels until it is discharged at position \(6\).

In the definition below, we make use of these notations: (1) given an obligation-set \(\Theta\) and a \(\delta \ge 0\) s.t. all waiting times of obligations in \(\Theta\) are at least \(\delta\), we define \(\Theta + \delta = \{ \theta + \delta \mid \theta \in \Theta \}\); (2) given an obligation \(\theta = (\psi, x, t)\) s.t. \(x \ge \delta\), we define \(\theta - \delta:= (\psi, x - \delta, t + \delta)\). In the obligation graph below, we choose a natural naming convention where each fresh obligation is assigned the smallest available identifier of its type.

The acceptance condition essentially mimicks the fact that every \(\mathcal{U}_I\) obligation that is generated is eventually discharged. When a new Until obligation arrives, a new identifier, say \(\psi \cdot i\) is assigned to it. When it is discharged, \(\psi \cdot i\) becomes inactive (notice the way we have defined \(\mathsf{id}'\)). Therefore, the acceptance condition amounts to verifying whether each identifier becomes inactive infinitely often. For Dual Until obligations, there is nothing to check.

For a timed word \(w = (a_1, \tau_1) (a_2, \tau_2) \cdots\), a run of \(w\) on \(\mathsf{Obl}(\varphi)\) from a node \((\Theta, \mathsf{id})\) is an infinite sequence \((\Theta, \mathsf{id}) \xrightarrow{\delta_1, a_1} (\Theta_1, \mathsf{id}_1) \xrightarrow{\delta_2, a_2} \cdots\) where \(\delta_i = \tau_i - \tau_{i-1}\) for all \(i \ge 1\), and taking \(\tau_0 = 0\). Since \(\mathsf{Obl}(\varphi)\) is non-deterministic, there could be several runs for \(w\). A run is said to be accepting if it satisfies the generalized Büchi condition given by \(\mathsf{Acc}(\varphi)\): for every Until subformula \(\psi\) and every \(i \ge 0\), \(F_\psi^i\) should be visited infinitely often. In other words, every time there appears an Until obligation with identifier \(\psi \cdot i\), there should be a later point in the run where it disappears. We say a word \(w\) is accepting from a node if it has some accepting run in \(\mathsf{Obl}(\varphi)\) from this node, and define the language of a node as the set of accepting words from that node. For the graph \(\mathsf{Obl}(\varphi)\), we define the language of \(\mathsf{Obl}(\varphi)\) as \(L(\mathsf{Obl}(\varphi)) = L(\operatorname{init}_{\varphi})\).

5 Reduced obligation graph↩︎

When there are multiple obligations of the same type in a node of \(\mathsf{Obl}(\varphi)\) we can eliminate or merge some of them.

In this section, we will provide optimization rules that will ensure that there is a bound \(k_{\psi}\) such that every node has at most \(k_\psi\) obligations for a given MITL formula \(\psi\), while still preserving the language of the obligation transition system. The optimization rules depend on the type of the obligations, whether they are \(\mathcal{U}_I\) or \(\widetilde{\mathcal{U}}_I\), and within each category, whether \(I\) is bounded or not.

Until with a bounded interval.

We start with the case of an Until formula with a bounded interval \(I\) which is typically the most difficult in all existing constructions. Let \(l, u\) be the left and right endpoints of \(I\). Let \(\Theta\) be a obligation-set containing the following two obligations, one of them having been freshly created with age \(0\): \[\begin{align} \theta_1 = (\varphi_1 \mathcal{U}_I \varphi_2, x_1, t_1) \qquad \theta_2 = (\varphi_1 \mathcal{U}_I \varphi_2, 0, t_2) \end{align}\] From the semantics of obligations, there was a position \(i_1\) earlier in the word which generated \(\theta_1\). The time that has elapsed ever since is \(x_1\), and the time left for the witness to appear is \(t_1\). Let \(i_2 > i_1\) be the position in the word when \(\theta_2\) was generated. Firstly, note that \(t_2 \in I\) since the initial guess made should lie in \(I\). The next two simple rules exhibit when we can keep only one obligation.

Remove-new

if \(t_1 \in I\), remove \(\theta_2\).

Modify-old

else, if \(x_1 + t_2 \in I\), update \(\theta_1\) to \((\varphi_1 \mathcal{U}_I \varphi_2, x_1, t_2)\) (the waiting time has been modified from \(t_1\) to \(t_2\)) and remove \(\theta_2\).

Intuitively, when \(t_1 \in I\), the witness guessed by \(\theta_1\) at position \(i_1\) is already a witness for position \(i_2\), and hence the presence of obligation \(\theta_1\) is sufficient for the satisfaction of \(\varphi_1 \mathcal{U}_I \varphi_2\) at position \(i_2\). In some sense, \(\theta_1\) covers for \(\theta_2\). For the Modify-oldcase: when \(x_1 + t_2 \in I\), observe that the witness guessed by \(\theta_2\) is a witness for position \(i_1\) as well. Therefore it is unnecessary to maintain two different guesses and hence we modify \(\theta_1\) to a new \(\theta_1'\) that points to the guess made by \(\theta_2\). When \(\theta'_1\) is finally discharged, we verify the guesses made both at \(i_1\) and at \(i_2\): both \(\theta_1\) and \(\theta_2\) are covered by \(\theta'_1\).

Here is a technical point crucial for the correctness of the approach. Suppose \(\theta_1\) covers \(\theta_2\) leading to Remove-newrule applied to eliminate \(\theta_2\). Further down the line, it may so happen that \(\theta_1\) is modified to obligation \(\theta'_1\). It turns out that this new \(\theta'_1\) also covers the previously removed obligation \(\theta_2\), and hence does not contradict our previous decision to remove \(\theta_2\). We illustrate this idea in the figure below. Assume \(\theta_1\) is generated at point \(i_1\) and it guesses a witness at point \(j_1\) inside the required interval. When \(i_2\) is encountered, Remove-newis applied. Hence \(j_1\) continues to be a witness for \(i_2\). Now, when \(i_3\) is seen, Modify-oldrule is applied to ascertain that \(j_3\) is a witness for \(i_1\) and hence \(\theta_1\) is updated to point to \(j_3\). We claim that \(j_3\) is a witness for \(i_2\) as well: since \(j_3\) satisfies the upper bound timing constraint wrt \(i_1\), it satisfies the upper bound constraint wrt \(i_2\); since \(j_3\) satisfies lower bound constraint wrt \(i_3\), we deduce that it satisfies the lower bound constraint wrt \(i_2\).

Bound on the number of obligations when \(I\) is non-singular. Let us now see how the two rules ensure a bound on the number of \(\mathcal{U}_I\) obligations. For simplicity, assume \(I = [l,u]\), a closed interval, and let \(\psi = \varphi_1 \mathcal{U}_I \varphi_2\). The key observation that helps in getting a bound for MITL is the following. When neither Remove-newnor Modify-oldis applicable on \(\theta_1= (\psi,x_1,t_1)\) and \(\theta_2 = (\psi,0,t_2)\), we will have: \[\begin{align} \label{eq:until-elimination-keep-both} t_1 < l \qquad \text{ and } \qquad x_1 + t_2 > u \end{align}\tag{1}\] This is because: initially all timers are initiated with a value in \([l,u]\). As \(t_1 \notin I\) (due to Remove-newnot being applicable), sufficient time has elapsed since it was generated and its value satisfies \(t_1 < l\). Similarly if \(x_1 + t_2 \notin I\) (due to Modify-oldnot being applicable) it means \(x_1 + t_2 > u\) since we know that \(t_2 \in I\) and \(x_1 \ge 0\). Now, consider an obligation-set that has three obligations of type \(\psi\), say \(\theta_1,\theta_2,\theta_3\) for \(\theta_i = (\psi,x_i,t_i)\). Assuming \(x_1 > x_2 > x_3\), we see that when the second obligation was newly created, the obligation-set had two obligations \(\theta_1 - x_2 = (\psi,x_1-x_2,t_1+x_2)\) and \(\theta_2 - x_2 = (\psi,0,t_2+x_2)\), and as they were both kept in the obligation-set, by 1 we know that \[\begin{align} t_1 + x_2 < l \quad \text{ and } \quad (x_1 - x_2) + (t_2 + x_2) = x_1 + t_2 > u \end{align}\] Similarly, we see that when the third obligation was newly created, the obligation-set contained \(\theta_2-x_3 = (\psi,x_2-x_3,t_2+x_3)\) and \(\theta_3-x_3 = (\psi,0,t_3+x_3)\), and by 1 : \[\begin{align} t_2 + x_3 < l \quad \text{ and } \quad x_2 + t_3 > u \end{align}\] Combining \(x_1 + t_2 > u\) and \(t_2 + x_3 < l\) gives \[\begin{align} x_1 - x_3 > u- l \end{align}\]

In summary: after the first two obligations for \(\varphi_1 \mathcal{U}_I \varphi_2\), a third one needs to be stored only after \(|I|\) time units. By this time the waiting time for the first obligation has come down to \(< I\). This allows us to deduce that while the first obligation is still alive, at most \(2 \times \lceil \frac{u}{u-l} \rceil\) obligations will be stored. Rewriting \(u = l + (u - l)\) and \(\kappa = \lceil \frac{l}{u-l} \rceil + 1\), we see that atmost \(2 \kappa\) obligations for \(\varphi_1 \mathcal{U}_{I} \varphi_2\) need to be stored in any node.

Until with an unbounded interval.

Now consider the case when \(I\) is unbounded, that is of the form \([l, \infty)\) or \((l, \infty)\). An Until obligation \((\varphi_1 \mathcal{U}_I \varphi_2, x, \bot)\) with \(I\) unbounded gets discharged at a point where \(l \le x\) (when \(I\) is left-closed) and \(l < x\) (when \(I\) is left-open). Suppose we have two obligations active in some obligation-set: \[\begin{align} \theta_1 = (\varphi_1 \mathcal{U}_I \varphi_2, x_1, \bot) \qquad \text{ and } \qquad \theta_2 = (\varphi_1 \mathcal{U}_I \varphi_2, x_2, \bot) \qquad \text{ s.t. } \qquad x_1 > x_2 \end{align}\] Clearly, if \(x_2 \in I\), then \(x_1 \in I\) too. Therefore a position where \(\theta_2\) finds a witness is also a witness position for \(\theta_1\). Hence we are tempted to remove \(\theta_1\). This way, we store only a single obligation for Until with an unbounded interval. However there is a problem if we do this repeatedly: if we continue to remove the older obligation and store only the newest one, there may never be a position where an obligation is actually discharged. We may continue to keep postponing the obligations. To eliminate this situation, we adopt a different strategy where we store two obligations.

Let \(\psi = \varphi_1 \mathcal{U}_I \varphi_2\) with \(I\) unbounded. Suppose \(\theta_1\) is the first obligation of type \(\psi\) that appears in the run. We will never discard it until it is discharged. When a second obligation appears later, say \(\theta_2\), we maintain \(\{ \theta_1, \theta_2 \}\). Now, when a third obligation appears, say \(\theta_3\), we replace \(\theta_2\) with \(\theta_3\) to obtain \(\{\theta_1, \theta_3\}\). Therefore, until \(\theta_1\) gets discharged, the second obligation may keep getting replaced. Suppose \(\theta_1\) gets discharged when the obligation-set is \(\{\theta_1, \theta_k\}\). Now \(\theta_k\) takes the role of \(\theta_1\), and so on. Using this strategy, we can enforce every \(\psi\)-obligation generated is ultimately asserted.

The above idea can naturally be implemented by storing up to two obligations at each point: the earliest generated, and the latest generated, which can be determined by looking at the ages. In other words, if there are three or more obligations containing the same \(\mathcal{U}_I\) formula with \(I\) unbounded, we store two obligations, one with the largest value of the age, and the other with the smallest value of the age (since our obligations are well-formed, we would never have two obligations of the same type having the same age) and remove the rest.

Dual Until.

For Dual until, the optimization merges two obligations into one. We start with the case when \(I\) is a bounded interval, with left end-point \(l\) and right end-point \(u\). From the semantics, a dual Until obligation \(\theta_1 = (\varphi_1 \widetilde{\mathcal{U}}_I \varphi_2, x_1, t_1)\) refers to an interval with end-points \(l - x_1\) and \(u - x_1\). When a fresh obligation \((\varphi_1 \widetilde{\mathcal{U}}_I \varphi_2, 0, u)\) appears, we check whether its corresponding interval with endpoints \(l\) and \(u\) overlap with the former: this will happen when either \(l < u - x_1\), or when \(l = u - x_1\) and \(I\) is either left-closed or right-closed (see figure below):

More succinctly put, here is the definition for the function:

Merge-overlapping

if \(t_1 \in I\), remove \(\theta_1, \theta_2\) and add a merged obligation \(\theta = (\varphi_1 \mathcal{U}_I \varphi_2, x_1, u)\)

Essentially, the life of the merged obligation is prolonged to cover the intervals represented by both \(\theta_1\) and \(\theta_2\). This explains the correctness of the merge. For the bound, let us look at two obligations \(\theta_1 = (\varphi_1 \widetilde{\mathcal{U}}_I \varphi_2,x_1,t_1)\) and \(\theta_2 = (\varphi_1 \widetilde{\mathcal{U}}_I \varphi_2,0,u)\) (a freshly created obligation). When both \(\theta_1\) and \(\theta_2\) remain even after applying the Merge-overlappingrule, it means that \(t_1 < I\), and since it was started at \(u\), it implies that \(x_1\) is at least \(|I|\). Hence, the time between these two obligations is at least \(|I|\). Moreover, since \(t_1 < I\), this obligation is alive only upto \(l\) time units, and the number of new obligations that can get generated when it is alive is at most \(1 + \lceil \frac{l}{|I|} \rceil\).

Finally, we consider the case when \(I\) is unbounded. Here the interval corresponding to every fresh obligation will overlap with the previous one. Hence we can always merge: or in other words, any fresh obligation can be removed. Therefore, there will be at most one dual until obligation stored for formulas with an unbounded interval.

The \(\mathsf{Optimize}\) function and the reduced obligation graph.

We formalize the rules mentioned above into an \(\mathsf{Optimize}\) function. Given a node \((\Theta, \mathsf{id})\) of the obligation graph \(\mathsf{Obl}(\varphi)\), we define a function \(\mathsf{Optimize}(\Theta, \mathsf{id})\) which returns a new node \((\Theta_{\mathsf{opt}}, \mathsf{id}_{\mathsf{opt}})\) with potentially fewer obligations. Optimization is performed for each type independently: for each \(\psi \in \mathsf{type}(\Theta)\), the \(\mathsf{Optimize}\) function restricts \(\Theta\) to obligations of type \(\psi\) and applies the rules corresponding to \(\psi\) (whether \(\mathcal{U}_I, \widetilde{\mathcal{U}}_I\), \(I\) bounded or unbounded) to this set. Using \(\mathsf{Optimize}\) we are able to define a reduced obligation graph which is shown to be correct, and also containing a bounded number of obligations (details in Appendix 9).

We can now state the two main theorems of this section: the first one says that the optimization rules are correct for any MTL formula, the second one states that for MITL this results in a graph where there are a bounded number of obligations in each node.

6 Symbolic computation↩︎

The goal of this section is to develop a finite abstraction of the reduced obligation graph \(\mathsf{Obl}^{\mathsf{red}}(\varphi)\) corresponding to an MITL formula \(\varphi\). The idea is to adapt the standard region equivalence studied for timed automata [14] in this context of obligations. The region equivalence is known to be a (time-abstract) bisimulation¹ on the space of configurations of a timed automaton, and its finite quotient called the region graph is a sound and complete abstraction of the timed automaton semantics.

The main challenge in our context lies in handling timer variables which move in an opposite direction to clocks, and it is known that for generalized timed automata (GTA) which contain both kinds of clocks (standard clocks and timers), there is in general no finite (time-abstract) bisimulation [15]. Here is a brief idea why this is so. The region equivalence is parameterized by a constant \(M \in \mathbb{N}\). For a clock, once it goes beyond \(M\), its actual value does not matter and can be abstracted into one chunk. However, for a timer, consider two different values \(M + 1\) and \(M + 2\). On a time elapse of \(1\), the former comes to \(M\), whereas the latter is still larger than \(M\). Hence equating \(M+1\) and \(M+2\) is incorrect for timers. In our case, this does not happen since our timer variables are always bounded by design and are never above the maximum constant. We develop an equivalence relation which intuitively corresponds to applying the standard region equivalence when timer values are replaced by their negation. Note nevertheless that we will keep the semantics of timers as we defined (non-negative guessed value and decrease).

Fix an MITL formula \(\varphi\). Let \(M\) be the maximum constant appearing in the formula. For a timer \(t\) (assuming non-negative values), let \(\lceil t \rceil\) be the smallest integer greater than or equal to \(t\), and let \(\{ t \} = \lceil t \rceil - t\). For a clock \(x\), let \(\lfloor x \rfloor\) be the largest integer lesser than or equal to \(x\), and let \(\{ x \} = x - \lfloor x \rfloor\).

We can extend the equivalence to nodes: \((\Theta, \mathsf{id}) \simeq_M (\Theta', \mathsf{id}')\) if \(\Theta \simeq_M \Theta'\) by a bijection \(h\), and for any \(\theta \in \Theta\), \(\mathsf{id}(\theta) = \mathsf{id}'(h(\theta))\). We will write \([(\Theta, \mathsf{id})]_M\) for the equivalence class of \((\Theta, \mathsf{id})\) w.r.t. \(\simeq_M\).

This leads us to the definition of a region graph over obligations. We will call the equivalence classes as obligation-regions and its quotient as the obligation-region graph.

The acceptance condition is adapted from \(\mathsf{Obl}^{\mathsf{red}}(\varphi)\). For every bounded Until subformula \(\psi\) of \(\varphi\), the number of obligations containing \(\psi\) in any obligation-region is atmost \(k_\psi\) (the bound of Theorem [thm:red-bdd-mitl]). For \(1 \le i \le k_\psi\), let \(G_{\psi}^i\) be the set \([(\Theta, \mathsf{id})]_M\) s.t. \((\Theta, \mathsf{id}) \in F_{\psi}^i\) (coming from Definition 10). An infinite run of the obligation region-graph is said to be accepting if for every bounded Until formula \(\psi\) and every \(1 \le i \le k_\psi\), some node in \(G_\psi^i\) appears infinitely often. This is a standard generalized Büchi condition.

Recall that satisfiability of \(\varphi\) is the question of checking whether there exists a non-Zeno word satisfying \(\varphi\). We can encode non-Zenoness using an MITL formula \(\phi_{nz} := \mathbf{G}(\top \implies \mathbf{F}_{[1, \infty)} \top)\). Hence satisfiability of \(\varphi\) reduces to checking whether there is an accepting run in the obligation-region graph of \(\varphi \land \phi_{nz}\). Thanks to Theorem [thm:red-bdd-mitl], each node of the obligation-region graph requires at most exponential space and the size of the obligation-region graph is at most doubly exponential in the formula, when constants are encoded in binary. When constants are encoded in unary, each node requires polynomial space and the graph is at most singly-exponential in the formula. Hence, we get the following corollary.

Note that the EXPSPACE upper bound coincides with the result of [7], as well as the PSPACE upper bound for MITL\(_{0,\infty}\). We did not find the other PSPACE upper bound mentioned in the previous literature. These complexity results are optimal, in the sense that the satisfiability problem for MITL is known to be EXPSPACE-hard, and the other logics encompass LTL, so PSPACE is optimal.

7 Conclusion↩︎

We have presented an alternate approach to MITL satisfiability. In spite of its long history, there has been a recent flurry of activity in MITL satisfiability as witnessed by two new orthogonal approaches leading to mature tools [11], [13]. We believe our approach complements the existing approaches and we hope that some of the insights we develop here could benefit the other approaches too. Both the existing tools for MITL started with a “seed” laying the foundations: [8], [9] for the tool MightyL and its successor MightyPPL, and [12] for TEMPORA. In our perspective, we view the current work as the seed for further investigations into this approach. Therefore, a natural future direction is the study of zone-based algorithms and tool development based on our simple obligations for MITL.

8 Appendix for Section 4↩︎

Before turning to the proof of Theorem [thm:oblcorr], we state three useful lemmas whose proofs follow from the definitions. We let \(\varphi\) be an MTL formula, and consider its obligation graph \(\mathsf{Obl}(\varphi)\). In these lemmas, we use all notations that were previously defined.

Basically, a join of two runs is a union of runs, where some obligations are removed to only have well-formed obligation-sets. Identifiers need to be adapted.

9 Appendix for Section 5↩︎

9.1 Reduced Obligation Graph↩︎

Consider an obligation graph \(\mathsf{Obl}(\varphi)\) for an MTL formula \(\varphi\). Given a node \((\Theta, \mathsf{id})\) we define a function \(\mathsf{Optimize}(\Theta, \mathsf{id})\) which returns a new node \((\Theta_{\mathsf{opt}}, \mathsf{id}_{\mathsf{opt}})\) with potentially fewer obligations than \(\Theta\), and a possibly changed naming function. For each subformula \(\psi\) of \(\varphi\) containing an \(\mathcal{U}_I\) or a \(\widetilde{\mathcal{U}}_I\) operator, assume there are \(\ell_\psi \ge 0\) obligations of type \(\psi\) in \(\Theta\). The number \(\ell_\psi\) can well be \(0\). When \(\ell_\psi > 0\), let the corresponding obligations be called: \(\theta^\psi_i = (\psi, x^\psi_i, t^\psi_i)\) for \(1 \le i \le \ell_{\psi}\). Since \(\Theta\) is well-formed, we can assume that the ages are distinct, and furthermore, for convenience, assume: \(x^\psi_{\ell_\psi} < x^{\psi}_{\ell_\psi - 1} < \cdots < x^\psi_2 < x^\psi_1\): the obligations were produced in increasing order of their indices, and hence the one with the largest index has the smallest age. The reduction rules depend on the type of \(\psi\). We make use of this notation: for an obligation-set \(\Theta\) and a formula \(\psi\), we write \(\Theta^\psi\) for the set of obligations of type \(\psi\) present in \(\Theta\).

9.2 Proof of Theorem [thm:oblredcorr]↩︎

We will first prove that if \(w = (a_1,\tau_1) (a_2,\tau_2) \dots\) has an accepting run in \(\mathsf{Obl}^{\mathsf{red}}(\varphi)\), then it has an accepting run in \(\mathsf{Obl}(\varphi)\).

Consider an accepting run for \(w\) in \(\mathsf{Obl}^{\mathsf{red}}(\varphi)\) of the following form, with \(\delta_i = \tau_i - \tau_{i-1}\) (taking \(\tau_0 = 0\)): \[\begin{align} \rho:= \operatorname{init}_\varphi \xRightarrow{(\delta_1, a_1)} (\Theta_1, \mathsf{id}_1) \xRightarrow{\delta_2, a_2} (\Theta_2, \mathsf{id}_2) \cdots \end{align}\] Firstly, we know that for every transition \((\Theta_{j-1}, \mathsf{id}_{j-1}) \xRightarrow{\delta_j, a_j} (\Theta_j, \mathsf{id}_j)\) of \(\rho\) there is a transition \((\Theta_{j-1}, \mathsf{id}_{j-1}) \xrightarrow{\delta_j, a_j} (\overline{\Theta}_{j}, \overline{\mathsf{id}}_j)\) in \(\mathsf{Obl}(\varphi)\) that was optimized to get the resulting node in the reduced graph. We call this transition:

\[\begin{align} \label{eq:original-transition} e_j: (\Theta_{j-1}, \mathsf{id}_{j-1}) \xrightarrow{\delta_j, a_j} (\overline{\Theta}_{j}, \overline{\mathsf{id}}_j) \end{align}\tag{2}\]

Another thing to observe is as follows:

We can now define the notion of a guess being a good witness for a bounded until subformula and some position, according to the run \(\rho\):

Good witnesses for bounded Until.

From Lemma 4, there is at most one obligation \((\psi, x, t) \in \Theta_j\) such that \(t \in I\). Let its identifier be \(\psi \cdot k\), i.e., \(\mathsf{id}_j(\psi, x, t) = \psi \cdot k\). Since \(\rho\) is an accepting run, there is a least index \(m > j\) s.t. \(k \notin \mathsf{range}(\psi, \mathsf{id}_m)\). Define \(\tau^\psi_j = \tau_m - \tau_j\).

Now, using \(\rho\) and the observations above, we will construct \((\Theta'_i, \mathsf{id}'_i)\) for all \(i \ge 1\) and claim that the following is an accepting run of \(\mathsf{Obl}(\varphi)\): \[\begin{align} \rho':= \operatorname{init}_\varphi \xrightarrow{(\delta_1, a_1)} (\Theta'_1, \mathsf{id}'_1) \xrightarrow{\delta_2, a_2} (\Theta'_2, \mathsf{id}'_2) \cdots \end{align}\] We will construct this run such that for every node \((\Theta'_i, \mathsf{id}'_i)\) and subformula \(\psi\) where \(\psi\) is a bounded until subformula, if \((\psi,0,t) \in \Theta'_i\), then \(t = \tau^\psi_i\). In addition, for each \(i \ge 1\), we will define a mapping \(h_{i}: \Theta'_{i} \mapsto \Theta_{i}\) such that for every \(\theta' \in \Theta'_i = (\psi',x',t')\), if \(h_i(\theta') = (\psi,x,t)\), then \(\psi=\psi'\). Intuitively, \(h_i(\theta')\) gives the obligation \(\theta\) in the reduced graph such that: if \(\theta\) is satisfied, then \(\theta'\) will also be satisfied. As we inductively build the run \(\rho'\), the mapping \(h_i\) will help us define the required successor \((\Theta'_{i+1}, \mathsf{id}'_{i+1})\).

Initial construction.

Firstly, we see that both \(\rho\) and \(\rho'\) will have \(\operatorname{init}_{\varphi}\) as the initial node. Also, because initial obligation-sets for a subformula have at most one obligation of that subformula, and \(\overline{\Theta}_{1}\) is well-formed, \(\mathsf{Optimize}(\overline{\Theta}_1,\overline{\mathsf{id}}_1) = (\overline{\Theta}_1,\overline{\mathsf{id}}_1)\). Thus, we can define \((\Theta'_1,\mathsf{id}'_1) = (\overline{\Theta}_1,\overline{\mathsf{id}}_1)\) itself, with \(h_1\) being the identity function.

Now, assuming we have constructed \((\Theta'_i, \mathsf{id}'_i)\) and we have the function \(h_i\), satisfying the required properties, we will see how to define \((\Theta'_{i+1},\mathsf{id}'_{i+1})\) and \(h_{i+1}\).

Delay transition.

We need to first prove that the delay \(\delta_{i+1}\) is possible from \((\Theta'_i,\mathsf{id}'_i)\). To do so, we see that for every bounded until \(\psi\) type obligation present in \(\Theta'_i\), at the time it was created, its waiting time was set as \(\tau^\psi_j\) for some \(j \leq i\), where \(\tau^\psi_j = \delta_{j+1} + \dots + \delta_k\), \(k > j\). This means that if such an obligation is present in \(\Theta'_i\), its waiting time is either exactly \(\delta_{i+1}\), or is greater than \(\delta_{i+1}\). This means the node \((\Theta'_i,\mathsf{id}'_i) + \delta_{i+1}\) is defined.

Constructing \((\Theta'_{i+1},\mathsf{id}'_{i+1})\).

We will use the transition in Equation \(\eqref{eq:original-transition}\) and \(h_{i}\) to decide the transitions picked for the obligations of \(\Theta'_{i} + \delta_{i+1}\). Looking at some \(\theta' \in \Theta'_i\), where \(h_{i}(\theta') = \theta\) for \(\theta = (\psi,x,t)\), we will look at the \((\delta_{i+1},a_{i+1})\)-extension of \(\theta\) in transition \(e_{i+1}\eqref{eq:original-transition}\).

• If \(\theta+\delta_{i+1}\) is present in \(\Theta''_{i+1}\), we will add \(\theta'+\delta_{i+1}\) to \(\Theta'_{i+1}\) and define \(\mathsf{id}'_{i+1}(\theta'+\delta_{i+1}) = \mathsf{id}'_{i}(\theta')\).

• If a ‘new’ obligation of type \(\psi'\), i.e. of the form \((\psi',0,t')\) is present in \(\overline{\Theta}_{i+1}\):

  • If \(\psi'\) is a bounded until subformula, we will add \((\psi',0,t'')\) to \(\Theta'_{i+1}\), where \(t'' = \tau^{\psi'}_{i+1}\). We will set \(\mathsf{id}'_{i+1}\) of this new obligation by picking the next available id for type \(\psi'\).

  • If \(\psi'\) is not a bounded until subformula, we will simply add \((\psi',0,t')\) to \(\Theta'_{i+1}\) and set its id to the next available one of type \(\psi'\).

Notice that by our construction, as we add only one new obligation for each subformula type, we are getting a successor \(\Theta'_{i+1}\) that is well-formed provided \(\Theta'_i\) was well-formed.

Defining \(h_{i+1}\).

Given some \(\theta' \in \Theta'_{i+1}\), we define \(h_{i+1}(\theta')\) as follows:

• If \(\theta'\) is also present in \(\Theta_{i+1}\), we just define \(h_{i+1}(\theta') = \theta'\).

• If \(\theta'\) is not present in \(\Theta_{i+1}\), we look at the type of obligation \(\theta'\), say \(\psi'\):

  • If \(\psi'\) is a bounded until formula, we know from Lemma 4 that there will be a simple \(\theta \in \Theta_{i+1}\) such that the waiting time of \(\theta\) will be in the interval of \(\psi'\). We will define \(h_{i+1}(\theta') = \theta\) in this case.

  • If \(\psi'\) is an unbounded until subformula or a dual until subformula, we look at \(\theta = (\psi',x,t) \in \Theta_{i+1}\) such that \(x\) has the least value among other obligations of type \(\psi'\) and define \(h_{i+1}(\theta') = \theta\).

Now, the constructed run \(\rho'\) is an accepting run. This is because we define \(h_i\) for each position \(i\) which ensures that every obligation of type \(\psi\) in \((\Theta'_i,\mathsf{id}'_i)\) is mapped to a formula of type \(\psi\) in \((\Theta_i,\mathsf{id}_i)\). Also, the \(id\) functions are defined so that if \(\mathsf{id}'_i(\theta'_1) = \mathsf{id}'_{i+1}(\theta'_2)\) in \(\rho'\) and \(h_i(\theta'_1) = \theta_1\), \(h_{i+1}(\theta'_2) = \theta_2\), then \(\mathsf{id}_i(\theta_1) = \mathsf{id}_{i+1}(\theta_2)\). Finally, we know that \(\rho\) is an accepting run, meaning every until obligation with a certain id has some node later in the run without that id. Hence \(\rho'\) is also an accepting run.

We now prove the other direction, that if \(w\) has an accepting run in \(\mathsf{Obl}(\varphi)\), it has an accepting run in \(\mathsf{Obl}^{\mathsf{red}}(\varphi)\).

Consider an accepting run for \(w\) in \(\mathsf{Obl}(\varphi)\): \[\begin{align} \pi':= \operatorname{init}_\varphi \xrightarrow{(\delta_1, a_1)} (\Theta'_1, \mathsf{id}'_1) \xrightarrow{\delta_2, a_2} (\Theta'_2, \mathsf{id}'_2) \cdots \end{align}\] Similar to earlier, we will use this run to construct an accepting run \(\pi'\) for \(w\) on \(\mathsf{Obl}^{\mathsf{red}}(\varphi)\) of the form: \[\begin{align} \pi:= \operatorname{init}_\varphi \xRightarrow{(\delta_1, a_1)} (\Theta_1, \mathsf{id}_1) \xRightarrow{\delta_2, a_2} (\Theta_2, \mathsf{id}_2) \cdots \end{align}\] We will also require a mapping \(g_i\) from \(\Theta_i\) to \(\Theta'_i\) to guide the successor computation. As mentioned before, \(\mathsf{Optimize}(\Theta'_1,\mathsf{id}'_1) = (\Theta'_1,\mathsf{id}'_1)\), and so the run \(\operatorname{init}_\varphi \xRightarrow{\delta_1,a_1} (\Theta'_1,\mathsf{id}'_1)\) will remain the same in \(\pi'\). To get \((\Theta_{i+1},\mathsf{id}_{i+1})\) and \(g_{i+1}\) from \((\Theta_i,\mathsf{id}_i)\) and \(g_i\), we will simply apply the optimize function and use \(g_i\) to decide successors: for every obligation \(\theta \in \mathsf{Optimize}(\Theta'_i)\), the next transition for \(\theta\) will be the transition for \(g_i(\theta)\) in \((\Theta'_i,\mathsf{id}'_i) \xrightarrow{\delta_{i+1},a_{i+1}} (\Theta'_{i+1},\mathsf{id}'_{i+1})\), and so we will get \(\Theta_{i+1}\) and accordingly get \(\mathsf{id}_{i+1}\). We define \(g_{i+1}\) as follows, where \(\theta = (\psi,x,t)\) is some obligation in \(\mathsf{Optimize}(\Theta'_i,\mathsf{id}'_i)\):

• If \(\psi\) is an unbounded until subformula, we know that the optimization rules either eliminate formulas, and \(\theta\) will be present in \(\Theta'_{i+1}\) too, so we will define \(g_{i+1}(\theta)\) as that obligation.

• If \(\psi\) is an until subformula or a dual until subformula, we know from the optimization rules that either \(\theta\) will be present in \(\Theta'_{i+1}\), or there will at least one of the two obligations \(\theta_1 = (\psi,x,t')\) or \(\theta_2 = (\psi,x',t)\) for some \(x',t'\). We will define \(g_{i+1}(\theta)\) as \(\theta\) if it is present, or \(\theta_1\) if it is present, else as \(\theta_2\).

We can now see that the \(\pi'\) we construct is an accepting run, the proof being similar to our earlier reasoning: we define \(g_i\) for each position \(i\) which ensures that every obligation of type \(\psi\) in \((\Theta_i,\mathsf{id}_i)\) is mapped to a formula of type \(\psi\) in \((\Theta'_i,\mathsf{id}'_i)\).

9.3 Proof of Theorem [thm:red-bdd-mitl]↩︎

10 Appendix for Section 6↩︎

References↩︎

---

1. We recall that a time-abstract bisimulation is an equivalence relation on configurations, where delays are matched by possibly different delays while discrete labelled transitions are matched by similarly-labelled transitions.↩︎