# 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).