 |
 |
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
Secondary volumes: Selected Papers of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005)
Published on: February 28, 2007
Imported 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
71 Documents citing this article
- Ariel González;Maximiliano Cristiá;Carlos Luna, 2025, Verification of quantitative temporal properties in RealTime-DEVS, SIMULATION, 101, 10, pp. 1057-1076, 10.1177/00375497251340070.
- Giacomo Acitelli;Elisa De Bellis;Fabrizio Maria Maggi;Andrea Marrella;Fabio Patrizi, 2025, Aligning Metric Temporal Constraints and Event Logs via Numeric Planning, Lecture notes in computer science, pp. 33-50, 10.1007/978-3-032-02867-9_4.
- Patricia Bouyer;B. Srivathsan;Vaishnavi Vishwanath, 2025, Model-Checking Real-Time Systems: Revisiting the Alternating Automaton Route, Lecture notes in computer science, pp. 399-421, 10.1007/978-3-031-90897-2_19, https://doi.org/10.1007/978-3-031-90897-2_19.
- Hsi-Ming Ho;Khushraj Madnani, 2024, When Do You Start Counting? Revisiting Counting and Pnueli Modalities in Timed Logics, Electronic Proceedings in Theoretical Computer Science, 408, pp. 73-89, 10.4204/eptcs.408.5, http://dx.doi.org/10.4204/eptcs.408.5.
- Thomas A. Henzinger, 2024, Reminiscences of a Real-Time Researcher, Lecture notes in computer science, pp. 154-164, 10.1007/978-3-031-73751-0_12.
- 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, 2022, Declarative Process Specifications: Reasoning, Discovery, Monitoring, Lecture notes in business information processing, pp. 108-152, 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, 2022, Metric Temporal Answer Set Programming over Timed Traces, Lecture notes in computer science, pp. 117-130, 10.1007/978-3-031-15707-3_10.
- Bartosz Bednarczyk;Jakub Michaliszyn, 2021, “Most of” leads to undecidability: Failure of adding frequencies to LTL, Lecture notes in computer science, pp. 82-101, 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.
- Clemente, Lorenzo;Lasota, Sławomir;Piórkowski, Radosław, 2020, Determinisability of One-Clock Timed Automata, arXiv (Cornell University), 10.4230/lipics.concur.2020.42, http://arxiv.org/abs/2007.09340.
- 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, ArTS Archivio della ricerca di Trieste (University of Trieste https://www.units.it/), 813, pp. 305-326, 10.1016/j.tcs.2019.12.030, https://www.sciencedirect.com/science/article/pii/S0304397519308126.
- 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.
- Christopher Hampson, 2019, On the Termination Problem for Counter Machines with Incrementing Errors, Research Portal (King's College London), pp. 137-148, 10.1007/978-3-030-30806-3_11, https://kclpure.kcl.ac.uk/portal/en/publications/87ceb73d-325c-4580-949f-484f38f45676.
- Hsi-Ming Ho, 2019, Revisiting timed logics with automata modalities, SHURA (Sheffield Hallam University Research Archive) (Sheffield Hallam University), pp. 67-76, 10.1145/3302504.3311818.
- 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, 2018, Safe and Trustworthy Human-Robot Interaction, Humanoid Robotics: A Reference, pp. 2397-2419, 10.1007/978-94-007-6046-2_131.
- Einar Broch Johnsen;Martin Steffen;Johanna Beate Stumpf;Lars Tveito, 2018, Checking Modal Contracts for Virtually Timed Ambients, Lecture notes in computer science, pp. 252-272, 10.1007/978-3-030-02508-3_14.
- Laura Bozzelli;Aniello Murano;Adriano Peron, 2018, Timed Context-Free Temporal Logics, Electronic Proceedings in Theoretical Computer Science, 277, pp. 235-249, 10.4204/eptcs.277.17, https://doi.org/10.4204/eptcs.277.17.
- Laura Bozzelli;Alberto Molinari;Angelo Montanari;Adriano Peron, 2018, Complexity of Timeline-Based Planning over Dense Temporal Domains: Exploring the Middle Ground, Electronic Proceedings in Theoretical Computer Science, 277, pp. 191-205, 10.4204/eptcs.277.14, https://doi.org/10.4204/eptcs.277.14.
- Patricia Bouyer;Uli Fahrenberg;Kim Guldstrand Larsen;Nicolas Markey;Joël Ouaknine;James Worrell, 2018, Model Checking Real-Time Systems, pp. 1001-1046, 10.1007/978-3-319-10575-8_29, https://hal.science/hal-01889280.
- Dejanira Araiza-Illan;Kerstin Eder, 2017, Safe and Trustworthy Human Robot Interaction, Humanoid Robotics: A Reference, pp. 1-23, 10.1007/978-94-007-7194-9_131-1.
- Thomas Brihaye;Gilles Geeraerts;Hsi-Ming Ho;Benjamin Monmege, 2017, MightyL: A Compositional Translation from MITL to Timed Automata, pp. 421-440, 10.1007/978-3-319-63387-9_21, https://hal.science/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, http://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, 2016, A Boyer-Moore Type Algorithm for Timed Pattern Matching, arXiv (Cornell University), pp. 121-139, 10.1007/978-3-319-44878-7_8, http://arxiv.org/abs/1606.07207.
- Ranko Lazić;Joël Ouaknine;James Worrell, 2016, Zeno, Hercules, and the Hydra, Oxford University Research Archive (ORA) (University of Oxford), 17, 3, pp. 1-27, 10.1145/2874774.
- Silvano Dal Zilio;Bernard Berthomieu, 2016, Automating the Verification of Realtime Observers Using Probes and the Modal mu-calculus, arXiv (Cornell University), pp. 90-104, 10.1007/978-3-319-28678-5_7, http://arxiv.org/abs/1509.06507.
- 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.
- Giorgio Bacci;Giovanni Bacci;Kim Guldstrand Larsen;Radu Mardare, 2015, On the Total Variation Distance of Semi-Markov Chains, Lecture notes in computer science, pp. 185-199, 10.1007/978-3-662-46678-0_12.
- Haiying Sun;Jing Liu;Xiaohong Chen;Dehui Du, 2015, Specifying Cyber Physical System Safety Properties with Metric Temporal Spatial Logic, 2015 Asia-Pacific Software Engineering Conference (APSEC), 62, pp. 254-260, 10.1109/apsec.2015.58.
- Shiguang Feng;Markus Lohrey;Karin Quaas, 2015, Path Checking for MTL and TPTL over Data Words, Lecture notes in computer science, pp. 326-339, 10.1007/978-3-319-21500-6_26.
- Angelo Montanari;Marco Pazzaglia;Pietro Sala, 2014, Metric Propositional Neighborhood Logic with an Equivalence Relation, 2014 21st International Symposium on Temporal Representation and Reasoning, 66, pp. 49-58, 10.1109/time.2014.26.
- Claudia Carapelle;Shiguang Feng;Oliver Fernández Gil;Karin Quaas, 2014, Satisfiability for MTL and TPTL over Non-monotonic Data Words, Lecture notes in computer science, pp. 248-259, 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.
- Karin Quaas, 2014, MTL-Model Checking of One-Clock Parametric Timed Automata is Undecidable, Electronic Proceedings in Theoretical Computer Science, 145, pp. 5-17, 10.4204/eptcs.145.3, https://doi.org/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, 2014, On MITL and Alternating Timed Automata over Infinite Words, Lecture notes in computer science, pp. 69-84, 10.1007/978-3-319-10512-3_6.
- Angelo Montanari;Pietro Sala, 2013, Adding an Equivalence Relation to the Interval Logic ABB: Complexity and Expressiveness, Institutional Research Information System (University of Udine), pp. 193-202, 10.1109/lics.2013.25.
- Karin Quaas, 2013, Model Checking Metric Temporal Logic over Automata with One Counter, Lecture notes in computer science, pp. 468-479, 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, 2013, Zeno, Hercules and the Hydra: Downward Rational Termination Is Ackermannian, Lecture notes in computer science, pp. 643-654, 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.
- Sylvain Schmitz;Philippe Schnoebelen, 2013, The Power of Well-Structured Systems, arXiv (Cornell University), pp. 5-24, 10.1007/978-3-642-40184-8_2, http://arxiv.org/abs/1402.2908.
- Thomas Brihaye;Morgane Estiévenart;Gilles Geeraerts, 2013, On MITL and Alternating Timed Automata, Lecture notes in computer science, pp. 47-61, 10.1007/978-3-642-40229-6_4.
- Carlo A. Furia;Dino Mandrioli;Angelo Morzenti;Matteo Rossi, 2012, Logic-Based Formalisms, Monographs in theoretical computer science, pp. 249-323, 10.1007/978-3-642-32332-4_9.
- I. Kitouni;H. Hachichi;S. D. Eddine, 2012, A simple approach for reducing timed automata, 2012 International Conference on Information Technology and e-Services, 2285, pp. 1-6, 10.1109/icites.2012.6216600.
- Ilham Kitouni, 2012, Reducing Timed Automata: A New Approach, SSRN Electronic Journal, 10.2139/ssrn.3896125, https://doi.org/10.2139/ssrn.3896125.
- Kitouni, Ilham;Hachichi, Hiba;Bouaroudj, Kenza, 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, 2012, Real-Time Specification Patterns and Tools, arXiv (Cornell University), pp. 1-15, 10.1007/978-3-642-32469-7_1, http://arxiv.org/abs/1301.7534.
- Nathalie Bertrand;Patricia Bouyer;Thomas Brihaye;Amélie Stainer, 2011, Emptiness and Universality Problems in Timed Automata with Positive Frequency, Lecture notes in computer science, pp. 246-257, 10.1007/978-3-642-22012-8_19.
- Taolue Chen;Marco Diciolla;Marta Kwiatkowska;Alexandru Mereacre, 2011, Time-Bounded Verification of CTMCs against Real-Time Specifications, Lecture notes in computer science, pp. 26-42, 10.1007/978-3-642-24310-3_4.
- Angelo Montanari;Gabriele Puppis;Pietro Sala, 2010, Maximal Decidable Fragments of Halpern and Shoham’s Modal Logic of Intervals, pp. 345-356, 10.1007/978-3-642-14162-1_29, https://hal.science/hal-00717788.
- Joël Ouaknine;James Worrell, 2010, Towards a Theory of Time-Bounded Verification, Lecture notes in computer science, pp. 22-37, 10.1007/978-3-642-14162-1_3.
- Mark Jenkin;Joël Ouaknine;Alexander Rabinovich;James Worrell, 2010, Alternating Timed Automata over Bounded Time, Oxford University Research Archive (ORA) (University of Oxford), 999, pp. 60-69, 10.1109/lics.2010.45.
- Paritosh K. Pandya;Simoni S. Shah, 2010, Unambiguity in Timed Regular Languages: Automata and Logics, Lecture notes in computer science, pp. 168-182, 10.1007/978-3-642-15297-9_14.
- Christel Baier;Nathalie Bertrand;Patricia Bouyer;Thomas Brihaye, 2009, When Are Timed Automata Determinizable?, ORBi UMONS, pp. 43-54, 10.1007/978-3-642-02930-1_4, https://orbi.umons.ac.be/handle/20.500.12907/7010.
- Joël Ouaknine;Alexander Rabinovich;James Worrell, 2009, Time-Bounded Verification, Lecture notes in computer science, pp. 496-510, 10.1007/978-3-642-04081-8_33.
- 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, 2009, Weak Alternating Timed Automata, Lecture notes in computer science, pp. 273-284, 10.1007/978-3-642-02930-1_23.
- Carlo A. Furia;Matteo Rossi, 2008, MTL with Bounded Variability: Decidability and Complexity, Lecture notes in computer science, pp. 109-123, 10.1007/978-3-540-85778-5_9.
- Joël Ouaknine;James Worrell, 2008, Some Recent Results in Metric Temporal Logic, Lecture notes in computer science, pp. 1-13, 10.1007/978-3-540-85778-5_1.
- Patricia Bouyer;Nicolas Markey;Pierre-Alain Reynier, 2008, Robust Analysis of Timed Automata Via Channel Machines, Lecture notes in computer science, pp. 157-171, 10.1007/978-3-540-78499-9_12, https://doi.org/10.1007/978-3-540-78499-9_12.
- Carlo Alberto Furia;Matteo Rossi, 2007, On the Expressiveness of MTL Variants over Dense Time, Lecture notes in computer science, pp. 163-178, 10.1007/978-3-540-75454-1_13.
- Patricia Bouyer;Nicolas Markey;Joel Ouaknine;James Worrell, 2007, The Cost of Punctuality, pp. 109-120, 10.1109/lics.2007.49, https://hal.science/hal-01194604.
Share and export
Consultation statistics
This page has been seen 3649 times.
This article's PDF has been downloaded 765 times.