We study translations from metric temporal logic (MTL) over the natural numbers to linear temporal logic (LTL). In particular, we present two approaches for translating from MTL to LTL which preserve the ExpSpace complexity of the satisfiability problem for MTL. In each of these approaches we consider the case where the mapping between states and time points is given by (i) a strict monotonic function and by (ii) a non-strict monotonic function (which allows multiple states to be mapped to the same time point). We use this logic to model examples from robotics, traffic management, and scheduling, discussing the effects of different modelling choices. Our translations allow us to utilise LTL solvers to solve satisfiability and we empirically compare the translations, showing in which cases one performs better than the other. We also define a branching-time version of the logic and provide translations into computation tree logic.
Hinweise
C. Dixon was partially supported by the EPSRC funded RAI Hubs FAIR-SPACE (EP/R026092/1) and RAIN (EP/R026084/1), and the EPSRC funded programme Grant S4 (EP/N007565/1)
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
1 Introduction
Linear and branching-time temporal logics have been used for a long time for the specification and verification of reactive systems. In linear-time temporal logic (LTL) [24, 48] we can, for example, express that a formula \(\psi \) holds now or at some point in the future using the formula \(\lozenge \psi \) (\(\psi \) holds eventually). However, some applications require not just that a formula \(\psi \) will hold eventually but that it holds within a particular time-frame, for example, between 3 and 7 moments from now.
To express such constraints, a range of Metric Temporal Logics (MTL) have been proposed [6, 7], considering different underlying models of time and operators allowed. MTL has been used to formalise vehicle routing problems [35], monitoring of algorithms [28, 53] and cyber-physical systems [2], among others. A survey about MTL and its fragments can be found in [46]. It is known that MTL over the reals is undecidable, though, decidable fragments have been investigated [5, 10, 12].
Anzeige
Here we consider MTL with pointwise semantics over the natural numbers, following [6], where each state in the sequence is mapped to a time point on a time line isomorphic to the natural numbers. In this instance of MTL, temporal operators are annotated with intervals, which can be finite or infinite. For example, \(\lozenge _{[3,7]}p\) means that p should hold in a state that occurs in the interval [3, 7] of time, while \(\Box _{[2,\infty )}p\) means that p should hold in all states that occur at least 2 moments from now. In contrast to LTL, where the time difference from one state to the next is always one, in MTL, time is allowed to irregularly ‘jump’ from one state to the next. The semantics uses a mapping from states to time points to keep track of the time difference between consecutive states. MTL formulae can then express constraints on such time differences. For example, using \(\Circle _{[2,2]} p\) we can state that the time difference from the current state to the next state is two while \(\Circle _{[3,\infty ]} p\) states that the next state is at least three moments from now.
Following Alur and Henzinger [6], the mapping between states and time points is given by a (weakly) monotonic function, which allows multiple states to be mapped to the same time point. Underlying this semantics is the so-called digital-clock assumption: different states that are associated with the same discrete clock record events happening between successive clock ticks. If no events occur over one or more successive clock ticks, no state will be associated with those clock ticks. In this work, we also consider the semantics where the mapping between states and time points is given by a strictly monotonic function, which forces time to progress from one state to another.
We provide two approaches for translating from MTL to LTL: in the first approach we introduce a fresh propositional variable that we call ‘gap’, which is used to encode the ‘jumps’ between states, as mentioned above; the second approach is inspired by [6], where fresh propositional variables encode time differences between states. In each approach we consider the case where the mapping between states and time points is given by: (i) a strict monotonic function and by (ii) a non-strict monotonic function (which allows multiple states to be mapped to the same time point). All translations are polynomial w.r.t. the largest constant occurring in an interval (although exponential in the size of the MTL formula assuming a binary encoding of the constants). Since the satisfiability problem for LTL is PSpace-complete [51], our translations preserve the ExpSpace complexity of the MTL satisfiability problem over the natural numbers [6]. We provide a range of examples from robotics, traffic management, and scheduling. We present and discuss different modelling choices and their effect, including the choice between strict and non-strict semantics as the basis for the formalisation of a domain.
The translations allow us to use existing LTL solvers to determine the satisfiability of MTL formulae. To the best of our knowledge, there are no implementations of solvers for MTL with pointwise discrete semantics. We use several LTL solvers, covering a wide range of calculi and methods, to experimentally investigate the properties of the LTL formulae resulting from the translation of MTL formulae. We provide experimental results for both the modelled examples and we propose specific formulae to investigate and analyse the difference between the translations and provers.
Anzeige
Finally we consider a branching-time version of MTL and provide a translation into Computation Tree Logic (CTL) using the gap translation.
Our contributions are:
translations from MTL to LTL which preserve the ExpSpace complexity of the MTL satisfiability problem and allow the use of LTL solvers to determine the satisfiability of MTL formulae;
an experimental analysis of the behaviour of LTL solvers on the resulting formulae;
encodings of problems from robotics, traffic management, and the classical multiprocessor job-shop scheduling problem [16, 27] into MTL, as examples of the kind of problems that can be solved using MTL;
discussions about the modelling of these examples that illuminate interesting aspects of MTL specifications; and
a translation from a branching-time version of the logic into CTL that gives a tight 2EXPTIME upper bound to the satisfiability problem.
This paper is a revised and extended version of [33]. It includes a range of examples specified in MTL, full proofs, full details, updated and extended experimental results, a branching-time version of the logic with its translation into CTL and a more comprehensive discussion of related work.
In Sect. 2 we provide the syntax and semantics of LTL and MTL. We provide a range of examples in Sect. 3 encoding problems in MTL from robotics, traffic management, and job-shop scheduling. Our translations from MTL to LTL are provided in Sects. 4 and 5. Experimental results are provided in Sects. 6 and 7. A branching-time version of the logic and its translation into CTL is given in Sect. 8. We discuss related work in Sect. 9 and provide concluding remarks in Sect. 10.
2 Preliminaries
We briefly state the syntax and semantics of LTL and MTL. Let \({\mathcal {P}}\) be a (countably infinite) set of propositional variables. Well formed formulae in LTL are formed according to the rule:
where \(p \in {\mathcal {P}} \). We often omit parentheses if there is no ambiguity. We denote by \(\Circle ^c\) a sequence of c next operators, i.e., \(\Circle ^0 \varphi =\varphi \) and \(\Circle ^{n+1} \varphi =\Circle \Circle ^n\varphi \), for every \(n \in \mathbb {N}\).
An LTL model or state sequence\(\sigma \) over \((\mathbb {N}, <)\) is an infinite sequence of states \(\sigma _i \subseteq {\mathcal {P}} \), \(i \in \mathbb {N}\). The semantics of LTL is defined as follows.
Further connectives can be defined as usual: \({\mathbf {true}} \equiv p\vee \lnot p\), \({\mathbf {false}} \equiv \lnot ({\mathbf {true}})\), \(\lozenge \varphi \equiv {\mathbf {true}} \mathbin {{\mathcal {U}}} \varphi \) and \(\Box \varphi \equiv \lnot \lozenge \lnot \varphi \). To simplify the presentation, we further use additional n-ary boolean operators. If \(S = \{\varphi _1,\ldots ,\varphi _n\}\) is a finite set of LTL formulae, then \(\oplus _{\le 1} S\), \(\oplus _{\ge 1} S\), and \(\oplus _{= 1} S\) resp., are LTL formulae. The semantics of such formulae is as follows. Let \(\sigma '\) be a state sequence and \(i\in \mathbb {N}\). Then, \((\sigma ',i)\models \oplus _{\le 1} S\) iff \((\sigma ',i)\models \varphi _j\) for at most one \(\varphi _j\in S\), \(1\le j\le n\). Analogously, \((\sigma ',i)\models \oplus _{\ge 1} S\) iff \((\sigma ',i)\models \varphi _j\) for at least one \(\varphi _j\in S\), \(1\le j\le n\); and \((\sigma ',i)\models \oplus _{= 1} S\) iff \((\sigma ',i)\models \oplus _{\ge 1} S\wedge \oplus _{\le 1} S\).
MTL formulae are constructed in a way similar to LTL, with the difference that temporal operators are now bounded by an interval I with natural numbers as end-points or \(\infty \) on the right side. Note that since we work with natural numbers as end-points we can assume w.l.o.g that all our intervals are of the form \([c_1,c_2]\) or \([c_1,\infty )\), where \(c_1,c_2 \in \mathbb {N}\). We sometimes write \(k\in j +[c_1,c_2]\) with the meaning that \(k\in [c_1+j,c_2+j]\). Well formed formulae in MTL are formed according to the rule:
where \(p \in {\mathcal {P}} \). A timed state sequence\(\rho = (\sigma ,\tau )\) over \((\mathbb {N}, <)\) is a pair consisting of an infinite sequence \(\sigma \) of states \(\sigma _i \subseteq {\mathcal {P}} \), \(i \in \mathbb {N}\), and a function \(\tau : \mathbb {N}\rightarrow \mathbb {N} \) that maps every i corresponding to the i-th state to a time point \(\tau (i)\) such that \(\tau (i) < \tau (i+1)\). A non-strict timed state sequence \(\rho = (\sigma ,\tau )\) over \((\mathbb {N}, <)\) is a pair consisting of an infinite sequence \(\sigma \) of states \(\sigma _i \subseteq {\mathcal {P}} \), \(i \in \mathbb {N}\), and a function \(\tau : \mathbb {N}\rightarrow \mathbb {N} \) that maps every i corresponding to the i-th state to a time point \(\tau (i)\) such that \(\tau (i) \le \tau (i+1)\). We assume w.l.o.g. that \(\tau (0) = 0\). The semantics of MTL is defined as follows:
Further connectives are defined as usual: \(\lozenge _{I} \varphi \equiv ({\mathbf {true}} \mathbin {{\mathcal {U}}_{I}}\varphi )\) and \(\Box _{I}\varphi \equiv \lnot \lozenge _{I}\lnot \varphi \). A timed state sequence \(\rho = (\sigma ,\tau )\) is a model of an MTL formula \(\varphi \) iff \((\rho ,0)\models \varphi \). An MTL formula \(\varphi \) is satisfiable iff there exists a model of \(\varphi \) and it is valid iff every timed state sequence is a model of it. To transform an MTL formula into Negation Normal Form, one uses the constrained dual until \(\mathbin {\tilde{{\mathcal {U}}}_{I}}\) operator [46], defined as \((\varphi \mathbin {\tilde{{\mathcal {U}}}_{I}} \psi ) \equiv \lnot (\lnot \varphi \mathbin {{\mathcal {U}}_{I}} \lnot \psi )\).
An MTL formula \(\varphi \) is in Negation Normal Form (NNF) iff the negation operator (\(\lnot \)) occurs only in front of propositional variables. One of the differences between MTL and LTL is that in LTL we have the equivalence \(\lnot (\Circle p) \equiv \Circle \lnot p\), whereas in MTL \(\lnot (\Circle _{[2,2]} p) \not \equiv \Circle _{[2,2]} \lnot p\). If \(\lnot (\Circle _{[2,2]} p)\) then either p does not occur in the next state or the next state does not occur with time difference two. We can express this as follows:
To see this, consider the formula \(\lnot (p\mathbin {{\mathcal {U}}_{[2,2]}}q)\). It is satisfied by a timed state sequence in which p never holds, state 0 is mapped to time point 0, state 1 is mapped to time point 1, and q only holds in state 2 which is mapped to time point 2. The formula is satisfied because p does not hold at state 0 or 1. However this timed state sequence does not satisfy \(\Box _{[2,2]} \lnot q \vee ((\lnot q)\mathbin {{\mathcal {U}}_{[2,2]}}(\lnot p\wedge \lnot q))\) as the eventuality of the second disjunct does not hold within the interval [2, 2]. Note that in LTL the equivalence holds. In our example, if we remove the intervals from the equivalence and interpret the timed state sequence as an LTL model we would have the LTL formula \(\Box \lnot q \vee ((\lnot q)\mathbin {{\mathcal {U}}} (\lnot p \wedge \lnot q))\) holding at state 0 as the eventuality of the second disjunct holds at state 0 and 1. The intervals in MTL prevent this.
An MTL formula \(\varphi \) is in Flat Normal Form (FNF) iff it is of the form \(p_0 \wedge \bigwedge _i \Box _{[0,\infty )}(p_i \rightarrow \psi _i)\) where \(p_0, p_i\) are propositional variables or \({\mathbf {true}} \) and \(\psi _i\) is either a formula of propositional logic or it is of the form \(\Circle _{I} \psi _1\), \(\psi _1 \mathbin {{\mathcal {U}}_{I}} \psi _2\) or \(\psi _1 \mathbin {\tilde{{\mathcal {U}}}_{I}} \psi _2\) where \(\psi _1, \psi _2\) are formulae of propositional logic.
One can transform an MTL formula into FNF by renaming subformulae with nested operators, as in [23, 55]. For example, assume that we are given the following MTL formula: \( \Circle _{[2,3]}(\lnot \Box _{[1,2]}q).\) We first transform our formula into NNF and obtain: \(\Circle _{[2,3]}(\lozenge _{[1,2]}\lnot q).\) We then transform it into FNF:
The transformations into NNF and FNF are satisfiability preserving and can be performed in polynomial time.
3 Examples
We consider a range of examples that can be represented using MTL relating to robotics, traffic management, and job-shop scheduling.
First we consider a scenario relating to foraging robots based on a state transition system with timing constraints relating how long robots can spend in each state searching for food, moving home, etc. We first model a single robot using the strict semantics with timing constraints on the next operators to indicate the change from one state to another. We discuss the difficulties with this modelling approach for multiple robots and show how the scenario can be re-modelled to represent multiple robots of the same type. Next we consider an example related to traffic management, in particular, to traffic lights, again with the strict semantics. This has two traffic lights that are not identical, modelled using until operators with timing constraints that enforce the correct order and timings of the traffic light colours. The third example formulates multiprocessor job-shop scheduling. We have multiple processors and show how this can be modelled using both the strict and non-strict semantics.
3.1 Foraging Robots
This example is based on the models for foraging robot swarms [38]. Robots are located in an arena with a “home” for them, they leave the home, carry out a random walk to locate “food”. If food is detected they move towards the food, attempt to grab it and return home. If food is not found or another robot grabs the detected food and the time for searching for food is over the robot will move home without food. The food is deposited at home and increases the overall energy of the swarm but searching for food decreases this energy. Here we focus on the timing constraints rather than energy. Initially we consider one robot and later we consider multiple robots. Robots can be in one of nine states:
\({\textit{resting}}\)
resting at home;
\({\textit{leavingHome}}\)
leaving home;
\({\textit{randomWalk}}\)
moving around looking for food;
\({\textit{moveToFood}}\)
moving towards food having located it;
\({\textit{scanArena}}\)
looking for food;
\({\textit{grabFood}}\)
attempting to grab food that has been found;
\({\textit{moveToHome}}\)
the robot moves home with food;
\({\textit{deposit}}\)
the robot deposits the food at home, and
\({\textit{homing}}\)
the robot moves home without food.
The state transition system representing their movement between states is shown in Fig. 1.
Fig. 1
State transition system for foraging robots
×
There are three parameters: the maximum time \(T_r\) that can be spent resting, the maximum time \(T_s\) that can be spent searching for food (\({\textit{leavingHome}}\), \({\textit{randomWalk}}\), \({\textit{scanArena}}\), and \({\textit{moveToFood}}\)), and the maximum time \(T_d\) to get home with or without food (\({\textit{moveToHome}}\) and \({\textit{homing}}\)). The latter is based on an assumption that there is a maximum distance between the food and home. We assume that \({\textit{grabFood}}\) and \({\textit{leavingHome}}\) takes between two and three time units and \({\textit{deposit}}\) takes three to four time units. Initially the robot is resting (\({\textit{resting}}\)). Next we specify that the robot must be in exactly one of the states at any moment. Let
The variable \({\textit{searching}}\) holds in all the states \({\textit{leavingHome}}\), \({\textit{randomWalk}}\), \({\textit{scanArena}}\), \({\textit{moveToFood}}\) and nowhere else.
Here the highest value y for which we can prove this property is the minimum time the robot needs to return home.
For a single robot, we believe that the most natural way to represent the foraging robot scenario is as above, with most timing constraints on the next operator. However, to represent multiple robots we would need a copy of each state and the formulae representing the transitions for each robot, i.e. propositions such as \({\textit{resting}}\) and \({\textit{grabFood}}\) would be parameterised by robot number (for example \({\textit{resting}}_i\) and \({\textit{grabFood}}_i\) for robot i). In this type of scenario and modelling, the next operator is working as a synchronisation point: all robots must move into another state together. In general, this does not accurately reflect the intended behaviour of robots as some robots may stay in the state they are currently in whilst others may change state. A potential solution to this would be to include the current state of the robot on the right hand side of the formulae under a next operator, as follows
so that the robots do not have to change state at the same time. However this introduces other issues as the robot can now stay in the resting state for longer than \(T_r\) time units.
To model this correctly we would need to adopt an approach more like how we have dealt with the timings for searching, i.e. formulae for each transition in the state transition system, one denoting the possible next states and one denoting the required timing constraints to move out of the current state [like Eq. (1)]. We also need to introduce a new propositional variable for each robot, for each state, to denote the place where the proposition for that state changes from being false to becoming true. We need this so we can identify when we first entered some state so we can formalise the maximum time we can stay in this state. To illustrate this approach, we focus on the state \({\textit{resting}}_i\) in the following. Here, we denote the new propositional variable that indicates a state change by \({\textit{startResting}}_i\) and impose the following constraint on it.
Next, for robot i, to represent the transition out of the state \({\textit{resting}}{_i}\) we would have the following formulae, the first denoting the next possible states of robot i and the second enforcing the maximum time that robot i can be in the resting state.
Although we have introduced the proposition \({\textit{startResting}}_i\) to ensure the relevant timed formulae only hold from where \({\textit{resting}}_i\) first became true it is only essential here when the left hand side of the timing constraint is greater than one. Consider the following timed state sequence as an example. Let \(\rho = (\sigma ,\tau )\) be the timed state sequence where \( \tau (0) = 0, \tau (1) = 3\), \(\tau (2) = 4\), and \(\tau (3) = 10\) where \((\rho , 0) \models {\textit{resting}}_i\), \((\rho , 1) \models {\textit{resting}}_i\), \((\rho , 2) \models \lnot {\textit{resting}}_i\) and \((\rho , 3) \models \lnot {\textit{resting}}_i\). We consider using
In \(\rho \), \({\textit{resting}}_i\) changes from true to false within 3–5 time units from where \({{\textit{resting}}}_i\) was first true, as \(\tau (2)-\tau (0)\in [3,5]\). So
so (3) does not hold. But if we introduce \({\textit{startResting}}_i\) as defined in (2) then \((\rho , 0) \models {\textit{startResting}}_i\), \((\rho , 1) \models \lnot {\textit{startResting}}_i\), \((\rho , 2) \models \lnot {\textit{startResting}}_i\) and \((\rho , 3) \models \lnot {\textit{startResting}}_i\), and Eq. (4) holds as desired.
We discuss something similar in the next example in Sect. 3.2 relating to traffic lights about the proposition \(change_i\). Another solution to having multiple robots may be adopting the non-strict semantics in a similar way to what is presented for the multiprocessor job-shop scheduling problem in Sect. 3.3.
The timing aspects of other examples relating to robots could also be modelled. For example a personal robot assistant located in a house equipped with sensors that inform the robot about the state of the house and its participants is considered in [18, 19, 57]. The robot actions are controlled by a set of behaviours. These are of the form of “if ...then ...” where the “if” part depends on state of the robot, sensor data and internal variables and the “then” part contains a sequence of robot actions. These contain several timing aspects for example “wait ten seconds”, “wait an hour” etc that we could model using this logic.
3.2 Traffic Lights
Consider a pair of traffic lights at a junction with two roads, R1 and R2, crossing each other. Traffic light one is for road R1 and traffic light two is for road R2. As road R1 is busier, there is a camera to detect when there are cars waiting for traffic light 1. This makes the lights have different behaviour so the problem is not symmetric.
We use the following propositional variables to denote the states that the traffic lights and the detection sensor can be in:
\(r_i\)
traffic light i is at red;
\(a^r_i\)
traffic light i is at amber following being at red;
\(a^g_i\)
traffic light i is at amber following being at green;
\(a_i\)
traffic light i is at amber (i.e. one of the above holds);
\(g_i\)
traffic light i is at green;
detect
traffic light one detects cars waiting;
\(change_i\)
traffic light i has just changed colour;
Traffic light \(i \in \{1,2\}\) is exactly red, amber or green at every moment in time.
Traffic light \(i \in \{1,2\}\) is at amber if and only if either it is at amber after red or amber after green (at every moment in time). Note that while our modelling here does not explicitly allow the red and amber lights to both be on together, as is common in traffic light sequences in Europe, our use of two different propositional variables for amber after red and amber after green allows us to differentiate between these situations.
The sequence of the traffic lights is red, then amber, then green, then amber, then red, and so on. Both traffic lights eventually change to amber after having been at green, stay at amber after green between one and two time units before changing to red, and stay at amber after red between one and three time units before changing to green.
The formalisation of these constraints requires some careful consideration. For instance, one might consider the formula \(\Box _{[0,\infty )}(a^g_1\mathbin {{\mathcal {U}}_{[2,3]}} r_1)\) as a possible way of expressing that red follows amber after green within two or three time units. However, together with the constraints above, it is unsatisfiable: suppose there is a timed state sequence \(\rho = (\sigma ,\tau )\) that satisfies our constraints. For any \(i\in {\mathbb {N}}\), \((a^g_1\mathbin {{\mathcal {U}}_{[2,3]}} r_1)\) is true at \((\rho ,i)\) and there exists \(k\ge i\) with \(\tau (k)-\tau (i)\in [2,3]\) and \(r_1\) is true at \((\rho ,k)\). But since \((a^g_1\mathbin {{\mathcal {U}}_{[2,3]}} r_1)\) is always true, it is also true at \((\rho ,k)\) and since \(0\not \in [2,3]\), \(a^g_1\) must be true at \((\rho ,k)\). This contradicts the constraint that \(a^g_1\) and \(r_1\) cannot both be true at any state. In the following we make use of the proposition \(change_i\) together with a particular colour as a guard making sure that the timing constraints hold when a light changes to that colour.
The variable \(change_i\) holds in the first moment in time and also if the traffic light was not red, (respectively amber, green) in the previous moment and is now red (respectively amber, green).
Strictly, for a formula such as \(\Box _{[0,\infty )}(g_1\mathbin {{\mathcal {U}}_{[0,\infty )}}a^g_1)\), expressing that traffic light 1 stays green until it eventually changes to amber after green, where the lower bound on the interval restricting the until operator is 0, we do not need a guard, but add one anyway in order to obtain the following more uniform formalisation.
Regarding the change from red to amber, the two traffic lights behave differently. The following two formulae state that traffic light 1 will eventually change to amber after having been red, while traffic light 2 will do so after 0 to 4 time units.
It is worthwhile to note that the property \(\Box _{[0,\infty )} (detect \rightarrow \lozenge _{[1,x']} g_1)\) is not provable for any value of \(x'\). In a countermodel, \(g_1\) always holds at exactly the same states as detect, i.e. it is true in states where detect is true and false in states where detect is false. This satisfies the constraint (5) trivially. Also (6) is still satisfied due to the until constraints forcing the correct light sequence thereby falsifying \(\lozenge _{[1,x']} g_1\).
If traffic light 2 is currently red then it will be green within 1 to y time units.
Here the property \(\Box _{[0,\infty )}(r_2 \rightarrow \lozenge _{[0,y]} g_2)\) would hold for exactly the same values of y as property (8). This follows from the constraint that the traffic lights cannot be red and green at the same time.
If a traffic light is currently amber or red, then a car has to wait at most z time units until the traffic light will be green. We could try to formalise this property as
However, the first conjunct of (9) does not follow from our specification as there is no upper bound on the time that traffic light 1 can stay red if no car is detected.
In order to correctly formalise the property we have to include that the presence of a car makes detect true:
Our next example is a generalisation of the classical job-shop scheduling problem, called the Multiprocessor Job-shop Scheduling (MJS) problem [16, 27]. The representation provided is based on that in [17]. Here a set of jobs have to be processed on a set of machines running in parallel. Each job requires a number of processor steps to complete (this number may also depend on the machine, i.e., job i may run faster in machine j than in machine l). The question is whether there is a schedule such that after t time units all jobs will have been processed by the machines.
We use this example to illustrate encodings with both the strict and non-strict semantics. Under the strict semantics we use propositional variables \(run_{j_im_l}\) to encode that job \(j_i\) is running on machine \(m_l\), whereas in the non-strict semantics we use separate propositional variables \(m_l\) for machines and \(run_{j_i}\) for (the execution of) jobs. So, the strict semantics uses quadratically more propositional variables than the non-strict semantics. This is due to the fact that in the non-strict semantics we can encode parallelism by associating multiple states with the same time point. Our encodings have the property that there is a schedule if and only if there is a model for the resulting MTL formulae. One can use any model of the MTL formulae to create a schedule satisfying the constraints of an instance of the problem.
We first show how one can encode the problem in MTL with the strict semantics and then we show the encoding with the non-strict semantics.
Strict Semantics
Assume we have n jobs \( j_1, j_2, \ldots , j_n\) and k machines \(m_1\), \(m_2, \ldots , m_k\). Let
\(startRun_{j_i}\), \(run_{j_i}\) and \(hasRun_{j_i}\) denote the start, the execution and the end of the execution of job \(j_i\) on some machine, respectively;
\(startRun_{j_im_l}\) and \(run_{j_im_l}\) denote the start and the execution of job \(j_i\) on machine \(m_l\), respectively; and
\(t_{j_im_l}\) to denote the time taken to run job \(j_i\) on machine \(m_l\).
The following formulae state that (11) once a job starts running it must start running on one of the machines and that (12) once a job starts running on a machine it must run on that machine (where \(\bigwedge _{1 \le i \le n}\) and \(\bigwedge _{1 \le i \le n, 1\le l\le k}\) in front of the formulas is omitted for brevity)
The parametric formula (13) states that: if a job is running on one machine then it cannot be running on another (integrity of jobs); and another job cannot be running on the same machine (integrity of machines). By parametric formula (14), once a job has started it cannot be started again.
We write \(\lnot run_{j_i}\) as a short hand for \(\bigwedge _{l=1}^{k} \lnot run_{j_im_l}\). We can use (15) to denote that once job \(j_i\) is started to run on machine \(m_l\) it takes time \(t_{j_im_l}\) and (16) to denote that once job \(j_i\) has finished running on machine \(m_l\) it will not run again. Further, parametric formula (17) denotes that job \(j_i\) cannot be run until it has started.
We assume that initially no jobs have run, i.e., \(\bigwedge _{i=1}^{n} \lnot hasRun_{j_i}\); and that (18) if a job has not run and is currently not running then it will not have run in the next moment.
We can now check whether we can achieve a schedule after at most t time points by adding \(\lozenge _{[0,t]} \bigwedge _{i=1}^{n}hasRun_{j_i}\). We can also specify constraints on jobs such as
\(\Box _{[0,\infty )}(run_{j_i}\leftrightarrow run_{j_i,m_l})\): job \(j_i\) must run on machine \(m_l\);
\(\Box _{[0,\infty )}(startRun_{j_i} \rightarrow \lozenge _{[1,\infty )} startRun_{j_m})\): job \(j_i\) must start before job \(j_m\) (note that this formalisation relies on the fact that each job is started exactly once);
\(\lozenge _{[c,d]} startRun_{j_i}\): job \(j_i\) must start at a point within the interval [c, d].
Non-Strict Semantics
We again assume we have n jobs \( j_1, j_2, \ldots , j_n\) and k machines \(m_1, m_2, \ldots , m_k\). Let
\(startRun_{j_i}\) and \(hasRun_{j_i}\) denote the start and the end of job \(j_i\) on some machine, respectively;
\(run_{j_i}\) denote that job \(j_i\) is running on some machine; and
\(t_{j_im_l}\) denote the time taken to run job \(j_i\) on machine \(m_l\).
In each state exactly one of the variables of the form \(m_{l}\) is true. Also, in each state at most one job is running, but now we may have multiple states at the same time. Let \(\varPi _m=\{m_1,\ldots ,m_k\}\) and \(\varPi _j=\{run_{j_1},\ldots , run_{j_n}\}\). The following states the constraints mentioned above (the meaning of \(\oplus _{=1} \) and \(\oplus _{\le 1} \) is as described in Sect. 2):
Parametric formula (20) specifies that if a job is running on one machine then it cannot be running on another. Parametric formula (21) states that once a job is started it cannot be started again (where \(\bigwedge _{1 \le i \le n, 1\le l\le k}\) and \(\bigwedge _{1 \le i \le n}\) is again omitted).
to denote that once job \(j_i\) started to run on machine \(m_l\) it takes time \(t_{j_im_l}\) and (23) to denote that once job \(j_i\) has finished running on machine \(m_l\) it will not run again. Further, we use \(\Box _{[0,\infty )}(\lnot run_{j_i} \mathbin {{\mathcal {U}}} startRun_{j_i})\) to state a job \(j_i\) cannot be run until it is started and \(\Box _{[0,\infty )}(\lnot hasRun_{j_i}\mathbin {{\mathcal {U}}} startRun_{j_i})\) to state that a job cannot have run before it starts (another rule above will make sure that \(hasRun_{j_i}\) will hold after the run has finished).
We assume that initially no jobs have run, i.e., \(\bigwedge _{i=1}^{n} \lnot hasRun_{j_i}\). We can now check whether we can achieve a schedule after at most t time points by adding \(\lozenge _{[0,t]} \bigwedge _{i=1}^{n}hasRun_{j_i}\) and checking for satisfiability.
4 From MTL to LTL: Encoding ‘Gaps’
Next we provide satisfiability preserving translations from MTL formulae for discrete time models into LTL using a new propositional variable gap, which is intended to hold at LTL states corresponding to unmapped time points in MTL models. Assume that our MTL formulae are in NNF and FNF. The main idea for our translation is to map each timed state sequence \(\rho = (\sigma ,\tau )\) into a state sequence \(\sigma '\) such that \(\rho = (\sigma ,\tau )\) is a model of an MTL formula if, and only if, \(\sigma '\) is a model of our LTL translation. We first present our translation using the strict semantics and then show how to adapt it for the non-strict semantics, where multiple states are allowed to be mapped to the same time point. Our LTL translations are exponential in the size of the input formula in MTL due to the binary encoding of the numbers in the intervals. This blow up is unavoidable and optimal, since reasoning in MTL is ExpSpace-hard and an exponential size LTL translation gives an ExpSpace upper bound.
For every model of a MTL formula there is going to be a model of the translated formula, such that \(\lnot gap\) is true in those states \(\sigma '_j\) of \(\sigma '\) such that there is \(i \in \mathbb {N}\) with \(\tau (i)=j\) and gap is true in all other states of \(\sigma '\). We now define our mappings between MTL and LTL models.
Definition 1
Given a timed state sequence \(\rho = (\sigma ,\tau )\), we define a state sequence \(\sigma ' = \sigma '_0 \sigma '_1 \ldots \), where \(\sigma '_j\) is as follows:
$$\begin{aligned} \sigma '_j = \left\{ \begin{array}{l l} \sigma _i &{} \quad \text {if there is }i \in \mathbb {N}\text { such that }\tau (i) = j;\\ \{gap\} &{} \quad \text {otherwise.} \end{array} \right. \end{aligned}$$
Figure 2 illustrates the mapping given by Definition 1. For instance, if \(\rho = (\sigma ,\tau )\) is the timed state sequence on the left side of Fig. 2a then \((\rho ,0)\models \Circle _{[2,3]} p\). Table 1 presents the translation of formulae of the form \(\Circle _{I} \alpha \), \(\alpha _1 \mathbin {{\mathcal {U}}_{I}} \beta \) or \(\alpha \mathbin {\tilde{{\mathcal {U}}}_{I}} \beta \), where \(\alpha , \beta \) are propositional formulae. Assume \((\varphi )^\sharp =\varphi \) if \(\varphi \) is a propositional formula. Observe that, in the definition of \(\cdot ^\sharp \), recursion is only used to deal with the case where 0 occurs on the left side of an interval. As shown in Table 1, we translate \(\Circle _{[2,3]} p\) into:
$$\begin{aligned} \bigvee _{2\le l \le 3}(\Circle ^l(\lnot gap \wedge p)\wedge \bigwedge _{1\le k <l} \Circle ^k gap). \end{aligned}$$
Table 1
Strict gap translation from MTL to LTL, where \(\alpha ,\beta \) are propositional formulae and \(c_1,c_2 >0\)
Note that the state sequence represented on the right side of Fig. 2 is a model of the translation. Since gap is a propositional variable not occurring in \(\sigma \), the time points mapped by the image of \(\tau \) do not contain gap.
Definition 2
Given a state sequence \(\sigma '\) such that \((\sigma ',0)\models \lnot gap\wedge \Box ( \lozenge \lnot gap)\), we inductively define \(\rho = (\sigma _0,\tau (0)) (\sigma _1,\tau (1)) \ldots \), where \((\sigma _0,\tau (0)) = (\sigma '_0,0)\) and, for \(i,j,k \in \mathbb {N}\) and \(i>0\), \((\sigma _i,\tau (i))\) is as follows:
$$\begin{aligned} \begin{array}{ll@{\ }l} \quad \sigma _i=\sigma '_j \text { and } \tau (i) = j \quad &{} \quad \text {if} &{} j> \tau (i-1), gap \not \in \sigma '_j\text { and for all }k, \\ &{} &{} \tau (i-1)< k < j, gap\in \sigma '_k. \end{array} \end{aligned}$$
As \(\sigma '\) is such that \((\sigma ',0)\models \lnot gap\wedge \Box ( \lozenge \lnot gap)\), for each \(i \in \mathbb {N}\) we have \(\tau (i)\in \mathbb {N}\). Also, for \(i>0\), \(\tau (i)>\tau (i-1)\) and, so, \(\tau :\mathbb {N}\rightarrow \mathbb {N}\) is well defined.
The following two propositions are useful for the proof of Theorem 1. Since gap is a propositional variable not occurring in \(\sigma \), the time points mapped by the image of \(\tau \) do not contain gap. Then, it is easy to see the following.
Proposition 1
Given a timed state sequence \(\rho = (\sigma ,\tau )\), let \(\sigma '\) be as in Definition 1. Then, \((\sigma ',0)\models \Box ( \lozenge \lnot gap)\).
The state sequence \(\sigma '\) in Definition 2 is such that \((\sigma ',0)\models \lnot gap\wedge \Box ( \lozenge \lnot gap)\). Consequently, for the timed state sequence constructed in Definition 2 we have that for each \(i \in \mathbb {N}\), \(\tau (i)\in \mathbb {N}\). Also, for \(i>0\), \(\tau (i)>\tau (i-1)\) and, so, \(\tau :\mathbb {N}\rightarrow \mathbb {N}\) is well defined. The following proposition states this property.
Proposition 2
Given a state sequence \(\sigma '\) such that \((\sigma ',0)\models \lnot gap\wedge \Box ( \lozenge \lnot gap)\), let \(\rho = (\sigma ,\tau )\) be as in Definition 2. Then, \(\tau :\mathbb {N}\rightarrow \mathbb {N}\) is a function such that \(\tau (i+1)>\tau (i)\), for all \(i \in \mathbb {N}\).
We are ready for Theorem 1, which states the correctness of our translation from MTL to LTL using ‘gap’s. One can use similar arguments to show Theorem 2.
Theorem 1
Let \(\varphi = p_0 \wedge \bigwedge _i \Box _{[0,\infty )}(p_i \rightarrow \psi _i)\) be an MTL formula in NNF and FNF. Let \(\varphi ^{\sharp } = p_0 \wedge \bigwedge _i \Box (p_i \rightarrow (\lnot gap \wedge \psi _i^\sharp ))\) be the result of replacing each \(\psi _i\) in \(\varphi \) by \(\psi _i^\sharp \) as in Table 1. Then, \(\varphi \) is satisfiable if, and only if, \(\varphi ^{\sharp }\wedge \lnot gap \wedge \Box ( \lozenge \lnot gap)\) is satisfiable.
Proof
\(\varphi \) is satisfiable if, and only if, there is a timed state sequence \(\rho = (\sigma ,\tau )\) such that \((\rho ,0)\models \varphi \). Given a timed state sequence \(\rho = (\sigma ,\tau )\), let \(\sigma ' = \sigma '_0 \sigma '_1 \ldots \) be as in Definition 1.
By Definition 1 we have that \((\sigma ',\tau (0))\models \lnot gap\) and, by Proposition 1, \((\sigma ',\tau (0))\models \Box ( \lozenge \lnot gap)\). By definition of \(\sigma '\), for all propositional variables \(p_i\) occurring in \(\sigma \) and all \(j\in \mathbb {N}\), we have \((\rho ,j)\models p_i\) if, and only if, \((\sigma ',\tau (j))\models p_i\). With an inductive argument, one can show that, for any propositional formula \(\alpha \) not containing gap, \((\rho ,j)\models \alpha \) if, and only if, \((\sigma ',\tau (j))\models \alpha \).
Also, \(\varphi ^{\sharp }\wedge \lnot gap \wedge \Box ( \lozenge \lnot gap)\) is satisfiable if, and only if, there is a state sequence \(\sigma '\) such that \((\sigma ',0)\models \varphi ^\sharp \wedge \lnot gap \wedge \Box ( \lozenge \lnot gap)\). Given \(\sigma '\), let \(\rho = (\sigma ,\tau )\) be as in Definition 2. By Proposition 2, \(\tau :\mathbb {N}\rightarrow \mathbb {N}\) is well defined. By definition of \(\sigma \), for all propositional variables \(p_i\) occurring in \(\sigma '_n\) with \(gap \not \in \sigma '_n\) there is \(j\in \mathbb {N}\) such that \(\tau (j) =n\) and \((\rho ,j)\models p_i\) iff \((\sigma ',\tau (j))\models p_i\). An inductive argument lifts this claim to propositional formulae.
Thus, following Table 1, we only need to show correspondences between \( \psi _i\) and \(\lnot gap \wedge \psi _i^\sharp \). This follows from Claims 1–3 below (other cases are similar), where \(\rho = (\sigma ,\tau )\) is a timed state sequence and \(j\in \mathbb {N}\). Let \(C-1\) be the greatest number occurring in an interval in \(\varphi \) or 1, if none occur. We argue that, for all natural numbers \(c_1\) with \(0< c_1\le c_2 < C\), the following claims hold.
\((\rho ,j)\models \Circle _{[c_1,c_2]}\alpha \) iff \((\rho ,j+1) \models \alpha \) and \(\tau (j+1)\in \tau (j)+[c_1,c_2]\). By Definitions 1 and 2, this happens iff \((\sigma ',\tau (j+1))\models \lnot gap \wedge \alpha \) and there is no \(n \in \mathbb {N}\) such that \(\tau (n) = m\), for \(\tau (j)<m<\tau (j+1)\), meaning that for all such m, \((\sigma ',m)\models gap\). As \(\tau (j)+c_1\le \tau (j+1) \le \tau (j)+c_2\), this happens iff \((\sigma ',\tau (j))\models \bigvee _{c_1\le l \le c_2}( \Circle ^l (\lnot gap\wedge \alpha ) \wedge \bigwedge _{1 \le k < l}\Circle ^k gap)\), and \((\sigma ',\tau (j))\models \lnot gap\), by definition of \(\sigma '\). So, \((\rho ,j)\models \Circle _{[c_1,c_2]}\alpha \) iff \((\sigma ',\tau (j))\models \lnot gap \wedge (\Circle _{[c_1,c_2]}\alpha )^\sharp \).
\((\rho ,j)\models \alpha \mathbin {{\mathcal {U}}_{[c_1,c_2]}}\beta \) iff there is \(k \in \mathbb {N}\) such that \(\tau (k)\in \tau (j)+[c_1,c_2]\) and \((\rho ,k)\models \beta \) and for all \(l \in \mathbb {N}\) with \(j\le l< k\) we have \((\rho , l)\models \alpha \). By Definitions 1 and 2, this happens iff (i) \((\sigma ',\tau (k))\models \lnot gap \wedge \beta \), (ii) as \(\tau (j)+c_1\le \tau (k)\le \tau (j)+c_2\), \((\sigma ',\tau (j))\models \bigvee _{c_1\le m \le c_2} (\Circle ^m (\lnot gap \wedge \beta ))\), and (iii), for all \(l\in \mathbb {N}\) with \(j\le l< k\) we have \((\sigma ',\tau (l))\models \alpha \). If \(n\in \mathbb {N}\) is such that \(\tau (j)\le n< \tau (k)\) and there is no \(l\in \mathbb {N}\) with \(n=\tau (l)\) then, by definition of \(\sigma '\), \((\sigma ',n)\models gap\).
By the semantics of \(\tilde{{\mathcal {U}}}\), we have that \((\rho ,j)\models \alpha \mathbin {\tilde{{\mathcal {U}}}_{[c_1,c_2]}}\beta \) iff \((\rho ,j)\models \)\(\lnot (\lnot (\alpha )\mathbin {{\mathcal {U}}_{[c_1,c_2]}}\lnot (\beta ))\). By Claim 2, \((\rho ,j)\not \models \lnot (\alpha )\mathbin {{\mathcal {U}}_{[c_1,c_2]}}\lnot (\beta )\) iff \((\sigma ',\tau (j))\not \models \lnot gap \wedge (\lnot (\alpha )\mathbin {{\mathcal {U}}_{[c_1,c_2]}}\lnot (\beta ))^\sharp \). Since \((\sigma ',\tau (j))\models \lnot gap\) (by definition of \(\sigma '\)), this happens iff \((\sigma ',\tau (j))\models \lnot gap\wedge \lnot (\lnot (\alpha )\mathbin {{\mathcal {U}}_{[c_1,c_2]}}\lnot (\beta ))^\sharp \). \(\square \)
Example Assume that we are given the following MTL formula in NNF and FNF: \(\varphi = p_0 \wedge \Box _{[0,\infty )}(p_0 \rightarrow \Circle _{[2,3]} p_1) \wedge \)\( \Box _{[0,\infty )}(p_1 \rightarrow \lozenge _{[1,2]}\lnot q).\) Using Table 1, we translate \(\varphi \) into LTL as follows (recall that \(\lozenge _{I} \psi \equiv \mathbf {true}\mathbin {{\mathcal {U}}_{I}} \psi \)):
$$\begin{aligned} \varphi ^{\sharp } = p_0 \begin{array}[t]{@{}l@{}} \hbox {}\wedge \Box (p_0 \rightarrow (\lnot gap \wedge (\bigvee \nolimits _{2\le l \le 3}(\Circle ^l(\lnot gap \wedge p_1) \wedge \bigwedge _{1\le k <l} \Circle ^k gap))\\ \hbox {}\wedge \Box (p_1 \rightarrow (\lnot gap \wedge (\bigvee \nolimits _{1\le l \le 2} ( \Circle ^l (\lnot gap \wedge \lnot q)))). \end{array} \end{aligned}$$
Non-Strict Semantics
We now show how we modify the Gap translation for non-strict timed state sequences. We introduce a fresh propositional variable called ‘same’. same is true exactly in those states \(\sigma '_j\) of \(\sigma '\) such that there is \(i \in \mathbb {N}\) with \(\tau (i)=j\) and, for \(i>0\), \(\tau (i)=\tau (i-1)\). Note that same and gap cannot both be true in any state. We say that a state s is a gap state if \(gap \in s\). We now define our mappings between MTL and LTL models.
Definition 3
Let \(\rho = (\sigma ,\tau )\) be a non-strict timed state sequence.
We define \(\sigma ' = \sigma '_0 \sigma '_1 \ldots \) by initially setting \(\sigma '=\sigma \) and then modifying \(\sigma '\) with the two following steps:
1.
For \(i>0\), if \(\tau (i)-\tau (i-1)=0\) then set \(\sigma '_i:=\sigma _i\cup \{same\}\);
2.
For \(i,j\ge 0\), if \(\sigma '_j\) is the i-th non-gap state in \(\sigma '\), \(\sigma '_{j+1}\) is a non-gap state and \(\tau (i+1)-\tau (i)=k>1\) then add \(k-1\) states of the form \(\{gap \}\) between \(\sigma '_j\) and \(\sigma '_{j+1}\).
Figure 3 illustrates the mapping given by Definition 3. For instance, if \(\rho = (\sigma ,\tau )\) is the non-strict timed state sequence on the left side then \((\rho ,0)\models \lozenge _{[2,2]} q\). Table 2 presents our translation of formulae of the form \(\Circle _{I} \alpha \), \(\alpha _1 \mathbin {{\mathcal {U}}_{I}} \beta \) or \(\alpha \mathbin {\tilde{{\mathcal {U}}}_{I}} \beta \), as in Table 1. As shown in Table 2, we translate \(\lozenge _{[2,2]} q\) into:
$$\begin{aligned} same \mathbin {{\mathcal {U}}} (\lnot same \wedge \Circle ( same \mathbin {{\mathcal {U}}} (\lnot same \wedge \Circle ((q \wedge \lnot gap)\vee \Circle ( same \mathbin {{\mathcal {U}}} (q \wedge same)))))). \end{aligned}$$
The main distinction from the translation presented in Table 1 is that here we use nested until operators to make progress in our encoding of the time line whenever we find a state with \(\lnot same \). Note that the state sequence represented on the right side of Fig. 3 is a model of the translation (recall that \(\lozenge _{[2,2]}q\equiv ({\mathbf {true}} \mathbin {{\mathcal {U}}_{[2,2]}}q)\)).
Definition 4
Let \(\sigma '\) be a state sequence such that \((\sigma ',0)\models \lnot gap\wedge \lnot same \wedge \Box ( \lozenge \lnot gap)\wedge \Box (\lnot same \vee \lnot gap) \wedge \Box (gap \rightarrow \Circle \lnot same)\).
We first define \(\tau :\mathbb {N}\rightarrow \mathbb {N}\) by setting \(\tau (0)=0\) and, for \(i>0\), \(\tau (i)\) is as follows:
$$\begin{aligned} \tau (i) = \left\{ \begin{array}{ll} \tau ({i}{-}{1}) &{} \text {if }\sigma '_j\text { is the } {i}{+}{1}\text {-th non-gap state and } same\,\in \, \sigma '_j\\ \tau ({i}{-}{1}){+}{k}{+}{1} &{} {\text {otherwise,}} \end{array} \right. \end{aligned}$$
where \(k\ge 0\) is the number of gap states between the i-th and \(i+1\)-th non-gap states. We now define \(\sigma \) as follows:
$$\begin{aligned} \sigma _i=\sigma '_j\setminus \{same \}, \hbox { where }\sigma '_j\hbox { is the }i+1\hbox {-th non-gap state.} \end{aligned}$$
We are ready for Theorem 2, which states the correctness of our translation from MTL to LTL using the variables ‘gap’ and ‘same’.
Theorem 2
Let \(\varphi = p_0 \wedge \bigwedge _i \Box _{[0,\infty )}(p_i \rightarrow \psi _i)\) be an MTL formula in NNF and FNF. Let \(\varphi ^{\sharp } = p_0 \wedge \bigwedge _i \Box (p_i \rightarrow (\lnot gap \wedge \psi _i^\sharp ))\) be the result of replacing each \(\psi _i\) in \(\varphi \) by \(\psi _i^\sharp \) as in Table 2. Then, \(\varphi \) is satisfiable if, and only if, \(\varphi ^{\sharp }\wedge \lnot gap\wedge \lnot same \wedge \Box ( \lozenge \lnot gap)\wedge \Box (\lnot same \vee \lnot gap) \wedge \Box (gap \rightarrow \Circle \lnot same)\) is satisfiable.
Proof
(Sketch) We use Definitions 3 and 4 to map models of \(\varphi \) into models of \(\varphi ^{\sharp }\wedge \lnot gap \wedge \Box ( \lozenge \lnot gap)\) and vice versa. The correctness of our translation is again given by a structural inductive argument. As mentioned, the main difference w.r.t. to Theorem 1 is that here we use the propositional variable \(same \) to encode multiple states mapped to the same time point. \(\square \)
Table 2
Non-strict gap translation from MTL to LTL, using gap and \(same \), where \(\alpha ,\beta \) are propositional logic formulae, \(c_1,c_2 >0\) and \((\Circle _{[c_1,\infty )}\alpha )^\sharp \) and \((\Circle _{[c_1,c_2]}\alpha )^\sharp \) are as in Table 1
Next we provide satisfiability preserving translations from MTL formulae for discrete time models into LTL using new propositional variables to denote the time differences from the previous state. Assume that our MTL formulae are in NNF and FNF. Similar to the previous section our proof strategy relies on mapping each timed state sequence \(\rho = (\sigma ,\tau )\) to a state sequence \(\sigma '\) such that \(\rho = (\sigma ,\tau )\) is a model of an MTL formula if, and only if, \(\sigma '\) is a model of our LTL translation. We first show a translation under the strict semantics and then we show how to adapt it for the non-strict semantics. Our LTL translations here are also exponential in the size of the input formula in MTL due to the binary encoding of the numbers in the intervals, and thus, yield tight ExpSpace upper bounds.
Strict Semantics
We denote by \(C-1\) the greatest number occurring in an interval in an MTL formula \(\varphi \) or 1, if none occur. We say that a timed state sequence \(\rho = (\sigma ,\tau )\) is C-bounded, for a constant \(C\in \mathbb {N}\), if \(\tau (0)\le C\) and, for all \(i \in \mathbb {N}\), \(\tau (i+1) -\tau (i)\le C\). To map a timed state sequence \(\rho = (\sigma ,\tau )\) to a state sequence \(\sigma '\) we employ the following result adapted from [7].
Theorem 3
Let \(\varphi \) be an MTL formula. If there is a timed state sequence \(\rho = (\sigma ,\tau )\) such that \((\rho ,0)\models \varphi \) then there is a C-bounded timed state sequence \(\rho _C\) such that \((\rho _C,0)\models \varphi \).
Definition 5
Given a timed sequence \(\rho = (\sigma ,\tau )\) and \(C\in \mathbb {N}\), we define a timed sequence \(\rho _C= (\sigma _C,\tau _C)\) as follows:
\(\sigma _C = \sigma \);
\(\tau _C(0)=\text {min}(\tau (0),C)\) and, for \(i>0\), we have that \(\tau _C(i) = \tau _C(i-1)+\text {min} (C,\tau (i)-\tau (i-1))\).
The following proposition states the main property of Definition 5.
Proposition 3
Let \(\rho = (\sigma ,\tau )\) be a timed state sequence and let \(\rho _C = (\sigma _C,\tau _C)\) be as in Definition 5. For all \(i,j \in \mathbb {N}\) and all intervals of the form \(I=[c_1,c_2]\) or \(I=[c_1,\infty )\) with \(c_1,c_2 < C\), the following holds:
Let \(\rho = (\sigma ,\tau )\) be a timed state sequence and let \(\rho _C = (\sigma _C,\tau _C)\) be as in Definition 5. By definition of \(\rho _C\) we have that \(\rho _C\) is C-bounded.
Assume w.l.o.g. that \(\varphi \) is in NNF. Let \(\mathsf{sub}(\varphi )\) be the set of all subformulae of \(\varphi \). To prove this lemma, we argue by structural induction and show that for all \(\varphi ' \in \mathsf{sub}(\varphi )\), if \((\rho ,i)\models \varphi '\) then \((\rho _C,i)\models \varphi '\), \(i \in \mathbb {N}\).
In the base case, \(\varphi '\) is a propositional formula. Then, as \(\sigma _C = \sigma \), we have that \((\rho ,i)\models \varphi '\) implies \((\rho _C,i)\models \varphi '\), \(i \in \mathbb {N}\). Suppose that, for \(\chi ,\psi \in \mathsf{sub}(\varphi )\) and \(i \in \mathbb {N}\), \((\rho ,i)\models \chi \) implies \((\rho _C,i)\models \chi \), and, \((\rho ,i)\models \psi \) implies \((\rho _C,i)\models \psi \). We explain for \(\Circle _{I}\), \(\mathbin {{\mathcal {U}}_{I}}\) and \(\mathbin {\tilde{{\mathcal {U}}}_{I}}\) (other cases are similar):
\(\varphi '\) is of the form \(\Circle _{I}\chi \): if \((\rho ,i)\models \Circle _{I}\chi \) then \(\tau (i+1) \in \tau (i) + I\) and \((\rho ,i+1)\models \psi \). By the induction hypothesis, \( (\rho _C,i+1)\models \psi \). By Proposition 3, \(\tau _C(i+1)\in \tau _C(i)+I\). Then, \((\rho _C,i)\models \Circle _{I}\chi \).
\(\varphi '\) is of the form \((\chi \mathbin {{\mathcal {U}}_{I}} \psi )\): if \((\rho ,i)\models (\chi \mathbin {{\mathcal {U}}_{I}} \psi )\) then there is \(k \in \mathbb {N}\) such that \(k \ge i\), \(\tau (k) \in \tau (i) + I\) and \((\rho ,k)\models \psi \) and for all \(j \in \mathbb {N}\), if \(i\le j< k\) then \((\rho ,j)\models \chi \). By the induction hypothesis, \( (\rho _C,k)\models \psi \text { and } (\rho _C,j)\models \chi \text {, for all }j \in \mathbb {N} \text { with } i\le j< k\). By Proposition 3, \(\tau _C(k)\in \tau _C(i)+I\). Then, \((\rho _C,i)\models (\chi \mathbin {{\mathcal {U}}_{I}} \psi )\).
\(\varphi '\) is of the form \((\chi \mathbin {\tilde{{\mathcal {U}}}_{I}} \psi )\): if \((\rho ,i)\models (\chi \mathbin {\tilde{{\mathcal {U}}}_{I}} \psi )\) then either:
1.
for all \(j \in \mathbb {N}\), if \(\tau (j)\in \tau (i)+I\) then \((\rho ,j)\models \psi \); or
2.
(if \(c_1>0\)) \((\rho ,k)\models \chi \) for some \(k \in \mathbb {N}\) such that \(\tau (k)\in \tau (i)+[0,c_1-1]\), where \(c_1\) is the left end-point of I; or
3.
\((\rho ,l)\models \chi \) for some \(l\in \mathbb {N}\) such that \(\tau (l)\in \tau (i)+I\) and for all \(l' \in \mathbb {N}\) such that \(\tau (i)+c_1\le \tau (l')\le \tau (l)\), we have \((\rho ,l')\models \psi \).
We make a case distinction. In Case (1), we have to establish that, for all \(j\in \mathbb {N}\), if \(\tau _C(j)\in \tau _C(i)+I\) then \((\rho _C,j)\models \psi \). By Proposition 3, if \(\tau _C(j)\in \tau _C(i)+I\) then \(\tau (j)\in \tau (i)+I\) and by induction hypothesis, \((\rho _C,j)\models \psi \), for all \(j\in \mathbb {N}\) with \(\tau (j)\in \tau (i)+I\). Therefore, \((\rho _C,i)\models (\chi \mathbin {\tilde{{\mathcal {U}}}_{I}} \psi )\). Cases (2) and (3) can be proved with similar arguments.\(\square \)
By Theorem 3, w.l.o.g., we can consider only timed state sequences where the time difference from a state to its previous state is bounded by C. Then, we can encode time differences using propositional variables of the form \(s^n_m\) with the meaning that ‘the sum of the time differences from the last n states to the current state is m’. For our translation, we only need to define these variables up to sums bounded by \(2\cdot C\). We can now define our mapping from an MTL model to an LTL model.1
Definition 6
Given a C-bounded timed state sequence \(\rho = (\sigma ,\tau )\), we define \(\sigma ' = \sigma '_0 \sigma '_1 \ldots \) by setting \(\sigma '_0 = \sigma _0\) and, for \(i > 0\):
where \(1 \le j< C,\ 1\le l \le 2\cdot C\) and \(1\le k\le C\) (assume variables of the form \(s^n_m\) do not occur in \(\sigma \)).
In Definition 6, if, for example, \(\tau (2)-\tau (0) = 4\) then \((\sigma ',2)\models s^{2}_{4}\). Intuitively, the variable \(s^2_4\) allow us to group together all the cases where the sum of the time differences from the last 2 states to the current state is 4. This happens when: \(\tau (2)-\tau (1) = 3\) and \(\tau (1)-\tau (0) = 1\); or \(\tau (2)-\tau (1) = 1\) and \(\tau (1)-\tau (0) = 3\); or \(\tau (2)-\tau (1) = 2\) and \(\tau (1)-\tau (0) = 2\). By definition of \(\sigma '\), Lemma 1 is immediate (see definition of \(\oplus _{\le 1}\) and \(\oplus _{\ge 1}\) in the Preliminaries).
Lemma 1
Let \(S_C\) be the conjunction of the following:
1.
\(\Circle \Box \oplus _{= 1} \varPi ^1\), for \(\varPi ^1 = \{s^1_k\mid 1 \le k \le C \}\);
2.
\(\Box \oplus _{\le 1} \varPi ^i\), for \(1< i < C\) and \(\varPi ^i = \{s^i_j \mid i \le j \le 2\cdot C\}\);
3.
\(\Box ((\Circle s^1_k\wedge s^j_l) \rightarrow \Circle s^{j+1}_{\mathsf{min}(l+k,2\cdot C)})\), for \(\{s^1_k,s^j_l,s^{j+1}_{\mathsf{min}(l+k,2\cdot C)}\} \subseteq \bigcup _{1 \le i < C } \varPi ^i\).
Given a C-bounded timed state sequence \(\rho = (\sigma ,\tau )\), let \(\sigma ' = \sigma '_0 \sigma '_1 \ldots \) be as in Definition 6. Then, \((\sigma ',0)\models S_C\).
There is exactly one value k, \(1\le k \le C\), that is going to be equal to the sum of the time difference of the last state to the current. This is encoded by \(s^1_k\) (Point 1). Point 2 ensures that at all times we cannot have more than one value for the sum of the time differences of the last i states. Finally, Point 3 has the propagation of sum variables: if the sum of the last j states is l and the time difference to the next is k then the next state should have that the sum of the last \(j+1\) states is \(l+k\).
Remark 1
To simplify the presentation, in this section we used variables of the form \(s^n_m\), where n ranges from 1 to \(C-1\) and m ranges from 1 (or from 0 for the non-strict semantics) to \(2\cdot C\) (in fact \(2\cdot C -1\) would be enough for the translation). As mentioned in Sect. 1, the exponential blow-up of the translations cannot be avoided. Though, we can have a slightly more succinct translation by encoding m in binary. So in our experiments, we encode variables of the form \(s^n_m\) with \(n\cdot \mathsf {log}\ m\) variables, where for each n we represent m in binary. For example, \(s^2_4\) is encoded with \(s^2_2\wedge \lnot s^2_1 \wedge \lnot s^2_0\).
We now define our mapping from an LTL model of \(S_C\) to an MTL model (for this mapping, we actually only need Point 1).
Table 3
Strict time difference translation from MTL to LTL where \(\alpha ,\beta \) are propositional logic formulae and \(c_1,c_2 > 0\)
MTL
Strict time difference translation
\( (\Circle _{[c_1,\infty )}\alpha )^\sharp \)
\(\begin{array}{l}\Circle (( \bigvee _{c_1\le i \le C} s^1_i)\wedge \alpha )\end{array}\)
\( (\Circle _{[0,\infty )}\alpha )^\sharp \)
\(\Circle \alpha \)
\( (\Circle _{[c_1,c_2]}\alpha )^\sharp \)
\(\begin{array}{l}\Circle (( \bigvee _{c_1\le i \le c_2} s^1_i)\wedge \alpha )\end{array}\)
Given a state sequence \(\sigma ' = \sigma '_0 \sigma '_1 \ldots \) such that \((\sigma ',0)\models S_C\), we define a C-bounded timed state sequence \(\rho = (\sigma ,\tau )\) by setting \(\sigma _i = \sigma '_i\setminus ( \bigcup _{1\le j < C}\varPi ^j)\), for \(i \in \mathbb {N}\), and:
Note that \(\rho \), in particular, \(\tau \), in Definition 7 is well-defined because for every \(i \in \mathbb {N}\) there is exactly one k such that \((\sigma ',i)\models s^1_k \). Table 3 presents our translation of formulae of the form \(\Circle _{I} \alpha \), \(\alpha _1 \mathbin {{\mathcal {U}}_{I}} \beta \) or \(\alpha \mathbin {\tilde{{\mathcal {U}}}_{I}} \beta \), as in Tables 1 and 2. As shown in Table 3, we translate, for example, \(\Circle _{[2,3]}p\) into \(\Circle ((s^1_2\vee s^1_3)\wedge p)\). The following two propositions are useful for the proof of Theorem 4.
Proposition 4
Given a C-bounded timed state sequence \(\rho = (\sigma ,\tau )\), let \(\sigma '\) be as in Definition 6. For all \(i<j\in \mathbb {N}\), if \(\tau (j) - \tau (i) = m \le 2\cdot C\) and \(j-i=n<C\) then \((\sigma ',j)\models s^n_m\).
Proof
In the base case \(j = i+1\), that is, \(n = 1\). As \(\rho \) is C-bounded, \(\tau (i+1)-\tau (i) = k\), for \(1 \le k \le C\). Then, by Definition 6, \((\sigma ',j)\models s^1_k\). Suppose that, for \(j = i+n\), if \(\tau (i+n)-\tau (i) = l\) then \((\sigma ',i+n)\models s^n_l\) where \(l \le 2\cdot C\). In the induction step we consider \(j = i +n +1\). Let \(k'\) be such that \(\tau (i +n +1)-\tau (i +n) = k'\). As \(\tau (i+n)-\tau (i) = l\) and \(\tau (i +n +1)-\tau (i +n) = k'\), we have that \(\tau (i +n +1)-\tau (i) = l+k'\). By Definition 6, \((\sigma ',i +n +1)\models s^1_{k'}\). By induction hypothesis, \((\sigma ',j)\models s^n_l\). By Definition 6, if \(l+k'\le 2\cdot C\), then \((\sigma ',i +n +1)\models s^{n+1}_{l+k'}\). \(\square \)
Proposition 5
Given a state sequence \(\sigma ' = \sigma '_0 \sigma '_1 \ldots \) such that \((\sigma ',0)\models S_C\), let \(\rho \) be as in Definition 7. For all \(i<j\in \mathbb {N}\), if \((\sigma ',j)\models s^n_m\) with \(j-i= n < C\) and \(m\le 2\cdot C\) then \(\tau (j) - \tau (i) = m\).
Proof
In the base case \(j = i+1\), that is, \(n = 1\). Assume that \((\sigma ',i+1)\models s^1_k\). Then, by Definition 7, \(\tau (i+1)-\tau (i) = k\le C\), \(i \in \mathbb {N}\). Suppose that, for \(j = i+n\), \((\sigma ',i+n)\models s^n_m\), with \(j-i=n < C\) and \(m\le 2\cdot C\), implies \(\tau (i+n) - \tau (i) = m\). In the induction step we consider \(j = i +n+1\). Assume that \((\sigma ',i+n+1)\models s^{n+1}_{l}\). By Points 1 and 2 of the definition of \(S_C\), there is \(1 \le k'\le C\) such that \((\sigma ',i+n+1)\models s^{1}_{k'}\). As \((\sigma ',i+n)\models s^n_m\) and \((\sigma ',i+n+1)\models s^{1}_{k'}\), we have that, by Point 4 of the definition of \(S_C\), \((\sigma ',i+n+1)\models s^{n+1}_{\mathsf{min}(m+k',2\cdot C)}\). Also, by Point 3 of the definition, there is no \(l\ne m+k'\) such that \((\sigma ',i+n+1)\models s^{n+1}_{l}\). Then, we can assume that \(l = \mathsf{min}(m+k',2\cdot C)\). By induction hypothesis, for \(m\le 2\cdot C\), we have that \(\tau (i+n) - \tau (i) = m\). By Definition 7, \(\tau (i+n+1) - \tau (i+n) = k'\). Then, if \(m+k'\le 2\cdot C\) we have that \(\tau (i+n+1) - \tau (i) = m+k'\). \(\square \)
We now show Theorem 4, which states the correctness of our translation using time differences. One can use similar arguments to show Theorem 5.
Theorem 4
Let \(\varphi = p_0 \wedge \bigwedge _i \Box _{[0,\infty )}(p_i \rightarrow \psi _i)\) be an MTL formula in NNF and FNF. Let \(\varphi ^{\sharp } = p_0 \wedge \bigwedge _i \Box (p_i \rightarrow \psi _i^\sharp )\) be the result of replacing each \(\psi _i\) in \(\varphi \) by \(\psi _i^\sharp \) as in Table 3. Then, \(\varphi \) is satisfiable if, and only if, \(\varphi ^{\sharp }\wedge S_C\) is satisfiable.
Proof
\(\varphi \) is satisfiable if, and only if, there is a timed state sequence \(\rho = (\sigma ,\tau )\) such that \((\rho ,0)\models \varphi \). By Theorem 3, we can assume w.l.g. that \(\rho \) is C-bounded, where \(C-1\) is the largest constant in \(\varphi \). Given a timed state sequence \(\rho = (\sigma ,\tau )\), let \(\sigma ' = \sigma '_0 \sigma '_1 \ldots \) be as in Definition 6. By Lemma 1, \((\sigma ',0)\models S_C\). By definition of \(\sigma '\), for all propositional variables \(p_i\) occurring in \(\sigma \) and all \(j\in \mathbb {N}\), we have \((\rho ,j)\models p_i\) iff \((\sigma ',j)\models p_i\). With an inductive argument one can show that, for any propositional formula \(\alpha \), \((\rho ,j)\models \alpha \) iff \((\sigma ',j)\models \alpha \).
Also, \(\varphi ^\sharp \wedge S_C\) is satisfiable if, and only if, there is a state sequence \(\sigma '\) such that \((\sigma ',0)\models \varphi ^\sharp \wedge S_C\). Given \(\sigma '\), let \(\rho = (\sigma ,\tau )\) be a C-bounded timed state sequence as in Definition 7. By definition of \(\sigma \), for all propositional variables \(p_i\) occurring in \(\sigma '\) but not in \( \bigcup _{1\le i' < C}\varPi ^{i'}\) and all \(j\in \mathbb {N}\), we have \((\rho ,j)\models p_i\) iff \((\sigma ',j)\models p_i\). Clearly, for any propositional formula \(\alpha \), \((\rho ,j)\models \alpha \) iff \((\sigma ',j)\models \alpha \).
Thus, following Table 3, we only need to show correspondences between \(\psi _i\) and \(\psi _i^\sharp \). This follows from Claims 4–6 below (other cases are similar), where \(\rho = (\sigma ,\tau )\) is a C-bounded timed state sequence. We argue that, for all natural numbers \(c_1\) with \(0< c_1\le c_2 < C\), the following claims hold.
\((\rho ,j)\models \Circle _{[c_1,c_2]}\alpha \), with \(c_1>0\), iff \((\rho ,j+1)\models \alpha \) and \(\tau (j+1)\in \tau (j)+[c_1,c_2]\). By Definitions 6 and 7, this happens iff \((\sigma ',j+1)\models \alpha \) and \((\sigma ',j+1)\models \bigvee _{c_1\le i \le c_2}s^1_i \), which is equivalent to \((\sigma ',j)\models \Circle (( \bigvee _{c_1\le i \le c_2}s^1_i)\wedge \alpha )\).
\((\rho ,j)\models \alpha \mathbin {{\mathcal {U}}_{[c_1,c_2]}}\beta \), with \(c_1>0\), iff there is \(i \in \mathbb {N}\) such that \(\tau (j+i) -\tau (j)\in [c_1,c_2]\), \((\rho ,j+i)\models \beta \) and for all \(n \in \mathbb {N}\), if \(j \le n < j+i\) then \((\rho ,n)\models \alpha \). By Definitions 6 and 7, this happens iff \((\sigma ',j+i)\models \beta \) and for all \(n \in \mathbb {N}\), if \(j \le n < j+i\) then \((\sigma ',n)\models \alpha \). By Propositions 4 and 5, for all \(i\in \mathbb {N}\), with \(0< j-i=n<C\), and \(m\le 2\cdot C\), we have that \((\sigma ',j)\models s^{n}_{m}\) iff \(\tau (j+i)-\tau (j)=m\). As \(c_1 >0\) and \(\tau \) is strictly monotonically increasing, we have \(1\le n\le c_2\). Also, \(c_1\le \tau (j+i)-\tau (j)=m\le c_2<C\),2 so this happens iff \(i \in \mathbb {N}\) is such that \((\sigma ',j+i)\models \Circle ^n(\bigvee _{c_1\le m \le c_2} s^{n}_m)\wedge \beta \), with \(n=j-i\), and \((\sigma ',\ell )\models \alpha \) for all \(\ell \in \mathbb {N}\) such that \(j \le \ell < j+i\). This is equivalent to \((\sigma ',j)\models \bigvee _{1\le n \le c_2} (\Circle ^n((\bigvee _{c_1\le m \le c_2} s^{n}_m) \wedge \beta )\wedge \bigwedge _{0\le k < n}\Circle ^k \alpha )\).
which is equivalent to \((\sigma ',j)\models \lnot (\lnot (\alpha )\mathbin {{\mathcal {U}}_{[c_1,c_2]}}\lnot (\beta ))^\sharp \). \(\square \)
Example Assume that we are given the following MTL formula in NNF and FNF: \(\varphi = p_0 \wedge \Box _{[0,\infty )}(p_0 \rightarrow \Circle _{[2,3]} p_1) \wedge \Box _{[0,\infty )}(p_1 \rightarrow \lozenge _{[1,2]}\lnot q)\). Using Table 3, we translate \(\varphi \) into LTL as follows:
(recall that \(\lozenge _{I} \psi \equiv {\mathbf {true}} \mathbin {{\mathcal {U}}_{I}} \psi \)). By Theorem 4, \(\varphi \) is satisfiable iff \(\varphi ^{\sharp }\wedge S_4\) is satisfiable, where \(S_4\) is the conjunction of the following:
1.
\(\Circle \Box \oplus _{= 1} \varPi ^1\), for \(\varPi ^1 = \{s^1_k\mid 1 \le k \le 4 \}\);
2.
\(\Box \oplus _{\le 1} \varPi ^i\), for \(1< i < 8\) and \(\varPi ^i = \{s^i_j \mid i \le j \le 8\}\);
3.
\(\Box (\Circle s^1_k\wedge s^j_l \rightarrow \Circle s^{j+1}_{\mathsf{min}(l+k,8)})\), for \(\{s^1_k,s^j_l,s^{j+1}_{\mathsf{min}(l+k,8)}\} \subseteq \bigcup _{1 \le i < 8 } \varPi ^i\).
Table 4
Non-strict time difference translation from MTL to LTL where \(\alpha ,\beta \) are propositional logic formulae, \(k_1,k_2 \ge 0\) and \(c_1,c_2 > 0\)
MTL
Non-strict time difference translation
\( (\Circle _{[k_1,\infty )}\alpha )^\sharp \)
\( (\Circle _{[k_1,k_2]}\alpha )^\sharp \)
\(\begin{array}{l}\Circle (( \bigvee _{k_1\le i \le k_2} s^1_i)\wedge \alpha )\end{array}\)
We now show how we modify the Time Difference translation for non-strict timed state sequences. We extend the set \(\varPi ^1 = \{s^1_i\mid 1 \le i \le C \}\) of propositional variables representing time differences with \(s^1_0\), which holds whenever the time difference to the previous state is 0. We say that a state is non-zero if the time difference to the previous state is non-zero. For \(m>0\), the meaning of the variables of the form \(s^n_m\) also needs to change. It now indicates that ‘the sum of the time differences from the last nnon-zero states to the current state is m’. As before, for our translation, we only need to define these variables up to sums bounded by \(2\cdot C\). We can now define our mapping from an MTL model to an LTL model.
Given a C-bounded non-strict timed state sequence \((\sigma ,\tau )\), we define a state sequence \(\sigma '\) as in Definition 6, with the difference that, whenever \(\tau (i)=\tau (i-1)\), we now make \(s^1_0\) true in \(\sigma '_i\) and, for \(m>0\), we copy all variables of the form \(s^n_m\) in \(\sigma '_{i-1}\) to \(\sigma '_i\). Let \(S'_C\) be the conjunction of the following:
1.
\(\Circle \Box \oplus _{= 1}\varPi ^1 \), for \(\varPi ^1 = \{s^1_k\mid 0 \le k \le C \}\);
2.
\(\Box \oplus _{\le 1} \varPi ^i\), for \(1< i < C\) and \(\varPi ^i = \{s^i_j \mid i \le j \le 2\cdot C\}\);
3.
\(\Box ((\Circle s^1_k\wedge s^j_l) \rightarrow \Circle s^{j+1}_{\mathsf{min}(l+k,2\cdot C)})\), for \(\{s^1_k,s^j_l,s^{j+1}_{\mathsf{min}(l+k,2\cdot C)}\} \subseteq \bigcup _{1 \le i < C } \varPi ^i\);
4.
\(\Box ((\Circle s^1_0\wedge s^j_l) \rightarrow \Circle s^{j}_{l})\), for \(s^j_l \in \bigcup _{1 \le i < C } \varPi ^i\) with \(l> 0\).
It is easy to see that \((\sigma ',0)\models S'_C\). Note that the only difference from \(S'_C\) to \(S_C\), defined in Lemma 1, is Point 4 which propagates the variables of the form \(s^n_m\) to the next state if the time difference is zero. The mapping from an LTL model of \(S'_C\) to an MTL model is defined in the same way as in Definition 7 (but now the time difference k can be zero). To simplify the notation, in Table 4 we write \(\phi \mathbin {{\mathcal {U}}^{n}} \gamma , \chi \) as a shorthand for \(\phi \mathbin {{\mathcal {U}}} ( \gamma \wedge \Circle (\phi \mathbin {{\mathcal {U}}^{n-1}} \gamma , \chi ))\), where \(\phi \mathbin {{\mathcal {U}}^{1}} \gamma , \chi = (\phi \mathbin {{\mathcal {U}}} \chi )\). Theorem 5 states the correctness of our translation (Table 4) using non-strict time differences. It can be proved with ideas similar to those used in the proof of Theorem 4. The main distinction appears in the translation of the ‘until’ formulas, where we nest until operators so that we can count n non-zero states and then check whether a variable of the form \(s^n_m\) holds (in the strict case all states are non-zero, so in Table 3 we can count these states with next operators).
Theorem 5
Let \(\varphi = p_0 \wedge \bigwedge _i \Box _{[0,\infty )}(p_i \rightarrow \psi _i)\) be an MTL formula in NNF and FNF. Let \(\varphi ^{\sharp } = p_0 \wedge \bigwedge _i \Box (p_i \rightarrow \psi _i^\sharp )\) be the result of replacing each \(\psi _i\) in \(\varphi \) by \(\psi _i^\sharp \) as in Table 4. Then, \(\varphi \) is satisfiable if, and only if, \(\varphi ^{\sharp }\wedge S'_C\) is satisfiable.
Proof
(Sketch) We use our modified versions of Definitions 6 and 7 for the non-strict semantics to map models of \(\varphi \) into models of \(\varphi ^{\sharp }\wedge S'_C\) and vice versa. The correctness of our translation is again given by a structural inductive argument. As mentioned, the main difference w.r.t. to Theorem 4 is that here we use the propositional variable \(s^1_0\) to encode multiple states mapped to the same time point. \(\square \)
6 Empirical Evaluation of the Translations
In order to empirically evaluate the translations, we have implemented them in SWI-Prolog and have used them together with the LTL satisfiability solvers Aalta, Leviathan, LS4, LWB-MOD, LWB-SAT, NuSMV-BDD , NuSMV-SBMC , pltl (graph) , pltl (tree) , TRP\(^{{\mathtt {++}}}\) , and TSPASS. The sources of the implementation of the translations and all auxiliary files necessary to replicate the evaluation can be found at [31].
Aalta [1] implements the obligation-based LTL satisfiability checking algorithm for finite and infinite traces devised by Li et al. [37]. We have performed experiments with both versions 1.2 and 2.0 of Aalta. As Aalta 2.0 was consistently several orders of magnitude faster than Aalta 1.2, we will only report the results for the latest version of Aalta.
NuSMV 2.6.0 [45] uses a reduction of the LTL satisfiability problem to the LTL model checking problem [15]. It is then possible to decide the latter problem either using a BDD-based algorithm (NuSMV-BDD) or a SAT-based algorithm (NuSMV-SBMC). We considered these to be two different solvers as they often exhibit different behaviours. We use NuSMV-BDD with the options dynamic for dynamic reordering and elbwd for backward image computation, for NuSMV-SBMC we have enabled the completeness check.
The Logics Workbench 1.1 (LWB) [39] contains implementations of two different LTL solvers. The first is a two-pass tableau-based decision procedure developed by Janssen [34] which underlies the provable and satisfiable functions of the pltl module of LWB. In the following we denote this procedure by LWB-SAT. The second is a one-pass tableau calculus by Schwendimann [50] which underlies the model function of the pltl module. In the following we denote this procedure by LWB-MOD. In contrast to LWB-SAT, LWB-MOD returns a model for satisfiable formulae. We again, consider these to be two different solvers as the underlying calculi are distinct.
Leviathan [36] is an LTL satisfiability checking and model building tool that implements a novel one-pass tableau calculus by Reynolds [11, 49].
The pltl [47] system implements two tableau-based methods. The tree method is again based on Schwendimann’s one-pass tableau calculus, the graph method is based on a one-pass and-or tree tableau calculus [26] resulting in a time complexity optimal decision procedure for LTL. We denote the former by pltl (tree) and the latter by pltl (graph). Neither of the two methods returns a model. In this section we will only report results for pltl (graph) as it always performs better than pltl (tree) .
TRP\(^{{\mathtt {++}}}\) 2.2 [54] is based on an ordered resolution calculus that operates on LTL formulae in a clausal normal form [32], while TSPASS [56] extends that calculus to monodic first-order linear time temporal logic over expanding domains [42]. We use TSPASS with the ModelConstruction option so that it returns a model for satisfiable formulae [41]. It should be noted that this model construction potentially requires significantly more resolution inferences to be performed than are necessary to just decide the satisfiability of a formula. Thus, the way we use TSPASS puts it as a distinct performance disadvantage over TRP\(^{{\mathtt {++}}}\) although both perform very similar inference steps when just deciding the satisfiability of an LTL formula.
LS4 [40] is an LTL-prover based on labelled superposition with partial model guidance developed by Suda and Weidenbach [52]. It operates on LTL formulae in the same clausal normal form as TRP\(^{{\mathtt {++}}}\) . LS4 optionally returns a model for satisfiable formulae.
We focus on formulae where differences between the two translations could lead to differences in the behaviour of solvers on these formulae. In particular, for \((\alpha \mathbin {{\mathcal {U}}_{[c_1,c_2]}}\beta )\) or \(\lozenge _{[c_1,c_2]}\beta \), the Strict and Non-Strict Time Difference Translations contain disjunctive subformulae of the form \(\bigvee _{c_1\le j \le c_2} \text { } s^{i}_j\) that have no equivalence in the Strict and Non-Strict Gap Translations of that formula. Each sum variable \(s^{i}_j\) is also subject to the constraints expressed by \(S_C\). The hypothesis is that the Gap Translations lead to better behaviour of solvers on such formulae. On the other hand, for \(\Circle _{[c_1,\infty )}\alpha \) both Gap Translations contain an eventuality formula \(gap \mathbin {{\mathcal {U}}_{}}(\alpha \wedge \lnot gap)\) that is not present in the Time Difference Translations of this formula. Here, the hypothesis is that the Time Difference Translations lead to better behaviour of solvers.
To test our two hypotheses, we consider the unsatisfiable parametrised formulae \(\theta ^1_{b_1}:= \lozenge _{[0,b_1]} p\wedge \Box _{[0,\infty )}\lnot p\) for values of \(b_1\) between 1 and 10, and \(\theta ^2_{b_2}:= \Circle _{[10,\infty )} p\wedge \Circle _{[b_2,\infty )}\lnot p\) for values of \(b_2\) between 10 and 100 in steps of 10.
After transformation to Flat Normal Form, we apply one of the four translations, and run a solver five times on the resulting LTL formula (with a timeout of 1000 CPU seconds), and then determine the median CPU time over those five runs. We refer to that median CPU time as the runtime. The repeated runs are necessary to moderate the fluctuations shown by all LTL solvers in the CPU time used to solve a particular formula. The experiments were conducted on a PC with Intel i7-2600 CPU @ 3.40 GHz and 16 GB main memory.
Recall that for the Time Difference Translations we encode variables of the form \(s^n_m\) with \(n\cdot \mathsf {log}\ m\) variables, where for each n we represent m in binary, e.g., \(s^2_4\) is encoded with \(s^2_2\wedge \lnot s^2_1 \wedge \lnot s^2_0\). In the following tables and graphs we denote this variant by ‘bTD’ to distinguish it from the variant used for related experiments in [33] and denoted by ‘TD’ there.
Tables 5 and 6 show the runtimes for the combination of our translations with the various LTL solvers on \(\theta ^1_{b_1}\), with values of \(b_1\) between 1 and 10, and on \(\theta ^2_{b_2}\), with values of \(b_2\) between 10 and 100 in steps of 10, respectively. An entry ‘T/O’ indicates that the timeout of 1000 CPU seconds was exceeded by an LTL solver while an entry ‘Fail’ indicates that the LTL solver encountered some other error condition and stopped before the timeout was reached. This is often a memory allocation error or some internal data structure running out of space.
Figures 4 and 5 show the same data in the form of ‘heat maps’ where different colours are used to represent different ranges of runtimes. This allows us to easily recognise significant differences in the performance of the various combinations of translations and LTL solver.
Table 5
Runtime, in CPU seconds, required to solve \(\theta ^1_{b_1}=\lozenge _{[0,b_1]} p\wedge \Box _{[0,\infty )}\lnot p\), \(1\le b_1\le 10\), by a particular combination of a translation with respect to the strict/non-strict semantics and an LTL solver
\(b_1\)
TD
Gap
TD
Gap
TD
Gap
TD
Gap
TD
Gap
Aalta
Aalta
Leviathan
Leviathan
LS4
LS4
LWBMOD
LWBMOD
LWBSAT
LWBSAT
Strict semantics
1
0.00
0.00
0.00
0.00
0.00
0.00
0.01
0.01
0.01
0.01
2
0.01
0.00
T/O
T/O
0.00
0.00
0.01
0.01
9.78
0.01
3
0.02
0.00
T/O
T/O
0.00
0.00
0.31
0.01
Fail
0.01
4
0.07
0.00
T/O
T/O
0.00
0.00
5.29
0.01
Fail
0.01
5
2.17
0.00
T/O
T/O
0.00
0.00
58.61
0.01
Fail
0.01
6
2.35
0.00
T/O
T/O
0.01
0.00
T/O
0.01
Fail
0.01
7
Fail
0.00
T/O
T/O
0.03
0.00
T/O
0.01
Fail
0.01
8
Fail
0.00
T/O
T/O
0.05
0.00
T/O
0.01
Fail
0.01
9
Fail
0.00
T/O
T/O
0.09
0.00
T/O
0.01
Fail
0.01
10
Fail
0.00
T/O
T/O
0.15
0.00
T/O
0.01
T/O
0.01
Non-strict semantics
1
0.02
0.00
T/O
T/O
0.00
0.00
0.06
0.01
6.42
0.01
2
0.09
0.00
T/O
T/O
0.00
0.00
36.95
0.01
Fail
0.01
3
1.56
0.00
T/O
T/O
0.02
0.01
T/O
0.01
Fail
0.01
4
4.58
0.00
T/O
T/O
0.09
0.02
T/O
0.01
Fail
0.01
5
4.09
0.00
T/O
T/O
0.33
0.04
T/O
0.01
Fail
0.02
6
40.48
0.00
T/O
T/O
0.99
0.07
T/O
0.02
Fail
0.02
9
Fail
0.01
T/O
T/O
15.38
0.26
T/O
0.06
Fail
0.40
10
Fail
0.01
T/O
T/O
60.83
0.45
T/O
0.12
Fail
1.22
TD
Gap
TD
Gap
TD
Gap
TD
Gap
TD
Gap
NuSMV
NuSMV
NuSMV
NuSMV
pltl
pltl
TRP\(^{{\mathtt {++}}}\)
TRP\(^{{\mathtt {++}}}\)
TSPASS
TSPASS
\(b_1\)
BDD
BDD
SBMC
SBMC
graph
graph
Strict semantics
1
0.01
0.00
0.01
0.00
0.00
0.00
0.00
0.00
0.00
0.00
2
0.27
0.00
0.05
0.01
4.73
0.00
0.00
0.00
0.00
0.00
3
3.57
0.00
0.20
0.01
T/O
0.00
0.00
0.00
0.02
0.00
4
31.39
0.00
0.58
0.02
T/O
0.00
0.01
0.00
0.04
0.00
5
419.95
0.00
1.50
0.02
T/O
0.00
0.03
0.00
0.11
0.00
6
T/O
0.00
3.70
0.02
T/O
0.00
0.91
0.00
4.25
0.00
7
T/O
0.01
8.89
0.03
T/O
0.00
0.19
0.00
0.40
0.00
8
T/O
0.01
18.44
0.04
T/O
0.00
1.51
0.00
11.17
0.00
9
T/O
0.01
36.34
0.05
T/O
0.00
52.02
0.00
T/O
0.00
10
T/O
0.01
68.83
0.07
T/O
0.00
88.16
0.00
T/O
0.00
Non-strict semantics
1
0.11
0.00
182.61
0.05
31.98
0.00
0.65
0.00
0.04
0.00
2
1.10
0.00
T/O
0.11
T/O
0.00
93.63
0.02
5.27
0.02
3
33.94
0.00
T/O
0.23
T/O
0.00
T/O
0.05
33.46
0.03
4
T/O
0.01
T/O
0.48
T/O
0.00
T/O
0.10
439.22
0.04
5
T/O
0.01
T/O
1.01
T/O
0.00
T/O
0.18
T/O
0.07
6
T/O
0.01
T/O
1.82
T/O
0.01
T/O
0.28
T/O
0.10
7
T/O
0.01
T/O
4.13
T/O
0.04
T/O
0.43
T/O
0.14
8
T/O
0.01
T/O
5.06
T/O
0.10
T/O
0.59
T/O
0.19
9
T/O
0.01
T/O
12.16
T/O
0.26
T/O
0.84
T/O
0.25
10
T/O
0.02
T/O
17.11
T/O
0.75
T/O
1.11
T/O
0.33
Table 6
Runtime, in CPU seconds, required to solve \(\theta ^2_{b_2}=\Circle _{[10,\infty )} p\wedge \Circle _{[b_2,\infty )}\lnot p\), \(10\le b_2\le 100\), by a particular combination of a translation with respect to the strict/non-strict semantics and an LTL solver
\(b_2\)
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
Aalta
Aalta
Leviathan
Leviathan
LS4
LS4
LWBMOD
LWBMOD
LWBSAT
LWBSAT
Strict semantics
10
0.00
0.05
0.00
T/O
0.00
0.01
0.01
0.01
0.01
0.01
20
0.00
1.31
T/O
T/O
0.00
0.04
0.01
0.01
0.01
0.01
30
0.00
6.77
T/O
T/O
0.00
0.09
0.01
0.01
0.01
0.01
40
0.00
24.13
T/O
T/O
0.00
0.20
0.01
0.01
0.01
0.01
50
0.00
66.99
T/O
T/O
0.00
0.29
0.01
0.01
0.01
0.01
60
0.00
Fail
T/O
T/O
0.00
0.55
0.01
0.01
0.01
0.01
70
0.00
Fail
T/O
T/O
0.00
0.84
0.01
0.02
0.01
0.01
80
0.00
Fail
T/O
T/O
0.00
0.96
0.02
0.02
0.01
0.01
90
0.00
Fail
T/O
T/O
0.00
1.33
0.01
0.02
0.01
0.01
100
0.00
Fail
T/O
T/O
0.00
2.27
0.01
0.03
0.01
0.01
Non-strict semantics
10
0.00
0.06
0.00
T/O
0.00
0.01
0.01
0.01
0.01
0.01
20
0.00
1.22
Fail
T/O
0.00
0.04
0.01
0.01
0.01
0.01
30
0.00
6.55
Fail
T/O
0.00
0.09
0.01
0.01
0.01
0.01
40
0.00
23.98
Fail
T/O
0.00
0.21
0.01
0.01
0.01
0.01
50
0.00
68.29
Fail
T/O
0.00
0.29
0.01
0.01
0.01
0.01
60
0.00
Fail
Fail
T/O
0.00
0.57
0.01
0.02
0.01
0.01
70
0.00
Fail
Fail
T/O
0.00
0.85
0.01
0.02
0.01
0.01
80
0.00
Fail
Fail
T/O
0.00
0.98
0.01
0.02
0.01
0.01
90
0.00
Fail
Fail
T/O
0.00
1.35
0.01
0.03
0.02
0.01
100
0.00
Fail
Fail
T/O
0.00
2.28
0.01
0.03
0.01
0.01
\(b_2\)
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
bTD +
Gap
NuSMV
NuSMV
NuSMV
NuSMV
pltl
pltl
TRP\(^{{\mathtt {++}}}\)
TRP\(^{{\mathtt {++}}}\)
TSPASS
TSPASS
BDD
BDD
SBMC
SBMC
graph
graph
Strict semantics
10
0.00
0.09
0.00
0.17
0.00
0.00
0.00
0.87
0.00
575.01
20
0.01
0.29
0.01
0.69
0.00
0.00
0.00
64.52
0.00
T/O
30
0.00
0.65
0.01
1.94
0.00
0.00
0.00
441.27
0.01
T/O
40
0.02
1.66
0.02
4.42
0.00
0.00
0.00
93.33
0.02
T/O
50
0.02
3.31
0.02
8.81
0.00
0.00
0.00
T/O
0.04
T/O
60
0.01
3.17
0.01
15.82
0.00
0.00
0.00
T/O
0.08
T/O
70
0.30
5.47
0.07
27.38
0.01
0.00
0.00
T/O
0.18
T/O
80
0.21
23.27
0.06
43.86
0.01
0.00
0.00
T/O
0.27
T/O
90
0.20
9.54
0.05
61.91
0.01
0.00
0.00
T/O
0.40
T/O
100
0.09
11.96
0.04
97.12
0.00
0.00
0.00
T/O
0.59
T/O
Non-strict semantics
10
0.00
0.11
0.01
0.19
0.00
0.00
0.00
0.87
0.00
597.09
20
0.01
0.49
0.01
0.76
0.00
0.00
0.00
65.61
0.00
T/O
30
0.01
0.99
0.00
2.07
0.00
0.00
0.00
499.20
0.01
T/O
40
0.07
1.31
0.02
4.64
0.00
0.00
0.00
96.15
0.02
T/O
50
0.02
1.89
0.02
9.79
0.00
0.00
0.00
T/O
0.04
T/O
60
0.01
7.77
0.01
16.47
0.00
0.00
0.00
T/O
0.07
T/O
70
0.32
6.61
0.06
27.67
0.01
0.00
0.00
T/O
0.17
T/O
80
0.21
21.40
0.06
43.68
0.01
0.00
0.00
T/O
0.27
T/O
90
0.10
10.21
0.05
66.00
0.02
0.00
0.00
T/O
0.40
T/O
100
0.09
22.18
0.04
95.39
0.00
0.00
0.00
T/O
0.59
T/O
Fig. 4
Heat map of the runtimes on \(\theta ^1_{b_1} = \lozenge _{[0,b_1]} p\wedge \Box _{[0,\infty )}\lnot p\). Each rectangle represents the runtime in CPU seconds of a particular combination of a translation with respect to the strict/non-strict semantics and an LTL solver on one instance of \(\theta ^1_{b_1}\), with runtimes given in colours as follows:
×
×
The results in Table 5 and Fig. 4 confirm our hypothesis that on \(\theta ^1_{b_1}\) the Gap translations will lead to better performance than the Time Difference translations. For both the strict and non-strict semantics, for all LTL solvers, and for all values of \(b_1\) considered, the Gap translations result in better or equal performance than the Time Difference translations (highlighted in bold in the Table 5), with the vast majority of entries indicating a significantly worse performance for the Time Difference translations.
Regarding the strict versus the non-strict translations, we would expect that a non-strict translation results in worse performance compared to the corresponding strict translation as the search space for an LTL solver is larger. This is indeed the case for all provers.
The best performing combination is Gap + Aalta. The most ‘robust’ LTL solver, in the sense of producing the lowest total runtime across all translations and all instances of \(\theta ^1_{b_1}\) considered, is LS4.
Fig. 5
Heat map of the runtimes on \(\theta ^2_{b_2}:= \Circle _{[10,\infty )} p\wedge \Circle _{[c_1,\infty )}\lnot p\). Each rectangle represents the runtime in CPU seconds of a particular combination of a translation with respect to the strict/non-strict semantics and an LTL solver on one instance of \(\theta ^2_{b_2}\), with runtimes given in colours as follows:
×
×
The results in Table 6 and Fig. 5 also largely confirm our hypothesis that on \(\theta ^2_{b_2}\) the Time Difference translations will lead to better performance than the Gap translations. In total we have considered ten LTL solvers with two translations under two different semantics, giving us twenty points of comparison between a Time Difference translation and a Gap translation, each over ten instances of \(\theta ^2_{b_2}\). In Table 6 we have highlighted in bold all instances where a Time Difference translation leads to better or equal performance and in italics all instances where the opposite is true. We see that for only seven instances the latter is the case, six of them for pltl (graph).
The reason is that most of background theories \(S_C\) and \(S_C'\) that form part of the Time Difference Translations turn out not to be relevant to the (un)satisfiability of \((\theta ^2_{b_2})^\sharp \). Most provers appear to be able to derive a contradiction without too many inferences involving \(S_C\) or \(S'_C\), while pltl (graph) does not. If one restricts \(S_C\) and \(S'_C\) by hand to smaller sets strictly necessary to establish the (un)satisfiability of \((\theta ^2_{b_2})^\sharp \), then pltl (graph) also performs better with the Time Difference Translations than with the Gap Translations on all instances.
Aalta, LS4 and TRP\(^{{\mathtt {++}}}\) with a Time Difference translation as well as pltl (graph) with a Gap translation can solve all instances in negligible time. The most ‘robust’ LTL solver on \(\theta ^2_{b_2}\) over all translations is pltl (graph).
Overall the evaluation presented in this section confirms that no translation is always strictly ‘better’ than the other. It will depend on the characteristics of the formula and sometimes on the LTL solver whether a Time Difference translation or a Gap translation results in better performance and therefore in a greater likelihood of deciding a formula in reasonable time. However, the experiments also show the significant performance improvements that can be achieved by choosing the ‘right’ translation and, arguably, the simplicity of the Gap translations means that more often than not it is the translation to use. The experimental results presented in the next section provide additional support for this.
7 Examples Revisited
In the following we revisit the examples given in Sect. 3. For the foraging robots, traffic lights and multiprocessor job-shop scheduling scenarios, we have stated a range of properties that we will now attempt to prove using our translations together with the LTL solvers Aalta, Leviathan, LS4, LWB-MOD, LWB-SAT, pltl (graph), NuSMV-BDD, NuSMV-SBMC, TRP\(^{{\mathtt {++}}}\) , and TSPASS. The collection of MTL formulae for the specifications and properties can again be found at [31].
7.1 Foraging Robots
For the foraging robots example we use the specification given in Sect. 3.1 with the maximum time that the robot can be spent resting \(T_r = \infty \), the maximum time that the robot be spent searching for food \(T_s = 5\), and the maximum time that the robot needs to get home with our without food \(T_d = 2\). Let \(\varSigma _{ FR }\) denote the conjunction of the formulae in the specification. We want to prove that the following properties follow from \(\varSigma _{ FR }\):
Having left home the robot will eventually reach home again.
×
The maximum time the robot needs to return home is x
The lowest value x for which we can prove that (\(F_2^x\)) follows from \(\varSigma _{ FR }\) is the maximum time the robot needs to return home. For our choice of \(T_d\), \(T_r\) and \(T_s\) that lowest value of x is 9 and in our experiments we consider \(F_2^8\) and \(F_2^9\), i.e., \(x=8\) and \(x=9\), respectively.
×
The minimum time the robot needs to return home is y.
The highest value y for which we can prove that (\(F_3^y\)) follows from \(\varSigma _{ FR }\) can be proved is the minimum time the robot needs to return home. This value is independent of the choice of \(T_d\), \(T_r\) and \(T_s\), instead it depends on the lower bounds in relevant intervals. For \(\varSigma _{ FR }\) that highest value of y is 3 and in our experiments we consider \(F_3^3\) and \(F_3^4\), i.e., \(y=3\) and \(y=4\), respectively.
×
To prove that \(\varSigma _{ FR }\rightarrow \varphi \) holds, we check the unsatisfiability of \(\varSigma _{ FR }\wedge \lnot \varphi \). In Table 7 we denote \(\varSigma _{ FR }\wedge \lnot \varphi \) by \(\bar{\varphi }\) in the first column. The second column indicates whether \(\bar{\varphi }\) is satisfiable (S) or unsatisfiable (U). The remaining columns of the table show the runtime for each translation and each prover. We again have used a timeout of 1000 CPU seconds and as before ‘T/O’ in the table indicates that a prover was not able to determine the satisfiability of the translated formula within that time while ‘Fail’ indicates that an LTL solver encountered some other error condition and stopped before the timeout was reached.
On all formulae each LTL solver, except TSPASS, performs better with the Gap Translation than with the Time Difference Translation. Only LS4 is able to decide the satisfiability of all formulae with both translations. LWB-MOD and NuSMV-BDD are able to decide the satisfiability of all formulae with the Gap Translation but fail to decide any of the formulae with the Time Difference Translation. The latter is also true for LWB-SAT, pltl, and TRP\(^{{\mathtt {++}}}\) . TSPASS is the only system showing better performance with the Time Difference Translation, it can solve two unsatisfiable formulae with that translation but none with the Gap Translation.
Table 7
Runtime, in CPU seconds, required to solve Foraging Robot properties by a particular combination of a translation and an LTL solver
S
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
Aalta
Aalta
Leviathan
Leviathan
LS4
LS4
LWBMOD
LWBMOD
LWBSAT
LWBSAT
\(\bar{F}_1\)
U
549.99
Fail
T/O
T/O
0.04
0.15
T/O
275.55
T/O
23.33
\(\bar{F}_2^8\)
S
Fail
6.50
Fail
Fail
0.31
0.01
T/O
6.15
T/O
8.67
\(\bar{F}_2^9\)
U
Fail
22.17
Fail
Fail
3.84
0.01
T/O
5.21
T/O
32.23
\(\bar{F}_3^3\)
U
0.92
0.60
T/O
T/O
0.01
0.00
T/O
2.93
T/O
21.49
\(\bar{F}_3^4\)
S
T/O
1.24
T/O
T/O
0.02
0.00
T/O
4.83
T/O
T/O
S
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
NuSMV
NuSMV
NuSMV
NuSMV
pltl
pltl
TRP\(^{{\mathtt {++}}}\)
TRP\(^{{\mathtt {++}}}\)
TSPASS
TSPASS
BDD
BDD
SBMC
SBMC
graph
graph
\(\bar{F}_1\)
U
T/O
1.29
Fail
Fail
T/O
T/O
Fail
T/O
96.95
T/O
\(\bar{F}_2^8\)
S
T/O
2.84
19.70
0.81
T/O
T/O
T/O
T/O
T/O
T/O
\(\bar{F}_2^9\)
U
T/O
2.66
Fail
T/O
T/O
T/O
T/O
T/O
T/O
T/O
\(\bar{F}_3^3\)
U
T/O
1.32
Fail
Fail
T/O
T/O
Fail
T/O
6.73
T/O
\(\bar{F}_3^4\)
S
T/O
1.81
1.90
0.20
T/O
T/O
Fail
T/O
T/O
T/O
7.2 Traffic Lights
For the traffic lights example we use the specification given in Sect. 3.2, denoted by \(\varSigma _{ TR }\). We want to prove that the following properties follow from \(\varSigma _{ TR }\):
Infinitely often each traffic light will be green.
×
If a car is detected on road R1 then the wait will be at most \(x_1\) time units.
This property holds for \(x\ge 3\) but not \(0\le x < 3\). In our experiments we consider \(T_2^2\) and \(T_2^3\), i.e., \(x=2\) and \(x=3\), respectively.
×
If traffic light 2 is currently red then it will be green within 1 to y time units.
This property holds for \(y\ge 7\) but not \(0\le y < 7\). Consequently, we will consider \(T_3^6\) and \(T_3^7\), i.e., \(y=6\) and \(y=7\).
×
If a traffic light is currently amber or red, then a car has to wait at most z time units until the traffic light will be green.
This property should hold for \(z\ge 9\) but not \(0\le z<9\) and we focus on \(T_4^8\) and \(T_4^9\).
×
Table 8
Runtime, in CPU seconds, required to solve traffic lights properties by a particular combination of a translation and an LTL solver
S
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
Aalta
Aalta
Leviathan
Leviathan
LS4
LS4
LWBMOD
LWBMOD
LWBSAT
LWBSAT
\(T_1\)
S
T/O
Fail
Fail
T/O
3.05
T/O
T/O
T/O
T/O
T/O
\(T_2^2\)
S
T/O
Fail
T/O
T/O
0.18
0.18
T/O
T/O
T/O
T/O
\(T_2^3\)
U
4.74
3.14
Fail
Fail
0.01
0.00
T/O
T/O
T/O
T/O
\(T_3^6\)
S
Fail
T/O
Fail
Fail
0.10
0.23
T/O
37.43
T/O
T/O
\(T_3^7\)
U
Fail
Fail
Fail
Fail
4.39
0.82
T/O
T/O
T/O
T/O
\(T_4^8\)
S
Fail
T/O
Fail
Fail
1.08
0.60
T/O
T/O
T/O
T/O
\(T_4^9\)
U
Fail
Fail
Fail
Fail
132.07
0.70
T/O
T/O
T/O
T/O
S
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
NuSMV
NuSMV
NuSMV
NuSMV
pltl
pltl
TRP\(^{{\mathtt {++}}}\)
TRP\(^{{\mathtt {++}}}\)
TSPASS
TSPASS
BDD
BDD
SBMC
SBMC
graph
graph
\(T_1\)
S
T/O
25.09
Fail
T/O
Fail
T/O
T/O
T/O
T/O
T/O
\(T_2^2\)
S
T/O
48.35
4.42
0.27
Fail
T/O
T/O
T/O
T/O
T/O
\(T_2^3\)
U
T/O
9.31
Fail
Fail
Fail
T/O
T/O
T/O
T/O
T/O
\(T_3^6\)
S
T/O
29.93
3.94
1.31
T/O
T/O
T/O
T/O
T/O
T/O
\(T_3^7\)
U
T/O
26.17
Fail
Fail
T/O
T/O
T/O
T/O
T/O
T/O
\(T_4^8\)
S
T/O
203.83
13.71
3.43
T/O
T/O
T/O
T/O
T/O
T/O
\(T_4^9\)
U
T/O
83.85
Fail
Fail
T/O
T/O
T/O
T/O
T/O
T/O
As for the Foraging Robots example, in order to prove \(\varSigma _{ TR }\rightarrow \varphi \) for an MTL formula \(\varphi \), we check the unsatisfiability of \(\varSigma _{ TR }\wedge \lnot \varphi \). In Table 8 we denote \(\varSigma _{ TR }\wedge \lnot \varphi \) by \(\bar{\varphi }\) in the first column. The second column indicates whether \(\bar{\varphi }\) is satisfiable (S) or not (U). The remaining columns show the runtime for each translation and each prover. We have for the first time included results for pltl (tree), as there are instances on which it performs better than pltl (graph).
As we can see, these formulae are much more challenging than those for the Foraging Robots example. This is not surprising if, for instance, one considers the state space of potential models for our specifications. A robot could only be in one of nine states. In contrast, each of the two traffic lights can be in one of four states plus we have a sensor that can be in one of two states. That already gives us 32 global states, only two of which are straightforwardly excluded by the constraint that not both traffic lights can be green at the same time. Furthermore, for the Foraging Robots example we only had one ‘defined’ propositional variable \({\textit{searching}}\) that had a rather straightforward definition while in the Traffic Lights example we have \(change_1\) and \(change_2\) that are subject to much more complicated temporal constraints.
As a consequence, only NuSMV-BDD with the Gap Translation and LS4 with the Time Difference Translation can solve all formulae. For LS4 the Gap Translation still results in better performance on all formulae that can be solved by both translations within the time limit. The same is true for NuSMV-SBMC and for Aalta. LWB-SAT, pltl, TRP\(^{{\mathtt {++}}}\) and TSPASS fail to solve a single formula with either translation within the timeout.
7.3 Multiprocessor Job-Shop Scheduling
Regarding the Multiprocessor Job-shop Scheduling problems (MJS problems for short) we made the simplifying assumption that a job \(j_i\), for each i, \(1\le i\le n\), takes the same amount of time \(t_i\) on whichever machine it is processed on. We can then characterise an MJS problem by stating (i) a job listJ consisting of a list of durations \((t'_1,\ldots ,t'_n)\), (ii) the number k of machines available, and (iii) the time bound t. In Eqs. 15, 16, 22 and 23, for every i, \(1\le i\le n\), and every l, \(1\le l\le k\), \(t_{j_i m_l}\) will be given by \(t'_{j_i}\). The time bound t is used in the formula \(\lozenge _{[0,t]} \bigwedge _{i=1}^{n}hasRun_{j_i}\) that expresses the requirement for a schedule that completes all n jobs on k machines in at most t time points.
It is an interesting characteristic of the MTL formulae for MJS instances that unsatisfiable MTL formulae are smaller than satisfiable MTL formulae. A time bound t that is too small leads to an MJS problem for which no schedule exists that can complete all jobs within the given time bound while a sufficiently large time bound guarantees that such a schedule can be found. By our encodings, a small time bound results in a smaller LTL formula than a large time bound. The difference in size is more pronounced for the Time Difference Translations than for the Gap Translations. This is in contrast to, say, random 3CNF formulae or random modal K3CNF formulae that are often used for benchmarking SAT solvers or modal logic provers, where unsatisfiable formulae tend to be larger than satisfiable formulae.
For our experiments we created 36 MJS problems with a number n of jobs between 1 and 4, a duration \(t'_i\) of a job between 1 and 4, a number k of machines between 1 and 3 and finally a time bound t between 0 and 5. We then constructed MTL formulae for the strict semantics and the non-strict semantics according to the formalisations in Sect. 3.3. Finally, we used a combination of one the encodings with an LTL solver to determine the satisfiability of each MTL formula, or if the LTL solver has that capability, attempt to find a model for it, with a timeout of 1000 CPU seconds.
Table 9
Runtime, in CPU seconds, required to solve MJS problems by a particular combination of a translation with respect to the strict semantics and an LTL solver (LWB-MOD, LWB-SAT, pltl (graph), pltl (tree))
J
k
t
S
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
LWBMOD
LWBMOD
LWBSAT
LWBSAT
pltlgraph
pltlgraph
pltltree
pltltree
1
1
0
U
0.01
0.01
0.01
0.01
0.00
0.00
0.00
0.00
1
1
1
S
0.01
0.01
0.01
0.01
0.00
0.00
0.00
0.00
1
1
2
S
0.05
0.01
89.47
0.01
6.71
0.00
6.68
0.00
1
1
3
S
1.83
0.01
Fail
0.01
T/O
0.00
T/O
0.00
1,2
1
0
U
0.01
0.01
0.01
0.01
0.00
0.00
0.00
0.00
1,2
1
1
U
0.01
0.01
0.34
0.01
964.39
0.11
281.09
0.06
1,2
1
2
U
0.42
0.01
Fail
0.02
T/O
1.65
T/O
0.67
1,2
1
3
S
92.83
0.02
Fail
0.03
T/O
3.29
T/O
1.27
1,2
2
0
U
0.01
0.01
0.01
0.01
0.00
0.00
0.00
0.00
1,2
2
1
U
0.25
0.01
7.45
0.05
T/O
0.84
T/O
1.44
1,2
2
2
S
0.17
0.02
Fail
0.08
T/O
11.80
T/O
18.04
1,2
2
3
S
2.34
0.03
Fail
0.11
T/O
11.79
T/O
18.17
1,1,2
2
0
U
0.01
0.01
0.02
0.01
0.00
0.00
0.00
0.00
1,1,2
2
1
U
0.02
0.02
639.29
9.82
T/O
370.68
T/O
521.65
1,1,2
2
2
S
0.36
0.12
Fail
4.15
T/O
T/O
T/O
T/O
1,1,2
2
3
S
4.04
0.11
Fail
4.07
T/O
T/O
T/O
T/O
1,1,2
3
0
U
0.01
0.01
0.02
0.02
0.00
0.00
0.00
0.00
1,1,2
3
1
U
1.42
0.03
T/O
133.82
T/O
T/O
T/O
T/O
1,1,2
3
2
S
0.82
0.41
Fail
243.63
T/O
T/O
T/O
T/O
1,1,2
3
3
S
3.39
0.18
Fail
247.49
T/O
T/O
T/O
T/O
1,1,2,2
2
0
U
0.01
0.01
0.07
0.06
0.00
0.00
0.00
0.00
1,1,2,2
2
1
U
0.02
0.02
T/O
55.56
T/O
T/O
T/O
T/O
1,1,2,2
2
2
U
6.34
0.73
Fail
207.58
T/O
T/O
T/O
T/O
1,1,2,2
2
3
S
T/O
1.83
Fail
286.03
T/O
T/O
T/O
T/O
1,1,2,2
3
0
U
0.01
0.01
0.03
0.10
0.00
0.00
0.00
0.00
1,1,2,2
3
1
U
0.06
0.05
T/O
T/O
T/O
T/O
T/O
T/O
1,1,2,2
3
2
S
3.75
3.85
Fail
T/O
T/O
T/O
T/O
T/O
1,1,2,2
3
3
S
T/O
2.72
Fail
T/O
T/O
T/O
T/O
T/O
1,2,2,3
2
1
U
0.03
0.02
T/O
80.00
T/O
T/O
T/O
T/O
1,2,2,3
2
2
U
532.16
0.73
Fail
279.51
T/O
T/O
T/O
T/O
1,2,2,3
2
3
U
T/O
4.06
Fail
580.51
T/O
T/O
T/O
T/O
1,2,2,3
2
4
S
T/O
7.71
T/O
T/O
T/O
T/O
T/O
T/O
1,2,3,4
2
2
U
T/O
0.68
T/O
176.96
T/O
T/O
T/O
T/O
1,2,3,4
2
3
U
T/O
4.28
T/O
544.73
T/O
T/O
T/O
T/O
1,2,3,4
2
4
U
T/O
12.98
T/O
T/O
T/O
T/O
T/O
T/O
1,2,3,4
2
5
S
T/O
28.03
T/O
T/O
T/O
T/O
T/O
T/O
Table 10
Runtime, in CPU seconds, required to solve MJS problems by a particular combination of a translation with respect to the strict semantics and an LTL solver (Aalta, Leviathan, TRP\(^{{\mathtt {++}}}\) , TSPASS)
J
k
t
S
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
Aalta
Aalta
Leviathan
Leviathan
TRP\(^{{\mathtt {++}}}\)
TRP\(^{{\mathtt {++}}}\)
TSPASS
TSPASS
1
1
0
U
0.00
0.00
0.62
20.03
0.00
0.00
0.00
0.00
1
1
1
S
0.00
0.00
2.59
T/O
0.00
0.22
0.02
1.11
1
1
2
S
0.02
0.00
Fail
T/O
0.06
0.39
0.13
2.00
1
1
3
S
0.21
0.00
Fail
T/O
T/O
0.52
1.01
7.35
1,2
1
0
U
0.00
0.00
Fail
T/O
0.00
0.00
0.01
0.01
1,2
1
1
U
0.00
0.00
Fail
T/O
0.00
0.00
0.01
0.03
1,2
1
2
U
0.05
0.01
Fail
T/O
1.85
0.16
15.10
0.08
1,2
1
3
S
1.77
0.01
Fail
T/O
T/O
T/O
0.02
259.68
1,2
2
0
U
0.00
0.00
Fail
T/O
0.00
0.00
0.01
0.01
1,2
2
1
U
0.00
0.00
Fail
T/O
0.01
0.04
0.04
0.08
1,2
2
2
S
0.07
0.01
Fail
T/O
739.38
T/O
46.35
34.80
1,2
2
3
S
0.14
0.01
Fail
T/O
T/O
T/O
477.05
118.83
1,1,2
2
0
U
0.00
0.00
Fail
T/O
0.00
0.00
0.01
0.02
1,1,2
2
1
U
0.01
0.01
Fail
T/O
0.00
0.08
0.02
0.20
1,1,2
2
2
S
0.08
0.03
Fail
T/O
T/O
T/O
129.76
943.98
1,1,2
2
3
S
0.49
0.02
Fail
T/O
T/O
T/O
T/O
T/O
1,1,2
3
0
U
0.00
0.00
Fail
T/O
0.00
0.00
0.01
0.02
1,1,2
3
1
U
0.01
0.02
Fail
T/O
0.07
0.33
0.10
0.28
1,1,2
3
2
S
0.07
0.04
Fail
T/O
T/O
T/O
157.11
150.70
1,1,2
3
3
S
0.76
0.03
Fail
T/O
T/O
T/O
T/O
640.67
1,1,2,2
2
0
U
0.00
0.00
Fail
T/O
0.00
0.01
0.02
0.03
1,1,2,2
2
1
U
0.01
0.01
Fail
T/O
0.06
0.20
0.03
0.53
1,1,2,2
2
2
U
0.11
0.07
Fail
T/O
T/O
38.11
T/O
1.83
1,1,2,2
2
3
S
1.01
0.06
Fail
T/O
T/O
T/O
T/O
T/O
1,1,2,2
3
0
U
0.00
0.00
Fail
T/O
0.00
0.02
0.02
0.04
1,1,2,2
3
1
U
0.02
0.02
Fail
T/O
0.31
0.96
0.09
0.76
1,1,2,2
3
2
S
0.28
0.07
Fail
T/O
T/O
T/O
T/O
T/O
1,1,2,2
3
3
S
0.34
0.05
Fail
T/O
T/O
T/O
T/O
T/O
1,2,2,3
2
1
U
0.04
0.01
Fail
T/O
0.13
0.29
0.06
0.73
1,2,2,3
2
2
U
0.52
0.03
Fail
T/O
T/O
382.45
T/O
1.31
1,2,2,3
2
3
U
7.53
0.24
Fail
T/O
T/O
T/O
T/O
591.02
1,2,2,3
2
4
S
13.00
0.28
Fail
T/O
T/O
T/O
T/O
T/O
1,2,3,4
2
2
U
0.94
0.06
Fail
Fail
T/O
T/O
T/O
2.26
1,2,3,4
2
3
U
11.19
0.27
Fail
Fail
T/O
T/O
T/O
15.00
1,2,3,4
2
4
U
T/O
0.66
Fail
Fail
T/O
T/O
T/O
T/O
1,2,3,4
2
5
S
116.90
0.99
Fail
Fail
T/O
T/O
T/O
T/O
Table 11
Runtime, in CPU seconds, required to solve MJS problems by a particular combination of a translation with respect to the strict semantics and an LTL solver (LS4, NuSMV-BDD, NuSMV-SBMC)
J
k
t
S
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
LS4
LS4
NuSMVBDD
NuSMVBDD
NuSMVSBMC
NuSMVSBMC
1
1
0
U
0.00
0.00
0.10
0.01
0.01
0.01
1
1
1
S
0.00
0.00
0.10
0.04
0.04
0.02
1
1
2
S
0.00
0.00
0.61
0.04
0.08
0.02
1
1
3
S
0.00
0.00
3.85
0.05
0.21
0.03
1,2
1
0
U
0.00
0.00
1.40
0.15
0.05
0.02
1,2
1
1
U
0.00
0.00
1.59
0.26
0.08
0.04
1,2
1
2
U
0.00
0.00
2.70
0.26
0.11
0.06
1,2
1
3
S
0.01
0.00
11.08
0.46
0.43
0.11
1,2
2
0
U
0.00
0.00
1.92
0.39
0.07
0.04
1,2
2
1
U
0.00
0.00
1.92
0.59
0.10
0.06
1,2
2
2
S
0.00
0.00
3.66
0.59
0.17
0.12
1,2
2
3
S
0.01
0.00
62.05
0.72
0.32
0.12
1,1,2
2
0
U
0.00
0.00
3.49
1.24
0.10
0.06
1,1,2
2
1
U
0.00
0.00
4.74
1.90
0.14
0.10
1,1,2
2
2
S
0.00
0.00
15.07
1.66
0.29
0.19
1,1,2
2
3
S
0.01
0.00
156.74
2.91
0.50
0.19
1,1,2
3
0
U
0.00
0.00
6.00
3.24
0.12
0.09
1,1,2
3
1
U
0.00
0.00
11.06
4.14
0.18
0.13
1,1,2
3
2
S
0.00
0.00
17.95
8.98
0.28
0.26
1,1,2
3
3
S
0.00
0.00
T/O
13.21
0.47
0.26
1,1,2,2
2
0
U
0.00
0.00
8.47
3.39
0.14
0.10
1,1,2,2
2
1
U
0.00
0.00
16.15
5.63
0.21
0.14
1,1,2,2
2
2
U
0.00
0.00
34.44
15.34
0.29
0.20
1,1,2,2
2
3
S
0.02
0.00
T/O
34.70
0.81
0.37
1,1,2,2
3
0
U
0.00
0.00
14.54
8.59
0.18
0.14
1,1,2,2
3
1
U
0.00
0.00
52.47
14.63
0.27
0.21
1,1,2,2
3
2
S
0.01
0.01
79.05
26.54
0.52
0.39
1,1,2,2
3
3
S
0.01
0.01
T/O
34.65
0.78
0.40
1,2,2,3
2
1
U
0.00
0.00
83.95
7.89
0.37
0.16
1,2,2,3
2
2
U
0.00
0.00
131.15
12.01
0.52
0.22
1,2,2,3
2
3
U
0.01
0.00
197.42
16.62
0.67
0.29
1,2,2,3
2
4
S
0.03
0.01
T/O
21.11
1.78
0.48
1,2,3,4
2
2
U
0.01
0.00
T/O
14.41
0.93
0.23
1,2,3,4
2
3
U
0.04
0.00
888.57
15.89
1.20
0.30
1,2,3,4
2
4
U
0.17
0.02
T/O
48.37
1.50
0.39
1,2,3,4
2
5
S
0.15
0.02
T/O
21.88
3.94
0.61
If an LTL solver reports that the formula resulting from an MJS problem with n jobs, k machines and time bound t is satisfiable, then a schedule exists that completes all n jobs on k machines within t time points. However, this provides us with no information about what that schedule might be. If for a satisfiable formula the LTL solver also returns a model, then the information at which time point \(startRun_{j_im_l}\) (or \(startRun{j_i}\wedge m_l\) for the non-strict semantics) becomes true indicates when a particular job has to be started on a particular machine in order to complete all jobs within the time bound, thus, the model provides us with a schedule.
Among the systems included in our experiments, only Leviathan, LS4, LWB-MOD, NuSMV-BDD, NuSMV-SBMC, and TSPASS can produce models and have been used with the command line options that require them to do so.
Tables 9, 10, 11, 12, 13, 14 show the results for the formalisation of MJS problems in MTL with strict semantics and non-strict semantics, respectively. The first three columns in each table show the job list J, the number k of machines and the time bound t. The fourth column indicates whether the corresponding MTL formula is satisfiable (S) or unsatisfiable (U). The remaining columns of the table show the runtime for each translation and each prover (‘T/O’ indicates timeout, ‘Fail’ indicates that the solver encountered some error condition before reaching the timeout). Figure 6 shows the same data in the form of a heat map.
Regarding the formalisation of MJS problems in the strict semantics, we see in Fig. 6 and Tables 9, 10, 11 for the 296 MJS problem for which an LTL solver can determine its satisfiability with either the Gap or the Time Difference Translation, for 183 problems the Gap Translation results in better performance, for 32 problems the opposite is true, while for 81 problems we get the same performance. The two LTL solvers for which the Time Difference Translation regularly results in better performance are TRP\(^{{\mathtt {++}}}\) and TSPASS. The Gap Translation together with LS4 offers the best performance for every instance.
Table 12
Runtime, in CPU seconds, required to solve MJS problems by a particular combination of a translation with respect to the non-strict semantics and an LTL solver (LWB-MOD, LWB-SAT, pltl (graph), pltl (tree))
J
k
t
S
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
LWBMOD
LWBMOD
LWBSAT
LWBSAT
pltlgraph
pltlgraph
pltltree
pltltree
1
1
0
U
12.28
0.01
Fail
0.01
T/O
0.00
T/O
0.00
1
1
1
S
9.87
0.01
Fail
0.01
T/O
0.01
T/O
0.00
1
1
2
S
11.46
0.01
Fail
0.01
T/O
0.02
T/O
0.01
1
1
3
S
T/O
0.02
Fail
0.01
T/O
0.02
T/O
0.01
1,2
1
0
U
T/O
0.02
Fail
0.08
T/O
1.10
T/O
0.63
1,2
1
1
U
T/O
0.11
Fail
1.68
T/O
15.98
T/O
7.74
1,2
1
2
U
T/O
0.52
Fail
19.16
T/O
120.69
T/O
35.48
1,2
1
3
S
T/O
0.32
Fail
46.44
T/O
586.95
T/O
83.87
1,2
2
0
U
T/O
1.03
Fail
20.39
T/O
T/O
T/O
T/O
1,2
2
1
U
T/O
10.38
Fail
763.74
T/O
T/O
T/O
T/O
1,2
2
2
S
T/O
3.89
Fail
396.55
T/O
T/O
T/O
T/O
1,2
2
3
S
T/O
13.55
Fail
738.24
T/O
T/O
T/O
T/O
1,1,2
2
0
U
T/O
12.50
Fail
T/O
T/O
T/O
T/O
T/O
1,1,2
2
1
U
T/O
782.01
Fail
T/O
T/O
T/O
T/O
T/O
1,1,2
2
2
S
T/O
162.42
Fail
T/O
T/O
T/O
T/O
T/O
1,1,2
2
3
S
T/O
982.67
Fail
T/O
T/O
T/O
T/O
T/O
1,1,2
3
0
U
T/O
T/O
Fail
Fail
T/O
T/O
T/O
T/O
1,1,2
3
1
U
T/O
T/O
Fail
Fail
T/O
T/O
T/O
T/O
1,1,2
3
2
S
T/O
T/O
Fail
Fail
T/O
T/O
T/O
T/O
1,1,2
3
3
S
T/O
T/O
T/O
Fail
T/O
T/O
T/O
T/O
1,1,2,2
2
0
U
T/O
51.83
Fail
T/O
T/O
T/O
T/O
T/O
1,1,2,2
2
1
U
T/O
T/O
Fail
T/O
T/O
T/O
T/O
T/O
1,1,2,2
2
2
U
T/O
T/O
Fail
T/O
T/O
T/O
T/O
T/O
1,1,2,2
2
3
S
T/O
T/O
Fail
T/O
T/O
T/O
T/O
T/O
1,1,2,2
3
0
U
T/O
T/O
Fail
Fail
T/O
T/O
T/O
T/O
1,1,2,2
3
1
U
T/O
T/O
Fail
Fail
T/O
T/O
T/O
T/O
1,1,2,2
3
2
S
T/O
T/O
Fail
Fail
T/O
T/O
T/O
T/O
1,1,2,2
3
3
S
T/O
T/O
Fail
Fail
T/O
T/O
T/O
T/O
1,2,2,3
2
1
U
T/O
T/O
Fail
T/O
T/O
T/O
T/O
T/O
1,2,2,3
2
2
U
T/O
T/O
Fail
T/O
T/O
T/O
T/O
T/O
1,2,2,3
2
3
U
T/O
T/O
Fail
T/O
T/O
T/O
T/O
T/O
1,2,2,3
2
4
S
T/O
T/O
Fail
T/O
T/O
T/O
T/O
T/O
1,2,3,4
2
2
U
T/O
T/O
Fail
T/O
T/O
T/O
T/O
T/O
1,2,3,4
2
3
U
T/O
T/O
Fail
T/O
T/O
T/O
T/O
T/O
1,2,3,4
2
4
U
T/O
T/O
Fail
T/O
T/O
T/O
T/O
T/O
1,2,3,4
2
5
S
T/O
T/O
Fail
T/O
T/O
T/O
T/O
T/O
Table 13
Runtime, in CPU seconds, required to solve MJS problems by a particular combination of a translation with respect to the non-strict semantics and an LTL solver (Aalta, Leviathan, TRP\(^{{\mathtt {++}}}\) , TSPASS)
J
k
t
S
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
Aalta
Aalta
Leviathan
Leviathan
TRP\(^{{\mathtt {++}}}\)
TRP\(^{{\mathtt {++}}}\)
TSPASS
TSPASS
1
1
0
U
0.08
0.01
Fail
T/O
T/O
143.99
448.09
80.30
1
1
1
S
0.01
0.02
T/O
T/O
T/O
T/O
485.57
93.04
1
1
2
S
0.24
0.00
T/O
T/O
T/O
T/O
T/O
461.46
1
1
3
S
0.90
0.01
T/O
T/O
T/O
T/O
T/O
T/O
1,2
1
0
U
2.41
0.06
T/O
Fail
T/O
T/O
T/O
T/O
1,2
1
1
U
9.77
0.20
T/O
Fail
T/O
T/O
T/O
T/O
1,2
1
2
U
13.57
Fail
T/O
Fail
T/O
T/O
T/O
T/O
1,2
1
3
S
10.62
0.10
T/O
Fail
T/O
T/O
T/O
T/O
1,2
2
0
U
3.54
0.29
T/O
Fail
T/O
T/O
T/O
T/O
1,2
2
1
U
3.87
3.92
T/O
Fail
T/O
T/O
T/O
T/O
1,2
2
2
S
Fail
0.72
T/O
Fail
T/O
T/O
T/O
T/O
1,2
2
3
S
3.95
0.18
T/O
Fail
T/O
T/O
T/O
T/O
1,1,2
2
0
U
62.73
2.69
T/O
Fail
T/O
T/O
T/O
T/O
1,1,2
2
1
U
326.11
11.76
T/O
Fail
T/O
T/O
T/O
T/O
1,1,2
2
2
S
Fail
Fail
T/O
Fail
T/O
T/O
T/O
T/O
1,1,2
2
3
S
316.40
1.14
T/O
Fail
T/O
T/O
T/O
T/O
1,1,2
3
0
U
16.59
6.19
T/O
Fail
T/O
T/O
T/O
T/O
1,1,2
3
1
U
Fail
Fail
T/O
Fail
T/O
T/O
T/O
T/O
1,1,2
3
2
S
42.01
1.24
T/O
Fail
T/O
T/O
T/O
T/O
1,1,2
3
3
S
9.95
T/O
T/O
Fail
T/O
T/O
T/O
T/O
1,1,2,2
2
0
U
309.85
3.43
T/O
Fail
T/O
T/O
T/O
T/O
1,1,2,2
2
1
U
408.69
Fail
T/O
Fail
T/O
T/O
T/O
T/O
1,1,2,2
2
2
U
Fail
Fail
T/O
Fail
T/O
T/O
T/O
T/O
1,1,2,2
2
3
S
Fail
Fail
T/O
Fail
T/O
T/O
T/O
T/O
1,1,2,2
3
0
U
487.85
223.50
T/O
Fail
T/O
T/O
T/O
T/O
1,1,2,2
3
1
U
Fail
Fail
T/O
Fail
T/O
T/O
T/O
T/O
1,1,2,2
3
2
S
Fail
Fail
T/O
Fail
T/O
T/O
T/O
T/O
1,1,2,2
3
3
S
Fail
5.38
T/O
Fail
T/O
T/O
T/O
T/O
1,2,2,3
2
1
U
T/O
Fail
T/O
Fail
T/O
T/O
T/O
T/O
1,2,2,3
2
2
U
Fail
Fail
T/O
Fail
T/O
T/O
T/O
T/O
1,2,2,3
2
3
U
Fail
Fail
T/O
Fail
T/O
T/O
T/O
T/O
1,2,2,3
2
4
S
Fail
Fail
T/O
Fail
T/O
T/O
T/O
T/O
1,2,3,4
2
2
U
T/O
Fail
T/O
Fail
T/O
T/O
T/O
T/O
1,2,3,4
2
3
U
Fail
Fail
T/O
Fail
T/O
T/O
T/O
T/O
1,2,3,4
2
4
U
Fail
Fail
T/O
Fail
T/O
T/O
T/O
T/O
1,2,3,4
2
5
S
Fail
Fail
T/O
Fail
T/O
T/O
T/O
T/O
Table 14
Runtime, in CPU seconds, required to solve MJS problems by a particular combination of a translation with respect to the non-strict semantics and an LTL solver (LS4, NuSMV-BDD, NuSMV-SBMC)
J
k
t
S
bTD +
Gap +
bTD +
Gap +
bTD +
Gap +
LS4
LS4
NuSMVBDD
NuSMVBDD
NuSMVSBMC
NuSMVSBMC
1
1
0
U
0.00
0.00
2.66
0.01
Fail
3.05
1
1
1
S
0.00
0.00
3.01
0.05
0.12
0.03
1
1
2
S
0.00
0.00
2.51
0.05
0.13
0.03
1
1
3
S
0.01
0.00
52.36
0.05
0.35
0.03
1,2
1
0
U
0.03
0.00
61.51
0.26
Fail
T/O
1,2
1
1
U
0.05
0.02
421.65
0.28
Fail
T/O
1,2
1
2
U
0.10
34.42
33.54
0.33
Fail
T/O
1,2
1
3
S
0.05
0.01
T/O
0.61
0.70
0.12
1,2
2
0
U
0.07
0.08
34.48
0.79
Fail
Fail
1,2
2
1
U
0.46
1.71
44.12
1.59
Fail
T/O
1,2
2
2
S
0.06
0.03
324.58
4.15
0.62
0.13
1,2
2
3
S
0.04
0.03
614.42
5.95
0.63
0.14
1,1,2
2
0
U
116.57
0.94
T/O
2.97
Fail
T/O
1,1,2
2
1
U
T/O
T/O
T/O
6.03
Fail
T/O
1,1,2
2
2
S
0.10
0.06
217.56
31.27
0.94
0.25
1,1,2
2
3
S
0.08
0.06
T/O
76.94
0.96
0.27
1,1,2
3
0
U
T/O
T/O
87.65
6.48
Fail
T/O
1,1,2
3
1
U
T/O
T/O
T/O
25.01
Fail
T/O
1,1,2
3
2
S
0.10
0.12
T/O
277.16
1.11
0.36
1,1,2
3
3
S
0.11
0.09
T/O
628.20
1.13
0.37
1,1,2,2
2
0
U
T/O
3.21
245.82
5.35
Fail
T/O
1,1,2,2
2
1
U
T/O
T/O
581.67
22.54
Fail
T/O
1,1,2,2
2
2
U
T/O
T/O
T/O
78.75
Fail
T/O
1,1,2,2
2
3
S
0.22
0.16
T/O
409.10
1.51
0.52
1,1,2,2
3
0
U
T/O
T/O
T/O
70.22
Fail
Fail
1,1,2,2
3
1
U
T/O
T/O
T/O
253.77
Fail
T/O
1,1,2,2
3
2
S
0.33
0.28
T/O
T/O
1.75
0.72
1,1,2,2
3
3
S
0.22
0.40
T/O
T/O
1.78
0.70
1,2,2,3
2
1
U
T/O
T/O
T/O
17.76
Fail
Fail
1,2,2,3
2
2
U
T/O
T/O
T/O
103.68
Fail
T/O
1,2,2,3
2
3
U
T/O
T/O
T/O
T/O
Fail
T/O
1,2,2,3
2
4
S
0.76
0.47
T/O
T/O
3.73
0.78
1,2,3,4
2
2
U
T/O
T/O
T/O
127.44
Fail
T/O
1,2,3,4
2
3
U
T/O
T/O
T/O
T/O
Fail
T/O
1,2,3,4
2
4
U
T/O
T/O
T/O
T/O
Fail
T/O
1,2,3,4
2
5
S
2.37
2.90
T/O
T/O
9.71
1.02
Fig. 6
Heat map for the performance of LTL provers on MJS problems. Each rectangle represents the runtime of our two encodings of the MJS problem, with runtimes given in colours as follows:
×
×
Regarding the formalisation of MJS problems in the non-strict semantics, the most striking observation we can make from Fig. 6 and from the data in Tables 12, 13, 14 is how much more challenging the corresponding LTL satisfiability problems are for all the provers. In total there are 36 MJS problems on which we benchmarked 11 LTL solvers / settings with 2 different translations producing a total of 792 results. Of these 449 were timeouts, compared to 206 timeouts for MJS problems in the strict semantics. In a further 130 instances an LTL solver failed, that is, it encountered a memory allocation error, exhausted the limited size of some internal data structure, or produced some other internal failure before reaching the timeout. This compares to 53 failures for the strict semantics. So, in both categories the numbers more than double, resulting only in 213 instances where a combination of a translation with an LTL solver succeeded within the time given compared to 533 instances with the strict semantics.
Overall, the Non-Strict Gap Translation results in better performance than the Non-Strict Time Difference Translation: For the 139 MJS problem where an LTL solver can decide its satisfiability with either the Gap or Time Difference Translation, for 125 of those problems the Non-Strict Gap Translations results in better performance, for 11 problems the opposite is true while for just 3 problems the two encodings result in the same performance. The combination of the Non-Strict Gap Translation and NuSMV-BDD solves the most problems within the time given, 29 out of 36. Of the seven MJS problems that NuSMV-BDD with the Non-Strict Gap Translation cannot solve, four can be solved by both LS4 and NuSMV-SBMC, interestingly, with both the Non-Strict Gap Translation and Non-Strict Time Difference Translation. The best results can be obtained by a combination of the Non-Strict Gap Translation with a portfolio consisting of LS4 and NuSMV-BDD.
It is worth pointing out that MJS is not our intended domain of application for the translations we have presented. There is a lot of symmetry in these problems that a more specialised solver can take advantage of while LTL solvers are oblivious to it, e.g., the order in which jobs are executed on a particular machine does not affect the overall time to completion nor does the choice of machine. However it provides us with a parameterised problem set on which we can experiment for both semantics. For problems containing less symmetry that can naturally be formalised in MTL, and for which scheduling or planning is just one part of it, the approach used here can be beneficial.
In summary, the experimental results presented in this section provide further insights into the differing behaviour of the Gap Translations and Time Difference Translations on a range of examples.
8 Branching Metric Temporal Logic
Combinations of branching temporal logic with quantitative time have been proposed with continuous semantics [4, 8, 44] and with discrete semantics [20]. The logic we propose, which we call \(\text {CTL}_{{\mathsf {M}}}\), is closely related to the logic Complete Real-Time3 Computation Tree Logic (CRTCTL), presented in [20]. The authors show that the complexity of the satisfiability problem for CRTCTL is 2EXPTIME-complete. In the following, we show that the satisfiability problem for \(\text {CTL}_{{\mathsf {M}}}\) is in 2EXPTIME via a translation to CTL. We then explain how to translate CRTCTL to \(\text {CTL}_{{\mathsf {M}}}\), which implies that our upper bound is tight. In this section, our main goal is to introduce \(\text {CTL}_{{\mathsf {M}}}\) and show complexity results for this logic. For this purpose we only need to provide one type of translation. We show that the ‘gap’ translation can be adapted to the branching time setting, under the strict semantics. One could similarly adapt the time difference translation and the non-strict semantics from the linear to the branching case.
We introduce the syntax and semantics of CTL and \(\text {CTL}_{{\mathsf {M}}}\). Let \({\mathcal {P}}\) be a (countably infinite) set of propositional symbols. Well formed formulae in CTL are formed according to the rule:
where \(p \in {\mathcal {P}} \) and \(\mathbf {Q}\in \{\mathbf {E},\mathbf {A}\}\).
As usual, the structure of a CTL model has the shape of an infinite tree. For the purposes of this work, a tree is a pair \(T = (W, <)\) such that (i) ‘<’ is a binary irreflexive and transitive relation over a non-empty set of nodes W and (ii) for all \(w \in W\) the set \(\{w' \in W\mid w' < w\}\) is linearly ordered by ‘<’. It is assumed that T has only one root (i.e. minimal element) denoted by \(\varepsilon \). A path \(\pi \) in a tree \(T = (W,<)\) starting at a node \(w \in W\) is a maximal sequence \(w_0 w_1 \ldots \) with \(w_0 = w\) and \(w_i < w_{i+1}\), for all \(i\ge 0\). We use \(\pi [i]\) to denote \(w_i\). In the following we assume that our trees have a (countably) infinite number of nodes and that our paths are infinite sequences of nodes. The semantics of CTL is defined as follows (we omit propositional cases).
Definition 8
A state tree\(\varrho = (T,\sigma )\) is a pair consisting of a tree \(T = (W,<)\) and a function \(\sigma : W\rightarrow 2^{{\mathcal {P}}}\) that maps every \(w\in W\) to a set of propositional symbols in \({\mathcal {P}}\).
Further connectives are defined as: \({\mathbf {true}} \equiv \lnot ({\mathbf {false}})\), \(\mathbf {Q}({\mathbf {true}} \mathbin {{\mathcal {U}}} \varphi )\equiv \mathbf {Q}(\lozenge \varphi )\), \(\mathbf {A}(\lozenge \varphi )\equiv \lnot \mathbf {E}(\Box \lnot \varphi )\), \(\mathbf {E}(\lozenge \varphi )\equiv \lnot \mathbf {A}(\Box \lnot \varphi )\), where \(\mathbf {Q}\in \{\mathbf {E},\mathbf {A}\}\). A state tree \(\varrho = (T,\sigma )\) is a model of a CTL formula \(\varphi \) iff \((\varrho ,\varepsilon )\models \varphi \). A CTL formula \(\varphi \) is satisfiable iff there exists a model of \(\varphi \) and it is valid iff every state tree is a model of it. \(\text {CTL}_{{\mathsf {M}}}\) formulae are constructed in a way similar to CTL with the difference that path specific operators are constrained by intervals, as in MTL. Well formed formulae in \(\text {CTL}_{{\mathsf {M}}}\) are formed according to the rule:
where \(p \in {\mathcal {P}} \) and \(\mathbf {Q}\in \{\mathbf {E},\mathbf {A}\}\). The semantics of \(\text {CTL}_{{\mathsf {M}}}\) is defined as follows (we omit propositional cases).
Definition 9
A timed state tree\(\varrho = (T,\sigma ,\tau )\) over \((\mathbb {N}, <)\) is a triple consisting of a tree \(T = (W,<)\), a function \(\sigma : W\rightarrow 2^{{\mathcal {P}}}\) that maps every \(w\in W\) to a set of propositional symbols in \({\mathcal {P}}\); and a function \(\tau : W\rightarrow \mathbb {N} \) that maps every \(w\in W\) to a time point \(\tau (w)\) such that, for all paths \(\pi \) in T, \(\tau (\pi [0]) < \tau (\pi [1])\).
The semantics of temporal connectives is then defined as follows.
Further connectives are defined as: \({\mathbf {true}} \equiv \lnot ({\mathbf {false}})\), \(\mathbf {Q}({\mathbf {true}} \mathbin {{\mathcal {U}}_{I}} \varphi )\equiv \mathbf {Q}(\lozenge _{I} \varphi )\), \(\mathbf {A}(\lozenge _{I} \varphi )\equiv \lnot \mathbf {E}(\Box _{I} \lnot \varphi )\), \(\mathbf {E}(\lozenge _{I} \varphi )\equiv \lnot \mathbf {A}(\Box _{I} \lnot \varphi )\), where \(\mathbf {Q}\in \{\mathbf {E},\mathbf {A}\}\). A timed state tree \(\varrho = (T,\sigma ,\tau )\) is a model of a \(\text {CTL}_{{\mathsf {M}}}\) formula \(\varphi \) iff \((\varrho ,\varepsilon )\models \varphi \). A \(\text {CTL}_{{\mathsf {M}}}\) formula \(\varphi \) is satisfiable iff there exists a model of \(\varphi \). A \(\text {CTL}_{{\mathsf {M}}}\) formula \(\varphi \) is in Negation Normal Form (NNF) iff the negation operator (\(\lnot \)) occurs only in front of propositional symbols. To transform a \(\text {CTL}_{{\mathsf {M}}}\) formula into Negation Normal Form, we use \(\mathbf {E}\tilde{{\mathcal {U}}}_I\) and \(\mathbf {A}\tilde{{\mathcal {U}}}_I\), defined as \(\mathbf {E}(\varphi \mathbin {\tilde{{\mathcal {U}}}_{I}} \psi ) \equiv \lnot \mathbf {A}(\lnot \varphi \mathbin {{\mathcal {U}}_{I}} \lnot \psi )\) and \(\mathbf {A}(\varphi \mathbin {\tilde{{\mathcal {U}}}_{I}} \psi ) \equiv \lnot \mathbf {E}(\lnot \varphi \mathbin {{\mathcal {U}}_{I}} \lnot \psi )\). A \(\text {CTL}_{{\mathsf {M}}}\) formula \(\varphi \) is in Flat Normal Form (FNF) iff it is of the form \(p_0 \wedge \bigwedge _i \mathbf {A}(\Box _{[0,\infty )}(p_i \rightarrow \psi _i))\) where \(p_0, p_i\) are propositional variables or \({\mathbf {true}} \) and \(\psi _i\) is either a formula of propositional logic or it is of the form \(\mathbf {Q} \Circle _{I} \psi _1 \), \(\mathbf {Q}(\psi _1 \mathbin {{\mathcal {U}}_{I}} \psi _2)\) or \(\mathbf {Q}(\psi _1 \mathbin {\tilde{{\mathcal {U}}}_{I}} \psi _2)\) where \(\psi _1, \psi _2\) are formulae of propositional logic and \(\mathbf {Q}\in \{\mathbf {E},\mathbf {A}\}\).
8.1 \(\text {CTL}_{{\mathsf {M}}}\) to CTL Translation: Encoding ‘Gaps’
Assume that our \(\text {CTL}_{{\mathsf {M}}}\) formulae are in NNF and FNF. We translate \(\text {CTL}_{{\mathsf {M}}}\) formulae over timed state trees into CTL using gap, a fresh propositional symbol, similar to what we did with our first translation from MTL to LTL. For this, we need to map each timed state tree \(\varrho = (T,\sigma ,\tau )\) to a state tree \(\varrho '\) such that \(\varrho \) is a model of a \(\text {CTL}_{{\mathsf {M}}}\) formula if, and only if, \(\varrho '\) is a model of our CTL translation. We now define our mappings between \(\text {CTL}_{{\mathsf {M}}}\) and CTL models.
Let \(\varrho = (T,\sigma ,\tau )\) with \(T = (W,<)\) be a timed state tree. With every \(w,w'\in W\) and \(k\in {\mathbb {N}}\) we uniquely associate a new node \(w''_{(w,w',k)}\). To simplify notation, in the following we denote \(w''_{(w,w',k)}\) by \(wg^kw'\).
Definition 10
Given a timed state tree \(\varrho = (T,\sigma ,\tau )\) with \(T = (W,<)\), we define a state tree \((T',\sigma ')\) with \(T' = (W',<')\), as follows:
We call nodes of the form \(wg^k w'\) ‘gap’ nodes.4 We now define \(<'\) as the transitive closure of all of the following:
1.
\(w <' wgw'\), if \(wgw'\in W'\);
2.
\(wg^k w' <' wg^{k+1}w'\);
3.
\(wg^k w'<' w'\), if \(wg^{k+1} w'\not \in W'\);
4.
\(w <' w'\) if \(wgw'\not \in W'\) and \(w < w'\);
For a ‘gap’ node \(wg^k w'\), we define \(\sigma '(wg^k w') = \{gap\}\) and, for \(w \in W\), we define \(\sigma '(w) = \sigma (w)\).
Intuitively, in Point (1) we relate a node in \(W'\) to a ‘gap’ node; in Point (2) we relate two consecutive ‘gap’ nodes; in Point (3) we relate the last of a sequence of ‘gap’ nodes to a node in \(W'\); finally in Point (4) we relate two non-‘gap’ nodes in \(W'\) if there is no gap between them, i.e, when \(\tau (w')-\tau (w) =1\).
\(\text {CTL}_{{\mathsf {M}}}\) to CTL translation using ‘gap’ where \(\mathbf {Q}\in \{\mathbf {E},\mathbf {A}\}\) and \(\alpha ,\beta \) are propositional logic formulae and \(c_1,c_2 > 0\)
Figure 7 illustrates the mapping given by Definition 10. For instance, if \(\varrho = (T,\sigma ,\tau )\) is the timed state tree on the left side of Fig. 7 and \(\sigma (w_1) = \{p\}\) then \((\varrho ,\varepsilon )\models \mathbf {E}\Circle _{[2,3]} p\). Table 15 presents our translation. As shown in Table 15, we translate \(\mathbf {E}\Circle _{[2,3]} p\) into:
Note that the state tree represented on the right side of Fig. 7 is a model of this CTL formula. Since gap is a propositional symbol not occurring in \(\varrho \), the states from \(W \subseteq W'\) do not contain gap.
The next proposition follows straightforwardly from Definition 10.
Proposition 6
Given a timed state tree \(\varrho = (T,\sigma ,\tau )\), let \(\varrho '\) be as in Definition 10. Then, \((\varrho ',\varepsilon )\models \lnot gap\wedge \mathbf {A}( \Box (\mathbf {A} \lozenge \lnot gap ))\).
Definition 11
Given a state tree \(\varrho ' = (T',\sigma ')\) with \(T' = (W',<')\) such that \((\varrho ',\varepsilon )\models \lnot gap\wedge \mathbf {A}( \Box (\mathbf {A} \lozenge \lnot gap ))\), we define \(\varrho = (T,\sigma ,\tau )\), with \(T = (W,< )\), as follows. We start by defining W and \(\sigma \).
$$\begin{aligned} W = \{w\mid w \in W' \text {, } gap \not \in \sigma '(w)\} \quad \text { and}\quad \sigma (w) = \sigma '(w)\text { for all }w \in W. \end{aligned}$$
It remains to define \(\tau \) and <. For any distinct \(w, w' \in W\), we define < as the transitive closure of:
\(w < w' \text { iff there is a path } \pi \) in \(T'\) such that \(\pi [0] = w\) and there is \( k \in \mathbb {N}\) with \(\pi [k] = w'\) and \(\forall j\), \(0< j < k\), \(gap \in \sigma '(\pi [j])\).
To define \(\tau \), we first set \(\tau (\varepsilon ) = 0\). Now, for any distinct \(w< w' \in W\), there is a path \(\pi \) in \(T'\) such that \(\pi [0] = w\) and there is \(k \in \mathbb {N}\) with \(\pi [k] = w'\) and \(\forall j\), \(0< j < k\), \(gap \in \sigma '(\pi [j])\). Observe that such k is unique and we set \(\tau (w') = \tau (w)+k\).
As \(\varrho '\) is such that \((\varrho ',\varepsilon )\models \lnot gap\wedge \mathbf {A}( \Box (\mathbf {A} \lozenge \lnot gap ))\), for each \(w \in W\), we define \(\tau (w)\in \mathbb {N}\). Also, for all \(\pi \) in T, \(\tau (\pi [1])>\tau (\pi [0])\), and so, \(\tau :W\rightarrow \mathbb {N}\) is well defined. The following proposition states this property.
Proposition 7
Given a state tree \(\varrho '\) such that \((\varrho ',\varepsilon )\models \lnot gap\wedge \mathbf {A} \Box (\mathbf {A} \lozenge \lnot gap )\), let \(\varrho = (T,\sigma ,\tau )\) be as in Definition 11. Then, \(\tau :W\rightarrow \mathbb {N}\) is a function such that \(\tau (\pi [0])<\tau (\pi [1])\), for all paths \(\pi \) in T.
We are ready for Theorem 6, which shows correctness of our translation from \(\text {CTL}_{{\mathsf {M}}}\) to CTL using ‘gap’s.
Theorem 6
Let \(\varphi = p_0 \wedge \bigwedge _i \mathbf {A}(\Box _{[0,\infty )}(p_i \rightarrow \psi _i))\) be an \(\text {CTL}_{{\mathsf {M}}}\) formula in NNF and FNF. Let \(\varphi ^{\sharp } = p_0 \wedge \bigwedge _i\mathbf {A}(\Box (p_i \rightarrow (\lnot gap \wedge \psi _i^\sharp )))\) be the result of replacing each \(\psi _i\) in \(\varphi \) by \(\psi _i^\sharp \) as in Table 15. Then, \(\varphi \) is satisfiable if, and only if, \(\varphi ^{\sharp }\wedge \lnot gap \wedge \mathbf {A}(\Box ( \mathbf {A} \lozenge \lnot gap))\) is satisfiable.
Proof
\(\varphi \) is satisfiable if, and only if, there is a timed state tree \(\varrho = (T,\sigma ,\tau )\) such that \((\varrho ,\varepsilon )\models \varphi \). Given a timed state tree \(\varrho = (T,\sigma ,\tau )\), let \(\varrho ' = (T',\sigma ')\) be as in Definition 10. By Proposition 6, \((\varrho ',\varepsilon )\models \lnot gap\wedge \mathbf {A}(\Box ( \mathbf {A} \lozenge \lnot gap))\). By definition of \(\varrho '\), for all \(w\in W\) and all propositional variables \(p_i\) occurring in \(\sigma (w)\), we have \((\varrho ,w)\models p_i\) iff \((\varrho ',w)\models p_i\). With an inductive argument one can show that, for any propositional formula \(\alpha \), \((\varrho ,w)\models \alpha \) iff \((\varrho ',w)\models \alpha \).
Also, \(\varphi ^{\sharp }\wedge \lnot gap \wedge \mathbf {A}(\Box ( \mathbf {A} \lozenge \lnot gap))\) is satisfiable if, and only if, there is a state tree \(\varrho ' = (T,\sigma ')\) such that \((\varrho ',\varepsilon )\models \varphi ^{\sharp }\wedge \lnot gap \wedge \mathbf {A}(\Box ( \mathbf {A} \lozenge \lnot gap ))\). Given \(\varrho '\), let \(\varrho = (T,\sigma ,\tau )\) be a timed state tree as in Definition 11. By Proposition 7, \(\tau :W\rightarrow \mathbb {N}\) is well defined. By definition of \(\varrho \), for all \(w\in W'\) with \(gap \not \in \sigma '(w)\), we have that for \(p_i\) a propositional variable occurring in \(\sigma '(w)\), \((\varrho ,w)\models p_i\) iff \((\varrho ',w)\models p_i\). As before, an inductive argument lifts this claim to propositional formulae. That is, for any propositional formula \(\alpha \), \((\varrho ,w)\models \alpha \) iff \((\varrho ',w)\models \alpha \).
Thus, following our translation in Table 15, we only need to show correspondences between \(\psi _i\) and \(\lnot gap \wedge \psi _i^\sharp \). This follows from Claims 7–9 below (other cases are similar).
In our claims, we use the following bijection between (infinite) paths \(\pi \) in T and \(\pi '\) in \(T'\), which is implied by Definitions 10 and 11: \(\pi \sim \pi '\) if, and only if, \(\pi [0]=\pi '[0]\) and \(\forall j \in \mathbb {N}\), \(\pi [j]=\pi '[k]\), where \(\tau (\pi [j])-\tau (\pi [0])=k\). We now argue that, for all natural numbers \(c_1,c_2\) with \(0<c_1\le c_2 <C\), the following claims hold.
\((\varrho ,w)\models \mathbf {A} \Circle _{[c_1,c_2]}\alpha \) iff for each \( \pi \) in T with \(\pi [0] = w\), we have \(\tau (\pi [1]) \in \tau (w) + [c_1,c_2]\) and \((\varrho ,\pi [1])\models \alpha \). By Definitions 10 and 11, this happens iff there is a \(\pi '\) in \(T'\) such that \(\pi \sim \pi '\) and, for \(k=\tau (\pi [1])-\tau (\pi [0])\), \((\varrho ',\pi '[k])\models \lnot gap \wedge \alpha \) and \(\forall j \in \mathbb {N}\) with \(0< j < k\), \((\varrho ',\pi '[j])\models gap \). Since \(\pi \) was arbitrary, this holds for all such \(\pi \). As \(\sim \) is a bijection, we obtain this for all such \(\pi '\) in \(T'\). Then, \((\varrho ,w)\models \mathbf {A} \Circle _{[c_1,c_2]}\alpha \) iff \((\varrho ',w)\models \lnot gap \wedge (\mathbf {A} \Circle _{[c_1,c_2]}\alpha )^\sharp \).
\((\varrho ,w)\models \mathbf {A}(\alpha \mathbin {{\mathcal {U}}_{[c_1,c_2]}}\beta )\) iff for each \( \pi \) in T with \(\pi [0] = w\), there is \(k \in \mathbb {N}\) such that \(\tau (\pi [k]) \in \tau (w) + [c_1,c_2]\) and \((\varrho ,\pi [k])\models \beta \); and \(\forall j \in \mathbb {N}\), \(0 \le j < k\) implies \((\varrho ,\pi [j])\models \alpha \). By Definitions 10 and 11, this happens iff there is a \(\pi '\) in \(T'\) such that \(\pi \sim \pi '\) and, for \(k'=\tau (\pi [k])-\tau (\pi [0])\), \((\varrho ',\pi '[k'])\models \lnot gap \wedge \beta \) and \(\forall j \in \mathbb {N}\) with \(0 \le j < k'\), \((\varrho ',\pi '[j])\models gap \vee \alpha \). Since \(\pi \) was arbitrary, this holds for all such \(\pi \). As \(\sim \) is a bijection, we obtain this for all such \(\pi '\) in \(T'\). Thus, \((\varrho ,w)\models \mathbf {A}(\alpha \mathbin {{\mathcal {U}}_{[c_1,c_2]}}\beta )\) iff \((\varrho ',w)\models \lnot gap \wedge (\mathbf {A}(\alpha \mathbin {{\mathcal {U}}_{[c_1,c_2]}}\beta ))^\sharp \).
By semantics of \(\mathbf {E}\tilde{{\mathcal {U}}}_I\), we have that \((\varrho ,w) \models \mathbf {E}(\alpha \mathbin {\tilde{{\mathcal {U}}}_{[c_1,c_2]}}\beta )\) iff \((\varrho ,w)\models \lnot (\mathbf {A}(\lnot (\alpha )\mathbin {{\mathcal {U}}_{[c_1,c_2]}}\lnot (\beta )))\). By Claim 8, \((\varrho ,w)\not \models \mathbf {A}(\lnot (\alpha )\mathbin {{\mathcal {U}}_{[c_1,c_2]}}\lnot (\beta ))\) iff \((\varrho ',w)\not \models \lnot gap \wedge (\mathbf {A}(\alpha \mathbin {{\mathcal {U}}_{[c_1,c_2]}}\beta ))^\sharp \). As \((\varrho ',w)\models \lnot gap\) (by definition of \((\varrho ',w)\)), we have that \((\varrho ',w)\not \models (\mathbf {A}(\alpha \mathbin {{\mathcal {U}}_{[c_1,c_2]}}\beta ))^\sharp \). Then, \((\varrho ,w)\models \mathbf {E}(\alpha \mathbin {\tilde{{\mathcal {U}}}_{[c_1,c_2]}}\beta )\) iff \((\varrho ',w)\models \lnot gap \wedge \lnot (\mathbf {A}(\lnot (\alpha )\mathbin {{\mathcal {U}}_{[c_1,c_2]}}\lnot (\beta )))^\sharp \). \(\square \)
Due to the binary encoding of constants, our translation is exponential in the size of the input. Then, since satisfiability of CTL can be decided in EXPTIME [21], we obtain 2EXPTIME as upper bound of this problem for \(\text {CTL}_{{\mathsf {M}}}\). Our lower bound follows from the fact that we can translate CRTCTL (which is 2EXPTIME-complete), presented in [20], to \(\text {CTL}_{{\mathsf {M}}}\). In CRTCTL, the models are the same as in CTL (infinite trees with a labelling function that maps nodes to propositional symbols) and the syntax extends CTL with formulae of the form \(\mathbf {Q} (\phi \mathbin {{\mathcal {U}}} ^{\le k} \psi )\) and \(\mathbf {Q} (\phi \mathbin {{\mathcal {U}}} ^{= k} \psi )\), where \(\mathbf {Q} \in \{\mathbf {A},\mathbf {E}\}\) and \(k \in \mathbb {N}\). For example, \(\mathbf {E} ({\mathbf {true}} \mathbin {{\mathcal {U}}} ^{\le 5} p)\) means that there is a path in which p occurs within 5 states from now. In fact, we can see CRTCTL models as a special case of \(\text {CTL}_{{\mathsf {M}}}\) models where time differences from one state to another can only be 1. Then, one can easily translate CRTCTL formulae into \(\text {CTL}_{{\mathsf {M}}}\) by replacing temporal operators \(\mathbin {{\mathcal {U}}} ^{\le k}\) with \(\mathbin {{\mathcal {U}}_{[0,k]}}\) and \(\mathbin {{\mathcal {U}}} ^{= k}\) with \(\mathbin {{\mathcal {U}}_{[k,k]}}\). For the CTL temporal operators we add the interval \([0,\infty )\). Finally we include \(\mathbf {A} \Box _{[0,\infty )} (\Circle _{[1,1]} {\mathbf {true}})\) to ensure that the time difference between states is always 1. For example, we translate \(\mathbf {E}\Circle p \wedge \mathbf {A}(p\mathbin {{\mathcal {U}}} ^{\le 3} q)\) into \(\mathbf {E}\Circle _{[0,\infty )} p \wedge \mathbf {A}(p\mathbin {{\mathcal {U}}_{[0, 3]}} q) \wedge \mathbf {A} \Box _{[0,\infty )} (\Circle _{[1,1]} {\mathbf {true}})\).
Theorem 7
Satisfiability of \(\text {CTL}_{{\mathsf {M}}}\) is 2EXPTIME-complete.
9 Related Work
As already mentioned in the introduction, propositional MTL has been proposed in the 90’s by Alur and Henzinger [6, 7] as a formalism for specifying quantitative temporal constraints. More recently, combinations of MTL with Description Logic [9, 29] and Datalog [13, 14] have also been investigated.
Since its proposal, several authors have used MTL to specify problems from a range of domains (security, robotics, among others). Karaman and Frazzoli use a fragment of MTL to specify some aspects of Vehicle Routing Problems (VRP) [35]. VRPs are a generalisation of the traveling salesman problem with a fleet of vehicles leaving from and returning to one or more departure locations, to delivery locations via a network of communication links e.g. roads or rail tracks, that also must satisfy certain constraints and minimizes transportation costs. In the mentioned work, their focus is on Unmanned Aerial Vehicles (UAVs) with target, launch and landing sites, times spent at the locations, as well as between them and parameters relating to relative risk for using a particular UAV and the time a UAV can be used without re-fueling [35]. This is solved by developing a Mixed-Integer Linear Programming (MILP) algorithm. The style of these problems is very similar to the job-shop scheduling examples we provided in Sect. 3.3, but an important difference is that problem specifications are not fully given in a logical formalism. A similar approach is taken by Zhou et al. [59], they applied a variant of MTL to formalise some constraints in motion planning problems in a dynamic environment for a UAV and for a car. Again, problems are translated into MILP.
Luo et. al define SMTL, an augmented version of a fragment of MTL, suitable for Scheduling Algorithms [43]. This language differs from ours as it has no next operator and the semantics is not pointwise. Fragments of SMTL are considered by restricting aspects of the language so each event can only occur a fixed number of times. They provide examples discussing how these fragments can be used to specify both Job Shop Scheduling and Temporal Networks. To find a schedule, a translation is provided into first order temporal logic and then to Satisfiability Modulo Theory (SMT).
Hoxha et. al describe a tool (Visual Specification Tool, VISPEC) that allows users that are not expert in logics or MTL to specify problems using a graphical formalism [30]. This is automatically translated into MTL. A usability study of the tool is provided and two applications relating to robot surgery and quadcopters are presented. The focus is on specifications rather than satisfiability checking that we consider here.
The robustness of signals modelling or controlling physical processes is considered by Fainekos and Pappas [22]. Robustness relates to how much a trajectory can be perturbed without changing the truth value of a specification expressed in the LTL or MTL. This work is used by Alqahtani et. al to consider safety in relation to path planning applied to an autonomous drone in an adversarial environment where specifications are given in MTL [3]. Robustness is further considered by Abbas et. al in the context of cyber physical systems [2]. They provide a testing framework that returns counterexamples using an MTL specification that minimises a robustness metric.
Thati and Roşu propose a runtime verification and monitoring approach for checking MTL formulae over execution traces of algorithms [53]. An algorithm is presented where both past and future-time MTL formulae are checked against timestamped execution traces. As we do, the authors also restrict the intervals on temporal operators to be natural numbers (or infinity) but also allow past-time operators. Models are timed state sequences allowing real-valued time points. Two subsets of MTL are also considered limiting the specifications to be checked to past-time MTL formulae and LTL. We note that this is a runtime verification approach rather than related to theorem proving.
A runtime verification and monitoring approach using MTL specifications applied to the security domain is presented by Gunadi and Tiu [28]. In particular, the authors consider the privilege escalation attack in the Android operating system. A privilege escalation attack occurs when access services or resources that the attacker doesn’t have permissions for is obtained. The past-time fragment of MTL is considered and models are based on the natural numbers and the intervals on temporal operators are natural numbers (where the left hand side is always 0). Similarly to the work by Thati and Roşu [53], the focus is on presenting and implementing an algorithm to check formulae over traces along with its application to the privilege escalation attack.
10 Conclusions
This work considers MTL, a temporal logic that allows timing constraints on the temporal operators, with a pointwise semantics over the natural numbers. We presented four satisfiability preserving translations from MTL to LTL. The translations using time difference are based on the MTL decision procedure presented in [6] and use the bounded model property. Note that the translations using ‘gap’ are proved independently of this property.
Our translations provide a route to practical reasoning about MTL over the naturals via LTL solvers. We specified examples from robotics, traffic management, and scheduling using MTL. Modelling these examples showed that using the next operator to specify the timing constraints on the next state a robot can move into acts a synchronisation point for all robots in multi-robot systems. Additional care has to be taken using until or eventually operators with intervals where the left hand side is greater than zero (for example \(\mathbin {{\mathcal {U}}_{[1,8]}}\)) in the scope of an always operator \(\Box _{[0,\infty )}\) as this can inadvertently lead to unsatisfiable timing constraints.
For the scheduling example we gave specifications based both on the strict semantics and on the non-strict semantics of MTL. We then used ten different LTL solvers to explore the extent these can solve satisfiability problems based on these specifications. Our experiments seem to indicate that (i) a formalisation based on the non-strict semantics results in poor performance compared to a formalisation based on the strict semantics, (ii) for the vast majority of problems a Gap translation results in better performance than a Time Difference translation, and (iii) LTL solvers that consistently perform well on translated formulae meaning a combination of translation and use of an LTL solver provides a viable means for MTL satisfiability checking and MTL theorem proving.
We have explored the question on what classes of formulae the use of each translation could be advantageous. We have defined two sets of parametrised formulae and again used a range of LTL solvers to verify that for one a Gap translation results in better performance while for the other the Time translation leads to better performance.
We also introduced an branching-time variant of MTL and provided a translation using ‘gaps’ into the branching-time temporal logic CTL. This opens up the opportunity to use CTL solvers such as [58] in a similar way as we have done for LTL solvers.
As future work, we intend to investigate whether we can translate PDDL3.0 statements [25] into MTL and apply our translations to the planning domain.
Open AccessThis article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
We write \(\mathsf{min}(l+k,2\cdot C)\) for the minimum between \(l+k\) and \(2\cdot C\). If the minimum is \(2\cdot C\) then \( s^{j+1}_{2\cdot C} \) means that the sum of the last \(j+1\) variables is greater or equal to \(2\cdot C\).
