Abstract
Based on pioneering work of Läuchli and Leonard in the 1960s, a novel and expressive formal language, Model Expressions, for describing the compositional construction of general linear temporal structures has recently been proposed. A sub-language, Real Model Expressions, is capable of specifying models over the real flow of time but its semantics are subtly different because of the specific properties of the real numbers.
Model checking techniques have been developed for the general linear Model Expressions and it was shown that checking temporal formulas against structures described in the formal language is PSPACE-Complete and linear in the length of the model expression.
In this paper we present a model checker for temporal formulas over real-flowed models. In fact the algorithm, and so its complexity, is the same as for the general linear case.
To show that this is adequate we use a concept of temporal bisimulations and establish that it is respected by the compositional construction method. We can then check the correctness of using the general linear model checking algorithm when applied to real model expressions with their special semantics on real-flowed structures.
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., Dill, D.: A theory of timed automata. TCS 126, 183–235 (1994)
Alur, R., Henzinger, T.A.: Logics and models of real time: A survey. In: de Bakker, J.W., Huizing, C., de Roever, W.P., Rozenberg, G. (eds.) REX 1991. LNCS, vol. 600, pp. 74–106. Springer, Heidelberg (1992)
Burgess, J.P., Gurevich, Y.: The decision problem for linear temporal logic. Notre Dame J. Formal Logic 26(2), 115–128 (1985)
Bouyer, P., Markey, N., Ouaknine, J., Worrell, J.B.: On expressiveness and complexity in real-time model checking. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 124–135. Springer, Heidelberg (2008)
Burgess, J.P.: Axioms for tense logic I: “Since” and “Until”. Notre Dame J. Formal Logic 23(2), 367–374 (1982)
Davoren, J., Nerode, A.: Logics for hybrid systems. Proc. IEEE (2000)
French, T., McCabe-Dansted, J., Reynolds, M.: Synthesis for temporal logic over the reals. In: AiML, 2012, pp. 217–238. College Pub. (2012)
French, T., McCabe-Dansted, J., Reynolds, M.: Verifying temporal properties in real models (long report version) (2013), http://www.csse.uwa.edu.au/~mark/research/Online/vtprm.html
French, T., McCabe-Dansted, J., Reynolds, M.: Synthesis for continuous time: long draft online. Journal Version Submitted, http://www.csse.uwa.edu.au/~mark/research/Online/sctm.htm
French, T., McCabe-Dansted, J., Reynolds, M.: Complexity of Model Checking over General Linear Time. In: TIME 2013, pp. 107–116. IEEE CPS (2013)
French, T., McCabe-Dansted, J., Reynolds, M.: Model Checking General Linear Temporal Logic. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS, vol. 8123, pp. 119–133. Springer, Heidelberg (2013)
Gabbay, D., Hodkinson, I.: An axiomatisation of the temporal logic with until and since over the real numbers. JLC 1(2), 229–260 (1990)
Gabbay, D.M., Hodkinson, I.M., Reynolds, M.A.: Temporal expressive completeness in the presence of gaps. In: Oikkonen, et al. (eds.) Logic Colloquium 1990. LNL, vol. 2, pp. 89–121. Springer (1993)
Gabbay, D., Hodkinson, I., Reynolds, M.: Temporal Logic: Mathematical Foundations and Computational Aspects. OUP (1994)
Hodkinson, I., Reynolds, M.: Separation: past, present &future. In: We Will Show Them: Essays in Honour of D. Gabbay, pp. 117–142. Coll. Publ. (2005)
Kamp, H.: Tense logic and the theory of linear order. PhD thesis, University of California, Los Angeles (1968)
Kurtonina, N., de Rijke, M.: Bisimulations for temporal logic. Journal of Logic, Language and Information 6(4), 403–425 (1997)
Läuchli, H., Leonard, J.: On the elementary theory of linear order. Fundamenta Mathematicae 59, 109–116 (1966)
Christopher McCabe-Dansted, J.: Model Checker Online (2012), http://www.csse.uwa.edu.au/~mark/research/Online/mechecker.html
Rabin, M.O.: Decidability of second order theories and automata on infinite trees. American Mathematical Society Transactions 141, 1–35 (1969)
Reynolds, M.: An axiomatization for Until and Since over the reals without the IRR rule. Studia Logica 51, 165–193 (1992)
Reynolds, M.: The complexity of the temporal logic over the reals. Annals of Pure and Applied Logic 161(8), 1063–1096 (2010)
Reynolds, M.: The complexity of decision problems for linear temporal logics. Journal of Studies in Logic 3, 19–50 (2010)
Rosenstein, J.G.: Linear Orderings. Academic Press, New York (1982)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
French, T., McCabe-Dansted, J., Reynolds, M. (2013). Verifying Temporal Properties in Real Models. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2013. Lecture Notes in Computer Science, vol 8312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-45221-5_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-45221-5_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-45220-8
Online ISBN: 978-3-642-45221-5
eBook Packages: Computer ScienceComputer Science (R0)