The Library
Zeno, Hercules, and the Hydra : safety metric temporal logic is ACKERMANN-complete
Tools
Lazic, Ranko, Ouaknine, Joel and Worrell, James (2016) Zeno, Hercules, and the Hydra : safety metric temporal logic is ACKERMANN-complete. ACM Transactions on Computational Logic, 17 (3). 16. doi:10.1145/2874774 ISSN 1557-945X .
|
PDF
WRAP_zeno_j.pdf - Accepted Version - Requires a PDF viewer. Download (585Kb) | Preview |
Official URL: http://dx.doi.org/10.1145/2874774
Abstract
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 nonelementary lower bound. 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 nonprimitive recursive problems). This is surprising since decidability was originally established using Higman's Lemma, suggesting a much higher nonmultiply recursive complexity.
Item Type: | Journal Article | ||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||||||||
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||||||||
Library of Congress Subject Headings (LCSH): | Algorithms, Computer programs -- Verification, Software engineering | ||||||||||
Journal or Publication Title: | ACM Transactions on Computational Logic | ||||||||||
Publisher: | A C M Special Interest Group | ||||||||||
ISSN: | 1557-945X | ||||||||||
Official Date: | February 2016 | ||||||||||
Dates: |
|
||||||||||
Volume: | 17 | ||||||||||
Number: | 3 | ||||||||||
Article Number: | 16 | ||||||||||
DOI: | 10.1145/2874774 | ||||||||||
Status: | Peer Reviewed | ||||||||||
Publication Status: | Published | ||||||||||
Access rights to Published version: | Restricted or Subscription Access | ||||||||||
Date of first compliant deposit: | 3 March 2016 | ||||||||||
Date of first compliant Open Access: | 4 March 2016 |
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |
Downloads
Downloads per month over past year