Some recent results in metric temporal logic. (English) Zbl 1171.68553
Cassez, Franck (ed.) et al., Formal modeling and analysis of timed systems. 6th international conference, FORMATS 2008, Saint Malo, France, September 15–17, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-85777-8/pbk). Lecture Notes in Computer Science 5215, 1-13 (2008).
Summary: Metric Temporal Logic (MTL) is a widely-studied real-time extension of Linear Temporal Logic. In this paper we survey results about the complexity of the satisfiability and model checking problems for fragments of MTL with respect to different semantic models. We show that these fragments have widely differing complexities: from polynomial space to non-primitive recursive and even undecidable. However we show that the most commonly occurring real-time properties, such as invariance and bounded response, can be expressed in fragments of MTL for which model checking, if not satisfiability, can be decided in polynomial or exponential space.
For the entire collection see [Zbl 1149.68007].
For the entire collection see [Zbl 1149.68007].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B44 | Temporal logic |
| 68Q25 | Analysis of algorithms and problem complexity |
References:
| [1] | Alur, R.; Courcoubetis, C.; Dill, D. L., Model-checking for real-time systems, Proceeding of LICS 1990 (1990), Los Alamitos: IEEE Comp. Society Press, Los Alamitos |
| [2] | Alur, R.; Dill, D., A theory of timed automata, Theoretical Computer Science, 126, 183-235 (1994) · Zbl 0803.68071 · doi:10.1016/0304-3975(94)90010-8 |
| [3] | Alur, R.; Feder, T.; Henzinger, T. A., The benefits of relaxing punctuality, Journal of the ACM, 43, 116-146 (1996) · Zbl 0882.68021 · doi:10.1145/227595.227602 |
| [4] | Alur, R.; Henzinger, T. A., Logics and models of real time: A survey, Proceedings of Real Time: Theory in Practice (1992), Heidelberg: Springer, Heidelberg |
| [5] | Alur, R.; Henzinger, T. A., Real-time logics: complexity and expressiveness, Information and Computation, 104, 35-77 (1993) · Zbl 0791.68103 · doi:10.1006/inco.1993.1025 |
| [6] | Alur, R.; Henzinger, T. A., A really temporal logic, Journal of the ACM, 41, 181-204 (1994) · Zbl 0807.68065 · doi:10.1145/174644.174651 |
| [7] | Alur, R.; Madhusudan, P.; Bernardo, M.; Corradini, F., Decision Problems for Timed Automata: A Survey, Formal Methods for the Design of Real-Time Systems (2004), Heidelberg: Springer, Heidelberg · Zbl 1105.68057 |
| [8] | Bouyer, P.; Chevalier, F.; Markey, N.; Ramanujam, R.; Sen, S., On the Expressiveness of TPTL and MTL, FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science (2005), Heidelberg: Springer, Heidelberg · doi:10.1007/11590156_35 |
| [9] | Bouyer, P.; Markey, N.; Ouaknine, J.; Worrell, J., The Cost of Punctuality, Proceedings of LICS 2007 (2007), Los Alamitos: IEEE Computer Society Press, Los Alamitos |
| [10] | Bouyer, P.; Markey, N.; Ouaknine, J.; Worrell, J., On Expressiveness and Complexity in Real-time Model Checking, Proceedings of ICALP 2008 (2008), Heidelberg: Springer, Heidelberg · Zbl 1155.68426 |
| [11] | Bouyer, P., Markey, N., Ouaknine, J., Schnoebelen, P., Worrell, J.: On Termination for Faulty Channel Machines. In: Proceedings of STACS 2008 (2008) · Zbl 1259.68120 |
| [12] | Comon, H.; Cortier, V.; Clote, P. G.; Schwichtenberg, H., Flatness is not a Weakness, Computer Science Logic (2000), Heidelberg: Springer, Heidelberg · Zbl 0973.68142 · doi:10.1007/3-540-44622-2_17 |
| [13] | Demri, S.; Lazić, R.; Nowak, D., On the Freeze Quantifier in Constraint LTL: Decidability and Complexity, Information and Computation, 205, 1, 2-24 (2007) · Zbl 1116.03014 · doi:10.1016/j.ic.2006.08.003 |
| [14] | Henzinger, T. A., Sooner is safer than later, Processing Letters, 43, 135-141 (1992) · Zbl 0753.68041 · doi:10.1016/0020-0190(92)90005-G |
| [15] | Henzinger, T. A.; Sangiorgi, D.; de Simone, R., It’s about time: Real-time logics reviewed, CONCUR ’98 Concurrency Theory (1998), Heidelberg: Springer, Heidelberg · Zbl 0928.03019 · doi:10.1007/BFb0055640 |
| [16] | Henzinger, T. A.; Manna, Z.; Pnueli, A.; Kuich, W., What good are digital clocks?, Automata, Languages and Programming (1992), Heidelberg: Springer, Heidelberg · Zbl 1425.68255 |
| [17] | Hirshfeld, Y.; Rabinovich, A. M., Logics for Real Time: Decidability and Complexity, Fundam. Inform., 62, 1, 1-28 (2004) · Zbl 1127.03012 |
| [18] | Henzinger, T. A.; Raskin, J.-F.; Shobbens, P.-Y.; Larsen, K. G.; Skyum, S.; Winskel, G., The regular real-time languages, Automata, Languages and Programming (1998), Heidelberg: Springer, Heidelberg |
| [19] | Higman, G., Ordering by divisibility in abstract algebras, Proc. of the London Mathematical Society, 2, 236-366 (1952) |
| [20] | Kamp, J.A.W.: Tense logic and the theory of linear order. Ph.D. Thesis, UCLA (1968) |
| [21] | Koymans, R., Specifying real-time properties with metric temporal logic, Real-time Systems, 2, 4, 255-299 (1990) · doi:10.1007/BF01995674 |
| [22] | Lasota, S.; Walukiewicz, I.; Sassone, V., Alternating timed automata, Foundations of Software Science and Computational Structures (2005), Heidelberg: Springer, Heidelberg · Zbl 1119.68109 |
| [23] | Ostroff, J.: Temporal logic of real-time systems. Research Studies Press, Taunton |
| [24] | Ouaknine, J.; Worrell, J., On the language inclusion problem for timed automata: Closing a decidability gap, Proceedings of LICS 2004 (2004), Los Alamitos: IEEE Computer Society Press, Los Alamitos |
| [25] | Ouaknine, J.; Worrell, J.; Aceto, L.; Ingólfsdóttir, A., Metric temporal logic and faulty Turing machines, Foundations of Software Science and Computation Structures (2006), Heidelberg: Springer, Heidelberg · doi:10.1007/11690634_15 |
| [26] | Ouaknine, J.; Worrell, J.; Hermanns, H.; Palsberg, J., Safety metric temporal logic is fully decidable, Tools and Algorithms for the Construction and Analysis of Systems (2006), Heidelberg: Springer, Heidelberg · Zbl 1180.03020 · doi:10.1007/11691372_27 |
| [27] | Ouaknine, J., Worrell, J.: On the Decidability and Complexity of Metric Temporal Logic over Finite Words. Logicical Methods in Computer Science 3(1) (2007) · Zbl 1128.03008 |
| [28] | Pnueli, A., The temporal logic of programs, Proceedings of FOCS 1977 (1977), Los Alamitos: IEEE Computer Society Press, Los Alamitos |
| [29] | Raskin, J.-F.; Schobbens, P.-Y.; Maler, O., State-clock logic: a decidable real-time logic, Hybrid and Real-Time Systems (1997), Heidelberg: Springer, Heidelberg · doi:10.1007/BFb0014711 |
| [30] | Schnoebelen, P., Verifying lossy channel systems has nonprimitive recursive complexity, Information Processing Letters, 83, 5, 251-261 (2002) · Zbl 1043.68016 · doi:10.1016/S0020-0190(01)00337-4 |
| [31] | Wilke, T.; Langmaack, H.; de Roever, W.-P.; Vytopil, J., Specifying timed state sequences in powerful decidable logics and timed automata, Formal Techniques in Real-Time and Fault-Tolerant Systems (1994), Heidelberg: Springer, Heidelberg |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
