Hustadt, Ullrich ORCID: 0000-0002-0455-0267, Ozaki, Ana and Dixon, Clare ORCID: 0000-0002-4610-9533
(2020)
Theorem Proving for Pointwise Metric Temporal Logic Overthe Naturals via Translations.
Journal of Automated Reasoning, 64 (8).
pp. 1553-1610.
Text
main.pdf - Author Accepted Manuscript Download (652kB) | Preview |
Abstract
We study translations from metric temporal logic (MTL) over the natural numbers to lineartemporal logic (LTL). In particular, we present two approaches for translating from MTLto LTL which preserve theExpSpacecomplexity of the satisfiability problem for MTL.In each of these approaches we consider the case where the mapping between states andtime points is given by (i) a strict monotonic function and by (ii) a non-strict monotonicfunction (which allows multiple states to be mapped to the same time point). We use thislogic to model examples from robotics, traffic management, and scheduling, discussing theeffects of different modelling choices. Our translations allow us to utilise LTL solvers tosolve satisfiability and we empirically compare the translations, showing in which cases oneperforms better than the other. We also define a branching-time version of the logic andprovide translations into computation tree logic.
Item Type: | Article |
---|---|
Uncontrolled Keywords: | Metric temporal logic, Theorem proving, Modelling |
Depositing User: | Symplectic Admin |
Date Deposited: | 14 Jan 2020 11:43 |
Last Modified: | 19 Jan 2023 00:09 |
DOI: | 10.1007/s10817-020-09541-4 |
Related URLs: | |
URI: | https://livrepository.liverpool.ac.uk/id/eprint/3070608 |