Abstract
LTLC is a continuous-time linear temporal logic for the specification of real-time systems. It can express both real-time systems and their properties. With LTLC, real-time systems can be described at different levels of abstraction, from high-level requirement specifications to low-level implementation models, and the conformance between different descriptions can be expressed by logical implication. The full logic of LTLC is undecidable. This paper will show that the existentially quantified fragment of LTLC is decidable. We achieve this goal by showing that the fragment can be translated into timed automata. Because the emptiness problem for timed automata is decidable, we then get a decision procedure for satisfiability for this fragment. This decidable part of LTLC is quite expressive. Many important real-time properties, such as bounded-response and bounded-invariance properties, can be expressed in it. The translation also enables us to develop a decision procedure for model checking real-time systems with quantifier-free LTLC specifications.
Supported by the National High Technology Development 863 Program of China under Grant No.2001AA113200; the National Natural Science Foundation of China under Grant No.60273025; and the National Grand Fundamental Research 973 Program of China under Grant No. 2002cb312200.
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. Information and Computation 104, 2–34 (1993)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. Journal of the ACM 43, 116–146 (1996)
Alur, R., Henzinger, T.A.: Logics and models of real time: a survey. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, Springer, Heidelberg (1992)
Alur, R., Henzinger, T.A.: A really temporal logic. Journal of the ACM 41, 181–204 (1994)
Bjørner, N., Manna, Z., Sipma, H., Uribe, T.: Deductive Verification of Real-time Systems using STeP. Theoretical Computer Science 253, 27–60 (2001)
Hirshfeld, Y., Rabinovich, A.: Quantitative Temporal Logic. In: Flum, J., RodrÃguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 172–187. Springer, Heidelberg (1999)
Laroussinie, F., Larsen, K., Weise, C.: From timed automata to logic -and back. In: Hájek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol. 969, pp. 529–540. Springer, Heidelberg (1995)
Li, G.: LTLC: A Continuous-time Temporal Logic for Real-time and Hybrid Systems, PhD Thesis, Institute of Software, Chinese Academy of Sciences (March 2001)
Li, G., Tang, Z.: Modeling Real-Time Systems with Continuous-Time Temporal Logic. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 231–236. Springer, Heidelberg (2002)
Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems: Specification. Springer, New York (1992)
Manna, Z., Pnueli, A.: Clocked transition systems. In: Logic and Software Workshop, Beijing, China (1995)
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
Li, G., Tang, Z. (2003). Translating a Continuous-Time Temporal Logic into Timed Automata. In: Ohori, A. (eds) Programming Languages and Systems. APLAS 2003. Lecture Notes in Computer Science, vol 2895. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-40018-9_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-40018-9_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20536-4
Online ISBN: 978-3-540-40018-9
eBook Packages: Springer Book Archive