Abstract
This paper investigates the properties of Metric Temporal Logic (MTL) over models in which time is dense but phenomena are constrained to have bounded variability. Contrary to the case of generic dense-time behaviors, MTL is proved to be fully decidable over models with bounded variability, if the variability bound is given. In these decidable cases, MTL complexity is shown to match that of simpler decidable logics such as MITL. On the contrary, MTL is undecidable if all behaviors with variability bounded by some generic constant are considered, but with an undecidability degree that is lower than in the case of generic behaviors.
Work partially supported by the MIUR FIRB Projects: ArtDeco and “Applicazioni della Teoria degli Automi all’Analisi, Compilazione e Verifica di Software Critico e in Tempo Reale”.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. Journal of the ACM 43(1), 116–146 (1996)
Alur, R., Henzinger, T.A.: Real-time logics: Complexity and expressiveness. Information and Computation 104(1), 35–77 (1993)
Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. Journal of the ACM 49(2), 172–206 (2002)
Bouyer, P., Markey, N., Ouaknine, J., Worrell, J.: The cost of punctuality. In: Proceedings of LICS 2007 (2007)
D’Souza, D., Prabhakar, P.: On the expressiveness of MTL in the pointwise and continuous semantics. Formal Methods Letters 9(1), 1–4 (2007)
M. Fränzle. Decidability of duration calculi on restricted model classes. Technical Report Kiel MF 21/1, Christian-Albrechts Universität Kiel (1996)
Furia, C.A., Pradella, M., Rossi, M.: Automated verification of dense-time MTL specifications via discrete-time approximation. In: Cuellar, J., Maibaum, T.S.E. (eds.) FM 2008. LNCS, vol. 5014, pp. 132–147. Springer, Heidelberg (2008)
Furia, C.A., Rossi, M.: Integrating discrete- and continuous-time metric temporal logics through sampling. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 215–229. Springer, Heidelberg (2006)
Furia, C.A., Rossi, M.: MTL with bounded variability: Decidability and complexity. Technical report, DEI, Politecnico di Milano (May 2008)
Gabbay, D.M., Hodkinson, I., Reynolds, M.: Temporal Logic, vol. 1. Oxford University Press, Oxford (1994)
Hirshfeld, Y., Rabinovich, A.M.: Logics for real time: Decidability and complexity. Fundamenta Informaticae 62(1), 1–28 (2004)
Lutz, C., Walther, D., Wolter, F.: Quantitative temporal logics over the reals: PSPACE and below. Information and Computation 205(1), 99–123 (2007)
Maler, O., Nickovic, D., Pnueli, A.: From MITL to timed automata. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 274–289. Springer, Heidelberg (2006)
Ouaknine, J., Worrell, J.: On the decidability and complexity of metric temporal logic over finite words. Logical Methods in Computer Science 3(1) (2007)
Rabinovich, A.: Temporal logics with incommensurable distances are undecidable. Information and Computation 205(5), 707–715 (2007)
Rabinovich, A.M.: Complexity of metric temporal logic with counting. In: Proceedings of FORMATS 2008. LNCS. Springer, Heidelberg (2008)
Wilke, T.: Specifying timed state sequences in powerful decidable logics and timed automata. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994. LNCS, vol. 863, pp. 694–715. Springer, Heidelberg (1994)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Furia, C.A., Rossi, M. (2008). MTL with Bounded Variability: Decidability and Complexity. In: Cassez, F., Jard, C. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2008. Lecture Notes in Computer Science, vol 5215. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85778-5_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-85778-5_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85777-8
Online ISBN: 978-3-540-85778-5
eBook Packages: Computer ScienceComputer Science (R0)