Theorem Proving for Pointwise Metric Temporal Logic Overthe Naturals via Translations



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.

[img] Text
main.pdf - Accepted Version

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: 28 May 2022 04:11
DOI: 10.1007/s10817-020-09541-4
Related URLs:
URI: https://livrepository.liverpool.ac.uk/id/eprint/3070608