Skip to main content
SpringerLink
Log in

Verifying Temporal Properties in Real Models

  • Conference paper
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2013)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8312))

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

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Dill, D.: A theory of timed automata. TCS 126, 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  2. 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)

    Chapter  Google Scholar 

  3. Burgess, J.P., Gurevich, Y.: The decision problem for linear temporal logic. Notre Dame J. Formal Logic 26(2), 115–128 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  4. 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)

    Chapter  Google Scholar 

  5. Burgess, J.P.: Axioms for tense logic I: “Since” and “Until”. Notre Dame J. Formal Logic 23(2), 367–374 (1982)

    Article  MathSciNet  MATH  Google Scholar 

  6. Davoren, J., Nerode, A.: Logics for hybrid systems. Proc. IEEE (2000)

    Google Scholar 

  7. French, T., McCabe-Dansted, J., Reynolds, M.: Synthesis for temporal logic over the reals. In: AiML, 2012, pp. 217–238. College Pub. (2012)

    Google Scholar 

  8. 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

  9. 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

  10. French, T., McCabe-Dansted, J., Reynolds, M.: Complexity of Model Checking over General Linear Time. In: TIME 2013, pp. 107–116. IEEE CPS (2013)

    Google Scholar 

  11. 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)

    Google Scholar 

  12. Gabbay, D., Hodkinson, I.: An axiomatisation of the temporal logic with until and since over the real numbers. JLC 1(2), 229–260 (1990)

    MathSciNet  MATH  Google Scholar 

  13. 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)

    Google Scholar 

  14. Gabbay, D., Hodkinson, I., Reynolds, M.: Temporal Logic: Mathematical Foundations and Computational Aspects. OUP (1994)

    Google Scholar 

  15. 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)

    Google Scholar 

  16. Kamp, H.: Tense logic and the theory of linear order. PhD thesis, University of California, Los Angeles (1968)

    Google Scholar 

  17. Kurtonina, N., de Rijke, M.: Bisimulations for temporal logic. Journal of Logic, Language and Information 6(4), 403–425 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  18. Läuchli, H., Leonard, J.: On the elementary theory of linear order. Fundamenta Mathematicae 59, 109–116 (1966)

    MathSciNet  MATH  Google Scholar 

  19. Christopher McCabe-Dansted, J.: Model Checker Online (2012), http://www.csse.uwa.edu.au/~mark/research/Online/mechecker.html

  20. Rabin, M.O.: Decidability of second order theories and automata on infinite trees. American Mathematical Society Transactions 141, 1–35 (1969)

    MathSciNet  MATH  Google Scholar 

  21. Reynolds, M.: An axiomatization for Until and Since over the reals without the IRR rule. Studia Logica 51, 165–193 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  22. Reynolds, M.: The complexity of the temporal logic over the reals. Annals of Pure and Applied Logic 161(8), 1063–1096 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  23. Reynolds, M.: The complexity of decision problems for linear temporal logics. Journal of Studies in Logic 3, 19–50 (2010)

    Google Scholar 

  24. Rosenstein, J.G.: Linear Orderings. Academic Press, New York (1982)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science and Software Engineering, University of Western Australia, Crawley, Perth Western, Australia, 6009

    Tim French, John McCabe-Dansted & Mark Reynolds

Authors
  1. Tim French
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. John McCabe-Dansted
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mark Reynolds
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, WA, USA

    Ken McMillan

  2. University of Innsbruck, Austria

    Aart Middeldorp

  3. University of Manchester, UK

    Andrei Voronkov

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation