Skip to main content
SpringerLink
Log in
Book cover

Runtime Verification pp 71–86Cite as

On Verifying Hennessy-Milner Logic with Recursion at Runtime

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9333))

Abstract

We study \(\mu \) HML (a branching-time logic with least and greatest fixpoints) from a runtime verification perspective. We establish which subset of the logic can be verified at runtime and define correct monitor-synthesis algorithms for this subset. We also prove completeness results these logical subsets that show that no other properties apart from those identified can be verified at runtime.

The research of L. Aceto and A. Ingolfsdottir was supported by the project 001-ABEL-CM-2013 of the NILS Science and Sustainability Programme and the project Nominal SOS (nr. 141558-051) of the Icelandic Research Fund.

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.

    A transition sequence is complete if it is either infinite or affords no more actions.

  2. 2.

    If a monitor cannot match a process action, but can transition silently, it is allowed to do so, and the matching check is applied again to the \(\tau \)-derivative monitor.

  3. 3.

    The problem of determining whether a (general) formula is logically equivalent to one in mHML is decidable in exponential time — probably EXPTIME complete.

References

  1. Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)

    Book  MATH  Google Scholar 

  2. Aceto, L., Ingólfsdóttir, A.: Testing Hennessy-Milner logic with recursion. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol. 1578, pp. 41–55. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  3. Aceto, L., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, New York (2007)

    Book  MATH  Google Scholar 

  4. Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 44–57. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  6. Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. Logic Comput. 20(3), 651–674 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  7. Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. TOSEM 20(4), 14 (2011)

    Article  Google Scholar 

  8. Cassar, I., Francalanza, A.: On synchronous and asynchronous monitor instrumentation for actor systems. In: FOCLASA, vol. 175, pp. 54–68 (2014)

    Google Scholar 

  9. Cerone, A., Hennessy, M.: Process behaviour: formulae vs. tests. In: EXPRESS. EPTCS, vol. 41, pp. 31–45 (2010)

    Google Scholar 

  10. Chang, E., Manna, Z., Pnueli, A.: Characterization of temporal property classes. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 474–486. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  11. Cini, C., Francalanza, A.: An LTL proof system for runtime verification. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 581–595. Springer, Heidelberg (2015)

    Google Scholar 

  12. Colombo, C., Pace, G., Schneider, G.: LARVA – safer monitoring of real-time Java programs (Tool paper). In: SEFM, pp. 33–37 (2009)

    Google Scholar 

  13. Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: 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)

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  15. Francalanza, A., Gauci, A., Pace, G.J.: Distributed system contract monitoring. JLAP 82(5–7), 186–215 (2013)

    MathSciNet  MATH  Google Scholar 

  16. Francalanza, A., Seychell, A.: Synthesising correct concurrent runtime monitors. In: Formal Methods in System Design (FMSD), pp. 1–36 (2014)

    Google Scholar 

  17. Geilen, M.: On the construction of monitors for temporal logic properties. In: RV. ENTCS, vol. 55, pp. 181–199 (2001)

    Google Scholar 

  18. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)

    MATH  Google Scholar 

  19. Kozen, D.: Results on the propositional \(\mu \)-calculus. TCS 27, 333–354 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  20. Leucker, M., Schallhart, C.: A brief account of runtime verification. JLAP 78(5), 293–303 (2009)

    MATH  Google Scholar 

  21. Manna, Z., Pnueli, A.: Completing the temporal picture. TCS 83(1), 97–130 (1991)

    Article  MATH  Google Scholar 

  22. Milner, R.: A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1982)

    MATH  Google Scholar 

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

    Chapter  Google Scholar 

  24. Sen, K., Roşu, G., Agha, G.: Generating optimal linear temporal logic monitors by coinduction. In: Saraswat, V.A. (ed.) ASIAN 2003. LNCS, vol. 2896, pp. 260–275. Springer, Heidelberg (2003)

    Google Scholar 

  25. detectEr Project. http://www.cs.um.edu.mt/svrg/Tools/detectEr/

Download references

Author information

Authors and Affiliations

  1. CS, ICT, University of Malta, Msida, Malta

    Adrian Francalanza

  2. ICE-TCS, Reykjavik University, Reykjavik, Iceland

    Luca Aceto & Anna Ingolfsdottir

Authors
  1. Adrian Francalanza
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Luca Aceto
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Anna Ingolfsdottir
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Adrian Francalanza .

Editor information

Editors and Affiliations

  1. TU Wien, Vienna, Austria

    Ezio Bartocci

  2. Max Planck Institute for Software Systems, Kaiserslautern, Germany

    Rupak Majumdar

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Francalanza, A., Aceto, L., Ingolfsdottir, A. (2015). On Verifying Hennessy-Milner Logic with Recursion at Runtime. In: Bartocci, E., Majumdar, R. (eds) Runtime Verification. Lecture Notes in Computer Science(), vol 9333. Springer, Cham. https://doi.org/10.1007/978-3-319-23820-3_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-23820-3_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-23819-7

  • Online ISBN: 978-3-319-23820-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation