Metric Temporal Logic: Tools and Experiments
Metric Temporal Logics are extensions of Linear Time Temporal Logic (LTL) that allow us to express timining constraints on temporal operators: While in LTL we can express that a proposition p eventually becomes true, in a Metric Temporal Logic we can express that it becomes true within in an interval I. A range of Metric Temporal Logic exists that differ with respect to the temporal operators that are allowed, whether the bounds of intervals are real numbers or natural numbers, whether unbounded intervals are allowed, and regarding the underlying semantics.
Hustadt, Ozaki and Dixon (2017) consider Metric Temporal Logic over the Naturals (MTL): All operators of LTL (next, until, always, eventually) are allowed and are constrained by intervals; the lower bound of an interval is a natural number, the upper bound of an interval is also a natural number or infinity. Following Alur and Henzinger (1993) we use a pointwise semantics over the natural numbers consisting of a sequence of states and a function mapping states to time points on a time line isomorphic to the natural numbers. We consider two variants of this semantics: In the non-strict semantics 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. In the strict semantics the mapping is given by a strictly monotonic function, which forces time to progress from one state to another.
In order to facilitate reasoning in Metric Temporal Logic with strict semantics we have devised two translations from MTL to LTL: (i) the Time Difference Translation for strict semantics which is inspired by Alur and Henzinger (1993) where fresh propositional variables encode time differences between states, and (ii) the Gap Translation for strict semantics which uses a fresh propositional variable called gap to encode the jumps between states. For reasoning in Metric Temporal Logic with non-strict semantics we specify variations of these two translations: (iii) the Time Difference Translation for non-strict semantics requires an additional propositional variable that encodes a time difference of zero between states, and (iv) the Gap Translation for non-strict semantics requires an additional propositional variable called same to identify states that are mapped to the same time point as the previous state.
Software
The translations have been implemented in SWI-Prolog and are available as mtl.tgz. This collection also contains files necessary to replicate the experiments described in Hustadt, Ozaki and Dixon (2017) (see also below). Download mtl.tgz, unpack it in a suitable location on your system, and read the files INSTALL and README for further instructions.
Comparison of the translations
In order to empirically evaluate the translations, we have used the translation together with a range of LTL satisfiability solvers on formulae where differences between the translations could lead to differences in the behaviour of solvers. In particular, for we haved considered the unsatisfiable parameterised formulae $\theta^1_{b_1} := \Diamond_{[0,b_1]} p\land\Box_{[0,\infty)}\neg p$ for values of $b_1$ between 0 and 10, and $\theta^2_{b_2} := \bigcirc_{[10,\infty)} p\land\bigcirc_{[b_2,\infty)}\neg p$ for values of $b_2$ between 10 and 20. For further details see Sections 5 and Appendix C of Hustadt, Ozaki and Dixon (2017).
Results for $\theta^1_{b_1}$
The heat map below shows the results for $\theta^1_{b_1} = \Diamond_{[0,b_1]} p\land\Box_{[0,\infty)}\neg p$ with $b_1$ ranging from 0 to 10 (x-axis) using the Time Difference and Gap translations together with various of LTL solvers. Hover over a rectangle in the heat map to see the runtime of the corresponding combination of translation and prover on a particular instance of $\theta^1_{b_1}$.
Results for $\theta^2_{b_2}$
The heat map below shows the results for $\theta^2_{b_2} = \bigcirc_{[10,\infty)} p\land\bigcirc_{[b_2,\infty)}\neg p$ with $b_2$ ranging from 10 to 20 (x-axis) using the Time Difference and Gap translations together with various of LTL solvers. Hover over a rectangle in the heat map to see the runtime of the corresponding combination of translation and prover on a particular instance of $\theta^2_{b_2}$.
Multiprocessor Job-shop Scheduling
In Section 6 of Hustadt, Ozaki and Dixon (2017) we have given formalisations of Multiprocessor Job-shop Scheduling (MJS) problems in MTL with respect both to the strict semantics and the non-strict semantic. Essentially, a Multiprocessor Job-shop Scheduling problem is the problem of finding a schedule that allows $N$ jobs to be run and completed on $M$ machines within a bound of $B$ time points. In general, the time it takes a particular job to be completed depends on the specific machine it runs on, though in our experiments we have assumed that a job takes the same time on any machine.
Results for Multiprocessor Job-shop Scheduling problems
We have conducted experiments on a range of MJS problems. In particular, we have varied the number $N$ of jobs between 1 and 4, the time that each job takes to be completed between 1 and 4, the number $M$ of machines between 1 and 3, and the time bound $B$ between 0 and 5. The heat map below shows the results we have obtained with combinations of translations and provers for both the strict and the non-strict semantics. Hover over a rectangle in the heat map to see the runtime of the corresponding combination of translation and prover on a particular MJS problem. For further details see Sections 6 and Appendix D of Hustadt, Ozaki and Dixon (2017).