Zeno, Hercules, and the Hydra: Safety metric temporal logic is Ackermann-complete
<p>Metric temporal logic (MTL) is one of the most prominent specification formalisms for real-time systems. Over infinite timed words, full MTL is undecidable, but satisfiability for a syntactially defined safety fragment, called safety MTL, was proved decidable several years ago. Satisfiabili...
Main Authors: | , , |
---|---|
Format: | Journal article |
Published: |
Association for Computing Machinery
2016
|