Abstract
In this paper, we study the model-checking and parameter synthesis problems of the logic TCTL over discrete-timed automata where parameters are allowed both in the model and in the property. We show that the model-checking problem of TCTL extended with parameters is undecidable over discrete-timed automata with only one parametric clock. The undecidability result needs equality in the logic. When equality is not allowed, we show that the model-checking and the parameter synthesis problems become decidable.
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.
Similar content being viewed by others
References
Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: Proceedings of the 25th Annual Symposium on Theory of Computing, pp. 592–601. ACM Press, New York (1993)
Alur, R., Etessami, K., La Torre, S., Peled, D.: Parametric temporal logic for model measuring. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 159–173. Springer, Heidelberg (1999)
Bés, A.: A survey of arithmetical definability. A tribute to Maurice Boffa, Special Issue of Belg. Math. Soc., 1–54 (2002)
Bruyére, V., Dall’olio, E., Raskin, J.-F.: Durations, parametric model-checking in timed automata with Presburger arithmetic. In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol. 2607, pp. 687–698. Springer, Heidelberg (2003)
Allen Emerson, E., Trefler, R.J.: Parametric quantitative temporal reasoning. Logic in Computer Science, 336–343 (1999)
Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.: Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming 53, 183–220 (2002)
Wang, F.: Timing behavior analysis for real-time systems. In: Proceedings of the Tenth IEEE Symposium on Logic in Computer Science, pp. 112–122 (1995)
Wang, F., Hsiung, P.-A.: Parametric analysis of computer systems. Algebraic Methodology and Software Technology, 539–553 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bruyère, V., Raskin, JF. (2003). Real-Time Model-Checking: Parameters Everywhere. In: Pandya, P.K., Radhakrishnan, J. (eds) FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2003. Lecture Notes in Computer Science, vol 2914. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24597-1_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-24597-1_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20680-4
Online ISBN: 978-3-540-24597-1
eBook Packages: Springer Book Archive