Theorem Proving for Metric Temporal Logic over the Naturals

From International Center for Computational Logic

Toggle side column

Theorem Proving for Metric Temporal Logic over the Naturals

Ullrich HustadtUllrich Hustadt,  Ana OzakiAna Ozaki,  Clare DixonClare Dixon
Ullrich Hustadt, Ana Ozaki, Clare Dixon
Theorem Proving for Metric Temporal Logic over the Naturals
Conference on Automated Deduction, to appear. Springer
  • KurzfassungAbstract
    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 (1) a strict monotonic function and by (2) a non-strict monotonic function (which allows multiple states to be mapped to the same time point). 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.
  • Projekt:Project: Cfaed
  • Forschungsgruppe:Research Group: Wissensbasierte SystemeKnowledge-Based Systems
The final publication is available at Springer.
@inproceedings{HOD2017,
  author    = {Ullrich Hustadt and Ana Ozaki and Clare Dixon},
  title     = {Theorem Proving for Metric Temporal Logic over the Naturals},
  booktitle = {Conference on Automated Deduction},
  publisher = {Springer},
  year      = {2017},
  month     = {August}
}

Web page with our implementation: http://cgi.csc.liv.ac.uk/~ullrich/MTL/