 |
 |
Joel Ouaknine ; James Worrell - On the decidability and complexity of Metric Temporal Logic over finite words
lmcs:2230 - Logical Methods in Computer Science, February 28, 2007, Volume 3, Issue 1 - https://doi.org/10.2168/LMCS-3(1:8)2007On the decidability and complexity of Metric Temporal Logic over finite
wordsArticle
Authors: Joel Ouaknine ; James Worrell 
NULL##0000-0001-8151-2443Joel Ouaknine;James Worrell
Metric Temporal Logic (MTL) is a prominent specification formalism for real-time systems. In this paper, we show that the satisfiability problem for MTL over finite timed words is decidable, with non-primitive recursive complexity. We also consider the model-checking problem for MTL: whether all words accepted by a given Alur-Dill timed automaton satisfy a given MTL formula. We show that this problem is decidable over finite words. Over infinite words, we show that model checking the safety fragment of MTL--which includes invariance and time-bounded response properties--is also decidable. These results are quite surprising in that they contradict various claims to the contrary that have appeared in the literature.
Source: arXiv.org:cs/0702120
Volume: Volume 3, Issue 1
Published on: February 28, 2007
Submitted on: May 15, 2006
Keywords: Computer Science - Logic in Computer Science,Computer Science - Computational Complexity,F.4.1
Classifications
Mathematics Subject Classification 20201
- 03B25 - Decidability of theories and sets of sentences
- 03B44 - Temporal logic
- 03D05 - Automata and formal grammars in connection with logical questions
- 03D15 - Complexity of computation (including implicit computational complexity)
- 68Q60 - Specification and verification (program logics, model checking, etc.)
Sources:
- [1] zbMATH Open.
Bibliographic References
66 Documents citing this article
- Shaokai Lin;Yatin A. Manerkar;Marten Lohstroh;Elizabeth Polgreen;Sheng-Jung Yu;et al., 2023, Towards Building Verifiable CPS using Lingua Franca, ACM Transactions on Embedded Computing Systems, 22, 5s, pp. 1-24, 10.1145/3609134, https://doi.org/10.1145/3609134.
- Claudio Di Ciccio;Marco Montali, Lecture notes in business information processing, Declarative Process Specifications: Reasoning, Discovery, Monitoring, pp. 108-152, 2022, 10.1007/978-3-031-08848-3_4, https://doi.org/10.1007/978-3-031-08848-3_4.
- Pedro Cabalar;Martín Diéguez;Torsten Schaub;Anna Schuhmann, Lecture notes in computer science, Metric Temporal Answer Set Programming over Timed Traces, pp. 117-130, 2022, 10.1007/978-3-031-15707-3_10.
- Bartosz Bednarczyk;Jakub Michaliszyn, Lecture notes in computer science, “Most of” leads to undecidability: Failure of adding frequencies to LTL, pp. 82-101, 2021, 10.1007/978-3-030-71995-1_5, https://doi.org/10.1007/978-3-030-71995-1_5.
- Christopher Hampson, 2021, On the termination and structural termination problems for counter machines with incrementing errors, Journal of Computer and System Sciences, 120, pp. 149-161, 10.1016/j.jcss.2021.03.007.
- Kohei FUJITA;Toshimitsu USHIO, 2021, Optimal Control of Timed Petri Nets Under Temporal Logic Constraints with Generalized Mutual Exclusion, IEICE Transactions on Fundamentals of Electronics Communications and Computer Sciences, E105.A, 5, pp. 808-815, 10.1587/transfun.2021map0003.
- Laura Bozzelli;Angelo Montanari;Adriano Peron, 2021, Complexity issues for timeline-based planning over dense time under future and minimal semantics, ArTS Archivio della ricerca di Trieste (University of Trieste https://www.units.it/), 901, pp. 87-113, 10.1016/j.tcs.2021.12.004, https://hdl.handle.net/11368/3032319.
- Ana de Almeida Borges;Juan José Conejero Rodríguez;David Fernández-Duque;Mireia González Bedmar;Joost J. Joosten, 2020, To drive or not to drive: A logical and computational analysis of European transport regulations, Information and Computation, 280, pp. 104636, 10.1016/j.ic.2020.104636.
- Hsi-Ming Ho;Ruoyu Zhou;Timothy M. Jones, 2020, Timed hyperproperties, Sussex Research Online (University of Sussex), 280, pp. 104639, 10.1016/j.ic.2020.104639, http://sro.sussex.ac.uk/id/eprint/94743/1/IandC_accepted_manuscript.pdf.
- Laura Bozzelli;Alberto Molinari;Angelo Montanari;Adriano Peron;Gerhard Woeginger, 2020, Timeline-based planning over dense temporal domains, Theoretical Computer Science, 813, pp. 305-326, 10.1016/j.tcs.2019.12.030, https://doi.org/10.1016/j.tcs.2019.12.030.
- Laura Bozzelli;Aniello Murano;Adriano Peron, 2020, Context-free timed formalisms: Robust automata and linear temporal logics, ArTS Archivio della ricerca di Trieste (University of Trieste https://www.units.it/), 283, pp. 104673, 10.1016/j.ic.2020.104673, https://hdl.handle.net/11368/3032321.
- Lorenzo Clemente;Slawomir Lasota;Radoslaw Piórkowski, International Conference on Concurrency Theory, Determinisability of One-Clock Timed Automata, pp. 17-, 2020, 10.4230/lipics.concur.2020.42.
- Christopher Hampson, Research Portal (King's College London), On the Termination Problem for Counter Machines with Incrementing Errors, pp. 137-148, 2019, 10.1007/978-3-030-30806-3_11, https://kclpure.kcl.ac.uk/portal/en/publications/on-the-termination-problem-for-counter-machines-with-incrementing-errors(87ceb73d-325c-4580-949f-484f38f45676).html.
- Hsi-Ming Ho, SHURA (Sheffield Hallam University Research Archive) (Sheffield Hallam University), Revisiting timed logics with automata modalities, 90, pp. 67-76, 2019, Montreal Quebec Canada, 10.1145/3302504.3311818, http://shura.shu.ac.uk/25238/1/Ho%20Revisiting%20Timed%20Logics%20with%20Automata%20Modalities.pdf.
- Shiguang Feng;Claudia Carapelle;Oliver Fernández Gil;Karin Quaas, 2019, MTL and TPTL for One-Counter Machines, ACM Transactions on Computational Logic, 21, 2, pp. 1-34, 10.1145/3372789.
- Dejanira Araiza-Illan;Kerstin Eder, Springer eBooks, Safe and Trustworthy Human-Robot Interaction, pp. 2397-2419, 2018, 10.1007/978-94-007-6046-2_131.
- Einar Broch Johnsen;Martin Steffen;Johanna Beate Stumpf;Lars Tveito, Lecture notes in computer science, Checking Modal Contracts for Virtually Timed Ambients, pp. 252-272, 2018, 10.1007/978-3-030-02508-3_14.
- Laura Bozzelli;Alberto Molinari;Angelo Montanari;Adriano Peron, 2018, Complexity of Timeline-Based Planning over Dense Temporal Domains: Exploring the Middle Ground, arXiv (Cornell University), 277, pp. 191-205, 10.4204/eptcs.277.14.
- Laura Bozzelli;Aniello Murano;Adriano Peron, 2018, Timed Context-Free Temporal Logics, arXiv (Cornell University), 277, pp. 235-249, 10.4204/eptcs.277.17.
- Patricia Bouyer;Uli Fahrenberg;Kim Guldstrand Larsen;Nicolas Markey;Joël Ouaknine;et al., Springer eBooks, Model Checking Real-Time Systems, pp. 1001-1046, 2018, 10.1007/978-3-319-10575-8_29.
- Dejanira Araiza-Illan;Kerstin Eder, Springer eBooks, Safe and Trustworthy Human Robot Interaction, pp. 1-23, 2017, 10.1007/978-94-007-7194-9_131-1.
- Thomas Brihaye;Gilles Geeraerts;Hsi-Ming Ho;Benjamin Monmege, MightyL: A Compositional Translation from MITL to Timed Automata, pp. 421-440, 2017, 10.1007/978-3-319-63387-9_21, https://hal.archives-ouvertes.fr/hal-01525524.
- Étienne André, 2017, What’s decidable about parametric timed automata?, arXiv (Cornell University), 21, 2, pp. 203-219, 10.1007/s10009-017-0467-0, https://arxiv.org/abs/1907.01721.
- Angelo Montanari;Marco Pazzaglia;Pietro Sala, 2016, Metric propositional neighborhood logic with an equivalence relation, Institutional Research Information System (University of Udine), 53, 6-8, pp. 621-648, 10.1007/s00236-016-0256-3, http://hdl.handle.net/11390/1110493.
- Carlo A. Furia;Paola Spoletini, 2016, Bounded variability of metric temporal logic, Annals of Mathematics and Artificial Intelligence, 80, 3-4, pp. 283-316, 10.1007/s10472-016-9532-8, https://doi.org/10.1007/s10472-016-9532-8.
- Masaki Waga;Takumi Akazaki;Ichiro Hasuo, arXiv (Cornell University), A Boyer-Moore Type Algorithm for Timed Pattern Matching, pp. 121-139, 2016, 10.1007/978-3-319-44878-7_8, https://arxiv.org/abs/1606.07207.
- Ranko Lazić;Joël Ouaknine;James Worrell, 2016, Zeno, Hercules, and the Hydra, Warwick Research Archive Portal (University of Warwick), 17, 3, pp. 1-27, 10.1145/2874774, http://wrap.warwick.ac.uk/76266/7/WRAP_zeno_j.pdf.
- Silvano Dal Zilio;Bernard Berthomieu, Automating the Verification of Realtime Observers Using Probes and the Modal mu-calculus, pp. 90-104, 2016, 10.1007/978-3-319-28678-5_7, https://hal.archives-ouvertes.fr/hal-01202799.
- Sylvain Schmitz, 2016, Complexity Hierarchies beyond Elementary, arXiv (Cornell University), 8, 1, pp. 1-36, 10.1145/2858784, http://arxiv.org/abs/1312.5686.
- Angelo Montanari;Marco Pazzaglia;Pietro Sala, 2015, Adding one or more equivalence relations to the interval temporal logic ABB¯, Theoretical Computer Science, 629, pp. 116-134, 10.1016/j.tcs.2015.11.030, https://doi.org/10.1016/j.tcs.2015.11.030.
- Giorgio Bacci;Giovanni Bacci;Kim Guldstrand Larsen;Radu Mardare, Lecture notes in computer science, On the Total Variation Distance of Semi-Markov Chains, pp. 185-199, 2015, 10.1007/978-3-662-46678-0_12, https://doi.org/10.1007/978-3-662-46678-0_12.
- Haiying Sun;Jing Liu;Xiaohong Chen;Dehui Du, 2015 Asia-Pacific Software Engineering Conference (APSEC), Specifying Cyber Physical System Safety Properties with Metric Temporal Spatial Logic, 62, pp. 254-260, 2015, New Delhi, 10.1109/apsec.2015.58.
- Shiguang Feng;Markus Lohrey;Karin Quaas, arXiv (Cornell University), Path Checking for MTL and TPTL over Data Words, pp. 326-339, 2015, 10.1007/978-3-319-21500-6_26, http://arxiv.org/abs/1412.3644.
- Angelo Montanari;Marco Pazzaglia;Pietro Sala, Institutional Research Information System (University of Udine), Metric Propositional Neighborhood Logic with an Equivalence Relation, 2014, Verona, Italy, 10.1109/time.2014.26, https://hdl.handle.net/11390/1110493.
- Claudia Carapelle;Shiguang Feng;Oliver Fernández Gil;Karin Quaas, Lecture notes in computer science, Satisfiability for MTL and TPTL over Non-monotonic Data Words, pp. 248-259, 2014, 10.1007/978-3-319-04921-2_20.
- Ingmar Meinecke;Karin Quaas, 2014, Parameterized model checking of weighted networks, Theoretical Computer Science, 534, pp. 69-85, 10.1016/j.tcs.2014.02.037, https://doi.org/10.1016/j.tcs.2014.02.037.
- Karin Quaas, 2014, MTL-Model Checking of One-Clock Parametric Timed Automata is Undecidable, arXiv (Cornell University), 145, pp. 5-17, 10.4204/eptcs.145.3.
- Nouha Abid;Silvano Dal Zilio;Didier Le Botlan, 2014, A formal framework to specify and verify real-time properties on critical systems, 5, 1/2, pp. 4, 10.1504/ijccbs.2014.059593, https://hal.science/hal-00941248.
- Thomas Brihaye;Morgane Estiévenart;Gilles Geeraerts, arXiv (Cornell University), On MITL and Alternating Timed Automata over Infinite Words, pp. 69-84, 2014, 10.1007/978-3-319-10512-3_6, https://arxiv.org/abs/1406.4395.
- Angelo Montanari;Pietro Sala, 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, Adding an Equivalence Relation to the Interval Logic ABB: Complexity and Expressiveness, pp. 193-202, 2013, New Orleans, LA, USA, 10.1109/lics.2013.25.
- Karin Quaas, Lecture notes in computer science, Model Checking Metric Temporal Logic over Automata with One Counter, pp. 468-479, 2013, 10.1007/978-3-642-37064-9_41.
- Md Tawhid Bin Waez;Juergen Dingel;Karen Rudie, 2013, A survey of timed automata for the development of real-time systems, Computer Science Review, 9, pp. 1-26, 10.1016/j.cosrev.2013.05.001.
- Ranko Lazić;Joël Ouaknine;James Worrell, Lecture notes in computer science, Zeno, Hercules and the Hydra: Downward Rational Termination Is Ackermannian, pp. 643-654, 2013, 10.1007/978-3-642-40313-2_57.
- Savas Konur, 2013, Specifying safety-critical systems with a decidable duration logic, Science of Computer Programming, 80, pp. 264-287, 10.1016/j.scico.2013.07.012, https://doi.org/10.1016/j.scico.2013.07.012.
- Sylvain Schmitz;Philippe Schnoebelen, arXiv (Cornell University), The Power of Well-Structured Systems, pp. 5-24, 2013, 10.1007/978-3-642-40184-8_2, https://arxiv.org/abs/1402.2908.
- Thomas Brihaye;Morgane Estiévenart;Gilles Geeraerts, arXiv (Cornell University), On MITL and Alternating Timed Automata, pp. 47-61, 2013, 10.1007/978-3-642-40229-6_4, http://arxiv.org/abs/1304.2814.
- Carlo A. Furia;Dino Mandrioli;Angelo Morzenti;Matteo Rossi, Monographs in theoretical computer science, Logic-Based Formalisms, pp. 249-323, 2012, 10.1007/978-3-642-32332-4_9.
- I. Kitouni;H. Hachichi;S. D. Eddine, 2012 International Conference on Information Technology and e-Services, A simple approach for reducing timed automata, pp. 1-6, 2012, Sousse, 10.1109/icites.2012.6216600.
- Ilham Kitouni, 2012, Reducing Timed Automata: A New Approach, Zenodo (CERN European Organization for Nuclear Research), 10.2139/ssrn.3896125, https://zenodo.org/record/2549855.
- Ilham Kitouni;Hiba Hachichi;Kenza Bouaroudj, 2012, Reducing Timed Automata: A New Approach, Zenodo (CERN European Organization for Nuclear Research), 10.5281/zenodo.2613142, https://zenodo.org/record/2613142.
- Nouha Abid;Silvano Dal Zilio;Didier Le Botlan, arXiv (Cornell University), Real-Time Specification Patterns and Tools, pp. 1-15, 2012, 10.1007/978-3-642-32469-7_1, http://arxiv.org/abs/1301.7534.
- Nathalie Bertrand;Patricia Bouyer;Thomas Brihaye;Amélie Stainer, arXiv (Cornell University), Emptiness and Universality Problems in Timed Automata with Positive Frequency, pp. 246-257, 2011, 10.1007/978-3-642-22012-8_19, https://arxiv.org/abs/1309.2842.
- Taolue Chen;Marco Diciolla;Marta Kwiatkowska;Alexandru Mereacre, CiteSeer X (The Pennsylvania State University), Time-Bounded Verification of CTMCs against Real-Time Specifications, pp. 26-42, 2011, 10.1007/978-3-642-24310-3_4, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.646.4924.
- Angelo Montanari;Gabriele Puppis;Pietro Sala, Maximal Decidable Fragments of Halpern and Shoham’s Modal Logic of Intervals, pp. 345-356, 2010, 10.1007/978-3-642-14162-1_29, https://hal.archives-ouvertes.fr/hal-00717788.
- Joël Ouaknine;James Worrell, Lecture notes in computer science, Towards a Theory of Time-Bounded Verification, pp. 22-37, 2010, 10.1007/978-3-642-14162-1_3.
- Mark Jenkin;Joël Ouaknine;Alexander Rabinovich;James Worrell, CiteSeer X (The Pennsylvania State University), Alternating Timed Automata over Bounded Time, 999, pp. 60-69, 2010, Edinburgh, United Kingdom, 10.1109/lics.2010.45, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.698.7834.
- Paritosh K. Pandya;Simoni S. Shah, Lecture notes in computer science, Unambiguity in Timed Regular Languages: Automata and Logics, pp. 168-182, 2010, 10.1007/978-3-642-15297-9_14.
- Christel Baier;Nathalie Bertrand;Patricia Bouyer;Thomas Brihaye, Lecture notes in computer science, When Are Timed Automata Determinizable?, pp. 43-54, 2009, 10.1007/978-3-642-02930-1_4.
- Joël Ouaknine;Alexander Rabinovich;James Worrell, CiteSeer X (The Pennsylvania State University), Time-Bounded Verification, pp. 496-510, 2009, 10.1007/978-3-642-04081-8_33, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.153.6937.
- Patricia Bouyer, 2009, Model-checking Timed Temporal Logics, Electronic Notes in Theoretical Computer Science, 231, pp. 323-341, 10.1016/j.entcs.2009.02.044, https://doi.org/10.1016/j.entcs.2009.02.044.
- Pawel Parys;Igor Walukiewicz, Weak Alternating Timed Automata, pp. 273-284, 2009, 10.1007/978-3-642-02930-1_23, https://hal.archives-ouvertes.fr/hal-00360122.
- Carlo A. Furia;Matteo Rossi, CiteSeer X (The Pennsylvania State University), MTL with Bounded Variability: Decidability and Complexity, pp. 109-123, 2008, 10.1007/978-3-540-85778-5_9, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.217.647.
- Joël Ouaknine;James Worrell, Lecture notes in computer science, Some Recent Results in Metric Temporal Logic, pp. 1-13, 2008, 10.1007/978-3-540-85778-5_1.
- Patricia Bouyer;Nicolas Markey;Pierre-Alain Reynier, Lecture notes in computer science, Robust Analysis of Timed Automata Via Channel Machines, pp. 157-171, 2008, 10.1007/978-3-540-78499-9_12, https://doi.org/10.1007/978-3-540-78499-9_12.
- Carlo Alberto Furia;Matteo Rossi, CiteSeer X (The Pennsylvania State University), On the Expressiveness of MTL Variants over Dense Time, pp. 163-178, 2007, 10.1007/978-3-540-75454-1_13, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.216.8837.
- Patricia Bouyer;Nicolas Markey;Joel Ouaknine;James Worrell, The Cost of Punctuality, pp. 109-120, 2007, Wroclaw, Poland, 10.1109/lics.2007.49, https://hal.archives-ouvertes.fr/hal-01194604/file/BMOW-lics07.pdf.
Share and export
Consultation statistics
This page has been seen 1803 times.
This article's PDF has been downloaded 458 times.