×

zbMATH — the first resource for mathematics

On the expressiveness and monitoring of metric temporal logic. (English) Zbl 07056237
Summary: It is known that Metric Temporal Logic (\(\mathsf{MTL}\)) is strictly less expressive than the Monadic First-Order Logic of Order and Metric (\(\mathsf{FO}[<, +1]\)) when interpreted over timed words; this remains true even when the time domain is bounded a priori. In this work, we present an extension of \(\mathsf{MTL}\) with the same expressive power as \(\mathsf{FO}[<, +1]\) over bounded timed words (and also, trivially, over time-bounded signals). We then show that expressive completeness also holds in the general (time-unbounded) case if we allow the use of rational constants \(q \in \mathbb{Q}\) in formulas. This extended version of \(\mathsf{MTL}\) therefore yields a definitive real-time analogue of Kamp’s theorem. As an application, we propose a trace-length independent monitoring procedure for our extension of \(\mathsf{MTL}\), the first such procedure in a dense real-time setting.
MSC:
03B70 Logic in computer science
68 Computer science
Software:
CESAR; SPIN
PDF BibTeX XML Cite
Full Text: arXiv
References:
[1] [ABLS05]Oliver Arafat, Andreas Bauer, Martin Leucker, and Christian Schallhart. Runtime verification revisited. Technical Report TUM-I0518, Technische Universität München, 2005.
[2] [AD94]Rajeev Alur and David Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994. · Zbl 0803.68071
[3] [AFH96]Rajeev Alur, Tomás Feder, and Thomas A. Henzinger. The benefits of relaxing punctuality. Journal of the ACM, 43(1):116-146, 1996. · Zbl 0882.68021
[4] [AH90]Rajeev Alur and Thomas A. Henzinger. Real-time logics: Complexity and expressiveness. In Proceedings of LICS 1990, pages 390-401. IEEE Computer Society Press, 1990.
[5] [AH92]Rajeev Alur and Thomas A. Henzinger. Back to the future: towards a theory of timed regular languages. In Proceedings of FOCS 1992, pages 177-186. IEEE Computer Society Press, 1992. · Zbl 0977.68548
[6] [AM04]Rajeev Alur and Parthasarathy Madhusudan. Decision problems for timed automata: A survey. In Formal Methods for the Design of Real-Time Systems, volume 3185 of LNCS, pages 1-24. Springer, 2004. · Zbl 1105.68057
[7] [AS87]Bowen Alpern and Fred B. Schneider. Recognizing safety and liveness. Distributed Computing, 2(3):117-126, 1987. · Zbl 0641.68039
[8] [BBBB09]Christel Baier, Nathalie Bertrand, Patricia Bouyer, and Thomas Brihaye. When are timed automata determinizable? In Proceedings of ICALP 2009, volume 5556 of LNCS, pages 43-54. Springer, 2009. · Zbl 1248.68284
[9] [BCE+14]David A. Basin, Germano Caronni, Sarah Ereth, Matús Harvan, Felix Klaedtke, and Heiko Mantel. Scalable offline monitoring. In Proceedings of RV 2014, volume 8734 of LNCS, pages 31-47. Springer, 2014. · Zbl 1380.68268
[10] [BCM05]Patricia Bouyer, Fabrice Chevalier, and Nicolas Markey. On the expressiveness of TPTL and MTL. In Proceedings of FSTTCS 2005, volume 3821 of LNCS, pages 432-443. Springer, 2005. · Zbl 1140.03303
[11] [BEG14]Thomas Brihaye, Morgane Estiévenart, and Gilles Geeraerts. On MITL and alternating timed automata over infinite words. In Proceedings of FORMATS 2014, volume 8711 of LNCS, pages 69-84. Springer, 2014. · Zbl 1448.68291
[12] [BGHM17] Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, and Benjamin Monmege. MightyL: A compositional translation from MITL to timed automata. In Proceedings of CAV 2017, volume 10426 of LNCS, pages 421-440. Springer, 2017.
[13] [Bir93]Jean-Camille Birget. State-complexity of finite-state devices, state compressibility and incompressibility. Mathematical Systems Theory, 26(3):237-269, 1993. · Zbl 0779.68061
[14] [BKV13]A Bauer, JC Küster, and Gil Vegliach. From propositional to first-order monitoring. In Proceedings of RV 2013, volume 8174 of LNCS, pages 59-75. Springer, 2013.
[15] [BKZ11]David Basin, Felix Klaedtke, and Eugene Zălinescu. Algorithms for monitoring real-time properties. In Proceedings of RV 2011, volume 7186 of LNCS, pages 260-275. Springer, 2011.
[16] [BLS11]Andreas Bauer, Martin Leucker, and Christian Schallhart. Runtime verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology, 20(4):14, 2011. · Zbl 1213.68363
[17] [BMOW07] Patricia Bouyer, Nicolas Markey, Joël Ouaknine, and James Worrell. The cost of punctuality. In Proceedings of LICS 2007, pages 109-120. IEEE Computer Society Press, 2007.
[18] [BN12]Kevin Baldor and Jianwei Niu. Monitoring dense-time, continuous-semantics, metric temporal logic. In Proceedings of RV 2012, volume 7687 of LNCS, pages 245-259. Springer, 2012.
[19] [BO14]Daniel Bundala and Joël Ouaknine. On the complexity of temporal-logic path checking. In Proceedings of ICALP 2014, volume 8573 of LNCS, pages 86-97. Springer, 2014. · Zbl 1410.68219
[20] [CE81]Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proceedings of IBM Workshop on Logic of Programs, volume 131 of LNCS, pages 52-71. Springer-Verlag, 1981.
[21] [Dam94]Mads Dam. Temporal logic, automata, and classical theories - an introduction, 1994.
[22] [DHV07]Deepak D’Souza, Raveendra Holla, and Deepak Vankadaru. On the expressiveness of TPTL in
[23] [DKL10]Christian Dax, Felix Klaedtke, and Martin Lange. On regular temporal logics with past. Acta Informatica, 47(4):251-277, 2010. · Zbl 1214.68211
[24] [DM13]Deepak D’Souza and Raj Mohan Matteplackel. A clock-optimal hierarchical monitoring automaton construction for MITL. Technical Report 2013-1, Department of Computer Science and Automation, Indian Institute of Science, 2013.
[25] [DP06]Deepak D’Souza and Pavithra Prabhakar. On the expressiveness of MTL in the pointwise and continuous semantics. International Journal on Software Tools for Technology Transfer, 9(1):1-4, 2006.
[26] [DT04]Deepak D’Souza and Nicolas Tabareau. On timed automata with input-determined guards. In Proceedings of FORMATS/FTRTFT 2004, volume 3253 of LNCS, pages 68-83. Springer, 2004. · Zbl 1109.68503
[27] [EFHL03]Cindy Eisner, Dana Fisman, John Havlicek, and Yoad Lustig. Reasoning with temporal logic on truncated paths. In Proceedings of CAV 2003, volume 2725 of LNCS, pages 27-39. Springer, 2003. · Zbl 1278.68168
[28] [EL86]E. Allen Emerson and Chin-Laung Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proceedings of LICS 1986, pages 267-278. IEEE Computer Society Press, 1986.
[29] [EW96]Kousha Etessami and Thomas Wilke. An until hierarchy for temporal logic. In Proceedings of LICS 1996, pages 108-117. IEEE Computer Society Press, 1996. · Zbl 1005.03021
[30] [FK09]Bernd Finkbeiner and Lars Kuhtz. Monitor circuits for LTL with bounded and unbounded future. In Proceedings of RV 2009, volume 5779 of LNCS, pages 60-75. Springer, 2009.
[31] [FMDR13] Tim French, John Christopher McCabe-Dansted, and Mark Reynolds. Verifying temporal properties in real models. In Proceedings of LPAR 2013, volume 8312 of LNCS, pages 309-323. Springer, 2013. · Zbl 1406.68052
[32] [GHR94]Dov M. Gabbay, Ian Hodkinson, and Mark Reynolds. Temporal Logics: Mathematical Foundations and Computational Aspects, Volume 1. Oxford University Press, 1994. · Zbl 0921.03023
[33] [GO03]Paul Gastin and Denis Oddoux. LTL with past and two-way very-weak alternating automata. In Proceedings of MFCS 2003, volume 2747 of LNCS, pages 439-448. Springer, 2003. · Zbl 1124.68387
[34] [GPSS80]Dov Gabbay, Amir Pnueli, Sharanon Shelah, and J. Stavi. On the temporal analysis of fairness. In Proceedings of POPL 1980, pages 163-173. ACM Press, 1980.
[35] [HMP92]Thomas A. Henzinger, Zohar Manna, and Amir Pnueli. What good are digital clocks? In Proceedings of ICALP 1992, volume 623 of LNCS, pages 545-558. Springer, 1992.
[36] [Hol97]Gerard J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279-295, 1997.
[37] [HOW13]Paul Hunter, Joël Ouaknine, and James Worrell. Expressive completeness of metric temporal logic. In Proceedings of LICS 2013, pages 349-357. IEEE Computer Society Press, 2013. · Zbl 1366.03184
[38] [HR01]Klaus Havelund and Grigore Roşu. Testing linear temporal logic formulae on finite execution traces. Technical Report RIACS 01.08, Research Institute for Advanced Computer Science, 2001.
[39] [HR04]Yoram Hirshfeld and Alexander Moshe Rabinovich. Logics for real time: Decidability and complexity. Fundamenta Informaticae, 62(1):1-28, 2004. · Zbl 1127.03012
[40] [HR06]Yoram Hirshfeld and Alexander Moshe Rabinovich. An expressive temporal logic for real time. In Proceedings of MFCS 2006, volume 4162 of LNCS, pages 492-504. Springer, 2006. · Zbl 1132.03323
[41] [HR07]Yoram Hirshfeld and Alexander Rabinovich. Expressiveness of metric modalities for continuous time. Logical Methods in Computer Science, 3(1), 2007. · Zbl 1128.03007
[42] [HRS98]Thomas A. Henzinger, Jean-François Raskin, and Pierre-Yves Schobbens. The regular real-time languages. In Proceedings of ICALP 1998, volume 1443 of LNCS, pages 580-591. Springer, 1998.
[43] [Hun13]Paul Hunter. When is metric temporal logic expressively complete? In Proceedings of CSL 2013, volume 23 of LIPIcs, pages 380-394. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013. · Zbl 1356.03063
[44] [Kam68]Johan A. Kamp. Tense logic and the theory of linear order. PhD thesis, University of California, Los Angeles, 1968.
[45] [KC05]Sascha Konrad and Betty H. C. Cheng. Real-time specification patterns. In Proceedings of ICSE 2005, pages 372-381. ACM Press, 2005.
[46] [KF09]Lars Kuhtz and Bernd Finkbeiner. LTL path checking is efficiently parallelizable. In Proceedings of ICALP 2009, volume 5556 of LNCS, pages 235-246. Springer, 2009. · Zbl 1248.68252
[47] [KKP11]Dileep Kini, Shankara N. Krishna, and Paritosh Pandya. On construction of safety signal · Zbl 1348.68106
[48] [Koy90]Ron Koymans. Specifying real-time properties with metric temporal logic. Real-Time Systems, 2(4):255-299, 1990.
[49] [KV01]Orna Kupferman and Moshe Y. Vardi. Model checking of safety properties. Formal Methods in System Design, 19(3):291-314, 2001. · Zbl 0995.68061
[50] [LPZ85]Orna Lichtenstein, Amir Pnueli, and Lenore D. Zuck. The glory of the past. In Proceedings of Logics of Programs 1985, volume 193 of LNCS, pages 196-218. Springer, 1985. · Zbl 0586.68028
[51] [LS09]Martin Leucker and Christian Schallhart. A brief account of runtime verification. Journal of Logic and Algebraic Programming, 78(5):293-303, 2009. · Zbl 1192.68433
[52] [LW08]Slawomir Lasota and Igor Walukiewicz. Alternating timed automata. ACM Transactions on Computational Logic, 9(2), 2008. · Zbl 1367.68172
[53] [MN04]Oded Maler and Dejan Nickovic. Monitoring temporal properties of continuous signals. In Proceedings of FORMATS/FTRTFT 2004, volume 3253 of LNCS, pages 152-166. Springer, 2004. · Zbl 1109.68518
[54] [MNP05]Oded Maler, Dejan Nickovic, and Amir Pnueli. Real time temporal logic: Past, present, future. In Proceedings of FORMATS 2005, volume 3829 of LNCS, pages 2-16. Springer, 2005. · Zbl 1175.03009
[55] [MNP06]Oded Maler, Dejan Nickovic, and Amir Pnueli. From MITL to timed automata. In Proceedings of FORMATS 2006, volume 4202 of LNCS, pages 274-289. Springer, 2006. · Zbl 1141.68436
[56] [MP95]Zohar Manna and Amir Pnueli. Temporal verification of reactive systems: safety, volume 2. Springer, 1995. · Zbl 0844.68079
[57] [MS03]Nicolas Markey and Philippe Schnoebelen. Model checking a path (preliminary report). In Proceedings of CONCUR 2003, volume 2761 of LNCS, pages 251-265. Springer, 2003. · Zbl 1274.68197
[58] [NP10]Dejan Nickovic and Nir Piterman. From MTL to deterministic timed automata. In Proceedings of FORMATS 2010, volume 6246 of LNCS, pages 152-167. Springer, 2010. · Zbl 1290.68077
[59] [ORW09]Joël Ouaknine, Alexander Rabinovich, and James Worrell. Time-bounded verification. In Proceedings of CONCUR 2009, volume 5710 of LNCS, pages 496-510. Springer, 2009. · Zbl 1254.68151
[60] [OW06]Joël Ouaknine and James Worrell. On metric temporal logic and faulty turing machines. In Proceedings of FoSSaCS 2006, volume 3921 of LNCS, pages 217-230. Springer, 2006. · Zbl 1180.03021
[61] [OW08]Joël Ouaknine and James Worrell. Some recent results in metric temporal logic. In Proceedings of FORMATS 2008, volume 5215 of LNCS, pages 1-13. Springer, 2008. · Zbl 1171.68553
[62] [OW10]Joël Ouaknine and James Worrell. Towards a theory of time-bounded verification. In Proceedings of ICALP 2010, volume 6199 of LNCS, pages 22-37. Springer, 2010. · Zbl 1288.68170
[63] [PD06]Pavithra Prabhakar and Deepak D’Souza. On the expressiveness of MTL with past operators. In Proceedings of FORMATS 2006, volume 4202 of LNCS, pages 322-336. Springer, 2006. · Zbl 1141.03311
[64] [PS11]Paritosh K. Pandya and Simoni S. Shah. On expressive powers of timed logics: Comparing boundedness, non-punctuality and deterministic freezing. In Proceedings of CONCUR 2011, volume 6901 of LNCS, pages 60-75. Springer, 2011. · Zbl 1343.03011
[65] [QS82]Jean-Pierre Queille and Joseph Sifakis. Specification and verification of concurrent systems in CESAR. In Proceedings of Symposium on Programming 1982, volume 137 of LNCS, pages 337-351. Springer, 1982.
[66] [Rab10]Alexander Rabinovich. Temporal logics over linear time domains are in PSPACE. In Proceedings of RP 2010, volume 6227 of LNCS, pages 29-50. Springer, 2010. · Zbl 1287.68081
[67] [Rey10]Mark Reynolds. The complexity of temporal logic over the reals. Annals of Pure and Applied Logic, 161(8):1063-1096, 2010. · Zbl 1235.03052
[68] [Rey14]Mark Reynolds. Metric temporal logics and deterministic timed automata (long report version). Technical report, University of West Australia, 2014.
[69] [Roş12]Grigore Roşu. On safety properties and their monitoring. Scientific Annals of Computer Science, 22(2):327-365, 2012.
[70] [SC85]A. Prasad Sistla and Edmund M. Clarke. The complexity of propositional linear temporal logics. Journal of the ACM, 32(3):733-749, 1985. · Zbl 0632.68034
[71] [SHL11]Oleg Sokolsky, Klaus Havelund, and Insup Lee. Introduction to the special section on runtime verification. International Journal on Software Tools for Technology Transfer, 14(3):243-247, 2011.
[72] [Sto74]Larry Stockmeyer. The complexity of decision problems in automata theory and logic. PhD thesis, TR 133, M.I.T., Cambridge, 1974.
[73] [Tri02]Stavros Tripakis. Fault diagnosis for timed automata. In Proceedings of FTRTFT 2002, volume 2469 of LNCS, pages 205-224. Springer, 2002. · Zbl 1278.68140
[74] [Var96]Moshe Y. Vardi. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency - Structure versus Automata (8th Banff Higher Order Workshop’95), volume 1043 of LNCS, pages 238-266. Springer, 1996.
[75] [Wil94]Thomas Wilke. Specifying timed state sequences in powerful decidable logics and timed automata. In Proceedings of FTRTFT 1994, volume 863 of LNCS, pages 694-715. Springer, 1994.
[76] [WVS83]Pierre Wolper, Moshe Y. Vardi, and A. Prasad Sistla. Reasoning about infinite computation paths. In Proceedings of FOCS 1983, pages 185-194. IEEE Computer Society Press, 1983.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.