Abstract
We study an extension of the logic MITL with parametric constants. In particular, we define a logic, denoted PMITL (parametric MITL), where the subscripts of the temporal operators are intervals with possibly a parametric endpoint. We consider typical decision problems, such as emptiness and universality of the set of parameter valuations under which a given parametric formula is satisfiable, or whether a given parametric timed automaton is a model of a given parametric formula. We show that when each parameter is used with a fixed polarity and only parameter valuations which evaluate parametric intervals to non-singular time intervals are taken into consideration, then the considered problems are decidable and Expspace-complete. We also investigate the computational complexity of these problems for natural fragments of PMITL, and show that in meaningful fragments of the logic they are Pspace-complete. Finally, we discuss other natural parameterizations of MITL, which indeed lead to undecidability.
This work was partially funded by the MIUR grants FARB 2008-2009 Università degli Studi di Salerno (Italy).
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., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Inf. Comput. 104(1), 2–34 (1993)
Alur, R., Etessami, K., La Torre, S., Peled, D.: Parametric temporal logic for “model measuring”. ACM Trans. Comput. Log. 2(3), 388–407 (2001)
Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996)
Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: STOC, pp. 592–601 (1993)
Bozzelli, L., La Torre, S.: Decision problems for lower/upper bound parametric timed automata. Formal Methods in System Design 35(2), 121–151 (2009)
Bruyère, V., Dall’Olio, E., Raskin, J.F.: Durations and parametric model-checking in timed automata. ACM Trans. Comput. Log. 9(2) (2008)
Bruyère, V., Raskin, J.F.: Real-time model-checking: Parameters everywhere. Logical Methods in Computer Science 3(1) (2007)
Campos, S.V.A., Clarke, E.M., Grumberg, O.: Selective quantitative analysis and interval model checking: Verifying different facets of a system. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 257–268. Springer, Heidelberg (1996)
Chevallier, R., Encrenaz-Tiphène, E., Fribourg, L., Xu, W.: Timed verification of the generic architecture of a memory circuit using parametric timed automata. Formal Methods in System Design 34(1), 59–81 (2009)
Courcoubetis, C., Yannakakis, M.: Minimum and maximum delay problems in real-time systems. Formal Methods in System Design 1(4), 385–415 (1992)
Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science. Formal Models and Sematics (B), vol. B, pp. 995–1072 (1990)
Emerson, E.A., Trefler, R.J.: Parametric quantitative temporal reasoning. LICS, 336–343 (1999)
Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear parametric model checking of timed automata. J. Log. Algebr. Program. 52-53, 183–220 (2002)
Kupferman, O., Piterman, N., Vardi, M.Y.: From liveness to promptness. Formal Methods in System Design 34(2), 83–103 (2009)
Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57. IEEE, Los Alamitos (1977)
Wang, F.: Parametric timing analysis for real-time systems. Inf. Comput. 130(2), 131–150 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Di Giampaolo, B., La Torre, S., Napoli, M. (2010). Parametric Metric Interval Temporal Logic. In: Dediu, AH., Fernau, H., Martín-Vide, C. (eds) Language and Automata Theory and Applications. LATA 2010. Lecture Notes in Computer Science, vol 6031. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13089-2_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-13089-2_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-13088-5
Online ISBN: 978-3-642-13089-2
eBook Packages: Computer ScienceComputer Science (R0)