Theorem Proving for Pointwise Metric Temporal Logic Over the Naturals via Translations
- PDF / 1,011,887 Bytes
- 58 Pages / 439.37 x 666.142 pts Page_size
- 91 Downloads / 192 Views
Theorem Proving for Pointwise Metric Temporal Logic Over the Naturals via Translations Ullrich Hustadt1
· Ana Ozaki2
· Clare Dixon1
Received: 31 May 2019 / Accepted: 6 January 2020 © The Author(s) 2020
Abstract 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. Keywords Metric temporal logic · Theorem proving · Modelling
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 ψ holds now or at some point in the future using the formula ♦ψ (ψ holds eventually). However, some applications require not just that a formula ψ will
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).
B
Clare Dixon [email protected] Ullrich Hustadt [email protected] Ana Ozaki [email protected]
1
Department of Computer Science, University of Liverpool, Liverpool, UK
2
Faculty of Computer Science, Free University of Bozen-Bolzano, Bolzano, Italy
123
U. Hustadt et al.
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 cyberphysical 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]. 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, ♦[3,7] p means that p should hold in a state that occurs in the interval [3, 7] of time, wh
Data Loading...
