Skip to main content
SpringerLink
Log in
Book cover

Models, Mindsets, Meta: The What, the How, and the Why Not? pp 218–234Cite as

Refining the Safety–Liveness Classification of Temporal Properties According to Monitorability

  • Chapter
  • First Online:

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

Abstract

Runtime verification is the topic of analyzing execution traces using formal techniques. It includes monitoring the execution of a system against temporal properties, commonly to detect violations. Not every temporal property is fully monitorable however: in some cases, the correctness of the execution does not depend on any finite prefix. We study the connection between monitorability and Lamport’s classification of properties to safety and liveness and their dual classes. We refine the definition of monitorability and provide algorithms to check which verdicts can be expected, a priori and during runtime verification.

D. Peled—The research performed by this author was partially funded by Israeli Science Foundation grant 2239/15: “Runtime Measuring and Checking of Cyber Physical Systems”.

K. Havelund—The research performed by this author was carried out at Jet Propulsion Laboratory, California Institute of Technology, under a contract with the National Aeronautics and Space Administration.

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   39.99
Price excludes VAT (USA)
  • Available as EPUB and 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

Learn about institutional subscriptions

Notes

  1. 1.

    The classical interpretation of LTL is over states [22], but in the context of RV, we monitor a sequence of events that are reported by the instrumentation.

  2. 2.

    A finite extension of a good (bad or ugly) prefix remains good (bad or ugly, respectively).

  3. 3.

    One can also use other operators to express the same property, e.g., by adding a trivial disjunct, as in \((\upvarphi \vee (\Box p \wedge \Diamond \lnot p))\).

  4. 4.

    To show that a property is not monitorable, one needs to guess a state of \(\mathcal{B}_\upvarphi \times \mathcal{B}_{\lnot \upvarphi }\) and check that (1) it is reachable, and (2) one cannot reach from it an empty component, both for \(\mathcal{B}_\upvarphi \) and for \(\mathcal{B}_{\lnot \upvarphi }\). (There is no need to construct \(\mathcal{C}_\upvarphi \) or \(\mathcal{C}_{\lnot \upvarphi }\).).

  5. 5.

    Proving that liveness was PSPACE-hard was shown in [3].

References

  1. Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117–126 (1987)

    Article  MATH  Google Scholar 

  2. Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 1–33. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75632-5_1

    Chapter  Google Scholar 

  3. Basin, D.A., Jiménez, C.C., Klaedtke, F., Zalinescu, E.: Deciding safety and liveness in TPTL. Inf. Process. Lett. 114(12), 680–688 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  4. Bauer, A., Leucker, M., Schallhart, C.: The good, the bad, and the ugly, but how ugly is ugly? In: Sokolsky, O., Taşıran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 126–138. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-77395-5_11

    Chapter  MATH  Google Scholar 

  5. Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Method. 20(4), 14:1–14:64 (2011)

    Article  Google Scholar 

  6. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)

    Google Scholar 

  7. Diekert, V., Leucker, M.: Topology, monitorable properties and runtime verification. Theor. Comput. Sci. 537, 29–41 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  8. Drissi-Kaitouni, O., Jard, C.: Compiling temporal logic specifications into observers, INRIA Research Report RR-0881 (1988)

    Google Scholar 

  9. Falcone, Y., Fernandez, J.-C., Mounier, L.: Runtime verification of safety-progress properties. In: Bensalem, S., Peled, D.A. (eds.) RV 2009. LNCS, vol. 5779, pp. 40–59. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04694-0_4

    Chapter  Google Scholar 

  10. Falcone, Y., Fernandez, J.-C., Mounier, L.: What can you verify and enforce at runtime? STTT 14(3), 349–382 (2012)

    Article  Google Scholar 

  11. Fernandez, J.-C., Jard, C., Jéron, T., Viho, C.: An experiment in automatic generation of test suites for protocols with verification technology. Sci. Comput. Program. 29(1–2), 123–146 (1997)

    Article  Google Scholar 

  12. Gerth, R., Peled, D.A., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembiński, P., Średniawa, M. (eds.) PSTV 1995. IFIPAICT, pp. 3–18. Springer, Boston (1996). https://doi.org/10.1007/978-0-387-34892-6_1

    Chapter  Google Scholar 

  13. Havelund, K., Reger, G., Thoma, D., Zălinescu, E.: Monitoring events that carry data. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 61–102. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75632-5_3

    Chapter  Google Scholar 

  14. Havelund, K., Roşu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342–356. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46002-0_24

    Chapter  MATH  Google Scholar 

  15. Isberner, M., Howar, F., Steffen, B.: The TTT algorithm: a redundancy-free approach to active automata learning. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 307–322. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11164-3_26

    Chapter  Google Scholar 

  16. Isberner, M., Howar, F., Steffen, B.: Learning register automata: from languages to program structures. Mach. Learn. 96(1–2), 65–98 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  17. Isberner, M., Howar, F., Steffen, B.: The open-source LearnLib. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 487–495. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_32

    Chapter  Google Scholar 

  18. Kupferman, O., Vardi, G.: On relative and probabilistic finite counterability. Formal Meth. Syst. Des. 52(2), 117–146 (2018)

    Article  MATH  Google Scholar 

  19. Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Meth. Syst. Des. 19(3), 291–314 (2001)

    Article  MATH  Google Scholar 

  20. Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3(2), 125–143 (1977)

    Article  MathSciNet  MATH  Google Scholar 

  21. Larsen, K.G., Legay, A.: Statistical model checking: past, present, and future. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 3–15. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47166-2_1

    Chapter  Google Scholar 

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

    Book  MATH  Google Scholar 

  23. Meredith, P.O., Jin, D., Griffith, D., Chen, F., Rosu, G.: An overview of the MOP runtime verification framework. Int. J. Softw. Tools Technol. Transf. 14, 249–289 (2011)

    Article  Google Scholar 

  24. Peled, D., Vardi, M.Y., Yannakakis, M.: Black box checking. In: Wu, J., Chanson, S.T., Gao, Q. (eds.) Formal Methods for Protocol Engineering and Distributed Systems. IAICT, vol. 28, pp. 225–240. Springer, Boston, MA (1999). https://doi.org/10.1007/978-0-387-35578-8_13

    Chapter  Google Scholar 

  25. Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 573–586. Springer, Heidelberg (2006). https://doi.org/10.1007/11813040_38

    Chapter  Google Scholar 

  26. Baier, C., Bertrand, N., Größer, M.: The effect of tossing coins in omega-automata. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 15–29. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04081-8_2

    Chapter  Google Scholar 

  27. Sistla, A.P.: Safety, liveness and fairness in temporal logic. Formal Aspects Comput. 6(5), 495–512 (1994)

    Article  MATH  Google Scholar 

  28. Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. In: STOC 1982, pp. 159-168 (1982)

    Google Scholar 

  29. Thomas, W.: Automata on infinite objects, handbook of theoretical computer science. In: Formal Models and Semantics, vol. B, pp. 133–192 (1990)

    Google Scholar 

  30. Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of programs. J. Comput. Syst. Sci. 32(2), 183–221 (1986)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Bar Ilan University, Ramat Gan, Israel

    Doron Peled

  2. Jet Propulsion Laboratory, California Institute of Technology, Pasadena, USA

    Klaus Havelund

Authors
  1. Doron Peled
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Klaus Havelund
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Doron Peled or Klaus Havelund .

Editor information

Editors and Affiliations

  1. Lero–The Irish Software Research Center, University of Limerick, Limerick, Ireland

    Tiziana Margaria

  2. Verimag Laboratory, Grenoble, France

    Susanne Graf

  3. Aalborg University, Aalborg, Denmark

    Kim G. Larsen

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Peled, D., Havelund, K. (2019). Refining the Safety–Liveness Classification of Temporal Properties According to Monitorability. In: Margaria, T., Graf, S., Larsen, K. (eds) Models, Mindsets, Meta: The What, the How, and the Why Not?. Lecture Notes in Computer Science(), vol 11200. Springer, Cham. https://doi.org/10.1007/978-3-030-22348-9_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-22348-9_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-22347-2

  • Online ISBN: 978-3-030-22348-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation