Skip to main content
SpringerLink
Log in
Book cover

Pillars of Computer Science pp 475–505Cite as

Checking Temporal Properties of Discrete, Timed and Continuous Behaviors

  • Chapter

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

Abstract

We survey some of the problems associated with checking whether a given behavior (a sequence, a Boolean signal or a continuous signal) satisfies a property specified in an appropriate temporal logic and describe two such monitoring algorithms for the real-time logic MITL.

This is a preview of subscription content, 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   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abarbanel, Y., et al.: FoCs: Automatic Generation of Simulation Checkers from Formal Specifications. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 538–542. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  2. Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126, 183–235 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  3. Alur, R., Feder, T., Henzinger, T.A.: The Benefits of Relaxing Punctuality. Journal of the ACM 43, 116–146 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  4. Alur, R., Henzinger, T.A.: Logics and Models of Real-Time: A Survey. In: Huizing, C., et al. (eds.) REX 1991. LNCS, vol. 600, pp. 74–106. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  5. Asarin, E.: Challenges in Timed Languages. Bulletin of EATCS 83 (2004)

    Google Scholar 

  6. Asarin, E., Caspi, P., Maler, O.: Timed Regular Expressions. The Journal of the ACM 49, 172–206 (2002)

    Article  MathSciNet  Google Scholar 

  7. Beer, I., et al.: The Temporal Logic Sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, Springer, Heidelberg (2001)

    Google Scholar 

  8. Bensalem, S., et al.: Testing Conformance of Real-time Applications with Automatic Generation of Observers. In: RV 2004 (2004)

    Google Scholar 

  9. Donzé, A.: Etude d’un Modèle de Contrôleur Hybride. Master’s thesis, INPG (2003)

    Google Scholar 

  10. Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Heidelberg (2006)

    Google Scholar 

  11. Eisner, C., et al.: Reasoning with Temporal Logic on Truncated Paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27–39. Springer, Heidelberg (2003)

    Google Scholar 

  12. Geilen, M.C.W., Dams, D.R.: An On-the-fly Tableau Construction for a Real-time Temporal Logic. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, pp. 276–290. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  13. Geilen, M.C.W.: Formal Techniques for Verification of Complex Real-time Systems, PhD thesis, Eindhoven University of Technology (2002)

    Google Scholar 

  14. Geilen, M.C.W.: An Improved On-the-fly Tableau Construction for a Real-time Temporal Logic. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 394–406. Springer, Heidelberg (2003)

    Google Scholar 

  15. Havelund, K., Rosu, G. (eds.): Runtime Verification RV 2002. ENTCS 70(4) (2002)

    Google Scholar 

  16. Havelund, K., Rosu, G.: Synthesizing Monitors for Safety Properties. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol. 2280, pp. 342–356. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  17. Henzinger, T.A.: It’s about Time: Real-time Logics Reviewed. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 439–454. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  18. Hirshfeld, Y., Rabinovich, A.: Logics for Real Time: Decidability and Complexity. Fundamenta Informaticae 62, 1–28 (2004)

    MATH  MathSciNet  Google Scholar 

  19. Kesten, Y., Pnueli, A.: A Compositional Approach to CTL* Verification. Theoretical Computer Science 331, 397–428 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  20. Kossentini C., Caspi, P.: Approximation, Sampling and Voting in Hybrid Computing Systems, HSCC (to appear, 2006)

    Google Scholar 

  21. Koymans, R.: Specifying Real-time Properties with with Metric Temporal Logic. Real-time Systems, 255–299 (1990)

    Google Scholar 

  22. Kim, M., et al.: Monitoring, Checking, and Steering of Real-time Systems. RV 2002, ENTCS 70(4) (2002)

    Google Scholar 

  23. Kristoffersen, K.J., Pedersen, C., Andersen, H.R.: Runtime Verification of Timed LTL using Disjunctive Normalized Equation Systems. RV 2003 ENTCS 89(2) (2003)

    Google Scholar 

  24. Krichen, M., Tripakis, S.: Black-box Conformance Testing for Real-time Systems. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 109–126. Springer, Heidelberg (2004)

    Google Scholar 

  25. Kupferman, O., Vardi, M.Y.: On Bounded Specifications. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 24–38. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  26. Mosterman, P.J.: An Overview of Hybrid Simulation Phenomena and their Support by Simulation Packages. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 165–177. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  27. Lichtenstein, O., Pnueli, A., Zuck, L.D.: The Glory of the Past. In: LCTES 2000. LNCS, pp. 196–218 (1985)

    Google Scholar 

  28. Maler, O.: A Unified Approach for Studying Discrete and Continuous Dynamical Systems. In: CDC, pp. 2083–2088. IEEE, Los Alamitos (1998)

    Google Scholar 

  29. Maler, O.: Control from Computer Science. Annual Reviews in Control 26, 175–187 (2002)

    Article  Google Scholar 

  30. Maler, O.: Analog Circuit Verification: a State of an Art. ENTCS 153, 3–7 (2006)

    Google Scholar 

  31. Maler, O., Nickovic, D.: Monitoring Temporal Properties of Continuous Signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004)

    Google Scholar 

  32. Maler, O., Nickovic, D., Pnueli, A.: Real Time Temporal Logic: Past, Present, Future. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 2–16. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  33. Maler, O., Nickovic, D., Pnueli, A.: From MITL to Timed Automata. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 274–289. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  34. Maler, O., Nickovic, D., Pnueli, A.: On Synthesizing Controllers from Bounded-Response Properties. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 95–107. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  35. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer, Heidelberg (1992)

    Google Scholar 

  36. Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995)

    Google Scholar 

  37. Nickovic, D., Maler, O.: AMT: A Property-Based Monitoring Tool for Analog Systems. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 304–319. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  38. Safra, S.: On the Complexity of ω-Automata. In: FOCS 1988, pp. 319–327 (1988)

    Google Scholar 

  39. Sokolsky, O., Viswanathan, M.(eds.): Runtime Verification RV 2003. ENTCS 89(2) (2003)

    Google Scholar 

  40. Trakhtenbrot, B.A.: Finite Automata and the Logic of One-place Predicates. DAN SSSR 140 (1961)

    Google Scholar 

  41. Thati, P., Rosu, G.: Monitoring Algorithms for Metric Temporal Logic Specifications. RV (2004)

    Google Scholar 

  42. Tripakis, S.: Fault Diagnosis for Timed Automata. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 205–224. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  43. Vardi, M.Y., Wolper, P.: An Automata-theoretic Approach to Automatic Program Verification. In: LICS 1986, pp. 322–331. IEEE, Los Alamitos (1986)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Verimag, 2 Av. de Vignate, 38610, Gières, France

    Oded Maler & Dejan Nickovic

  2. Weizmann Institute of Science, Rehovot, 76100, Israel

    Amir Pnueli

  3. New York University, 251 Mercer St., New York, NY 10012, USA

    Amir Pnueli

Authors
  1. Oded Maler
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dejan Nickovic
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Amir Pnueli
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Arnon Avron Nachum Dershowitz Alexander Rabinovich

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Maler, O., Nickovic, D., Pnueli, A. (2008). Checking Temporal Properties of Discrete, Timed and Continuous Behaviors. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds) Pillars of Computer Science. Lecture Notes in Computer Science, vol 4800. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78127-1_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-78127-1_26

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-78126-4

  • Online ISBN: 978-3-540-78127-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation