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
|
| _version_ | 1797081928164179968 |
|---|---|
| author | Lazić, R Ouaknine, J Worrell, J |
| author_facet | Lazić, R Ouaknine, J Worrell, J |
| author_sort | Lazić, R |
| collection | OXFORD |
| description | <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. Satisfiability for safety MTL is also known to be equivalent to a fair termination problem for a class of channel machines with insertion errors. However, hitherto its precise computational complexity has remained elusive, with only a non-elementary lower bound.</p> <br/> <p>Via another equivalent problem, namely termination for a class of rational relations, we show that satisfiability for safety MTL is Ackermann-complete, i.e., among the easiest non-primitive recursive problems. This is surprising since decidability was originally established using Higman’s Lemma, suggesting a much higher non-multiply recursive complexity.</p> |
| first_indexed | 2024-03-07T01:20:58Z |
| format | Journal article |
| id | oxford-uuid:904fd687-897b-425b-93b4-8b2ac277d83e |
| institution | University of Oxford |
| last_indexed | 2024-03-07T01:20:58Z |
| publishDate | 2016 |
| publisher | Association for Computing Machinery |
| record_format | dspace |
| spelling | oxford-uuid:904fd687-897b-425b-93b4-8b2ac277d83e2022-03-26T23:10:49ZZeno, Hercules, and the Hydra: Safety metric temporal logic is Ackermann-completeJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:904fd687-897b-425b-93b4-8b2ac277d83eSymplectic Elements at OxfordAssociation for Computing Machinery2016Lazić, ROuaknine, JWorrell, J<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. Satisfiability for safety MTL is also known to be equivalent to a fair termination problem for a class of channel machines with insertion errors. However, hitherto its precise computational complexity has remained elusive, with only a non-elementary lower bound.</p> <br/> <p>Via another equivalent problem, namely termination for a class of rational relations, we show that satisfiability for safety MTL is Ackermann-complete, i.e., among the easiest non-primitive recursive problems. This is surprising since decidability was originally established using Higman’s Lemma, suggesting a much higher non-multiply recursive complexity.</p> |
| spellingShingle | Lazić, R Ouaknine, J Worrell, J Zeno, Hercules, and the Hydra: Safety metric temporal logic is Ackermann-complete |
| title | Zeno, Hercules, and the Hydra: Safety metric temporal logic is Ackermann-complete |
| title_full | Zeno, Hercules, and the Hydra: Safety metric temporal logic is Ackermann-complete |
| title_fullStr | Zeno, Hercules, and the Hydra: Safety metric temporal logic is Ackermann-complete |
| title_full_unstemmed | Zeno, Hercules, and the Hydra: Safety metric temporal logic is Ackermann-complete |
| title_short | Zeno, Hercules, and the Hydra: Safety metric temporal logic is Ackermann-complete |
| title_sort | zeno hercules and the hydra safety metric temporal logic is ackermann complete |
| work_keys_str_mv | AT lazicr zenoherculesandthehydrasafetymetrictemporallogicisackermanncomplete AT ouakninej zenoherculesandthehydrasafetymetrictemporallogicisackermanncomplete AT worrellj zenoherculesandthehydrasafetymetrictemporallogicisackermanncomplete |