Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Towards a Verified Artificial Pancreas: Challenges and Solutions for Runtime Verification Read chapter Read first chapter

2015 | OriginalPaper | Chapter

On Verifying Hennessy-Milner Logic with Recursion at Runtime

Authors : Adrian Francalanza, Luca Aceto, Anna Ingolfsdottir

Published in: Runtime Verification

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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 https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-23820-3_5/367589_1_En_5_IEq2_HTML.gif these logical subsets that show that no other properties apart from those identified can be verified at runtime.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Robust Online Monitoring of Signal Temporal Logic
next chapter Assuring the Guardians
Footnotes
1
A transition sequence is complete if it is either infinite or affords no more actions.
 
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
The problem of determining whether a (general) formula is logically equivalent to one in mHML is decidable in exponential time — probably EXPTIME complete.
 
Literature
1.
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)CrossRefMATH
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) CrossRef
3.
Aceto, L., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, New York (2007) CrossRefMATH
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) CrossRef
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) CrossRef
6.
7.
Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. TOSEM 20(4), 14 (2011)CrossRef
8.
Cassar, I., Francalanza, A.: On synchronous and asynchronous monitor instrumentation for actor systems. In: FOCLASA, vol. 175, pp. 54–68 (2014)
9.
Cerone, A., Hennessy, M.: Process behaviour: formulae vs. tests. In: EXPRESS. EPTCS, vol. 41, pp. 31–45 (2010)
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) CrossRef
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)
12.
Colombo, C., Pace, G., Schneider, G.: LARVA – safer monitoring of real-time Java programs (Tool paper). In: SEFM, pp. 33–37 (2009)
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) CrossRef
14.
Falcone, Y., Fernandez, J.-C., Mounier, L.: What can you verify and enforce at runtime? STTT 14(3), 349–382 (2012)CrossRef
15.
Francalanza, A., Gauci, A., Pace, G.J.: Distributed system contract monitoring. JLAP 82(5–7), 186–215 (2013)MathSciNetMATH
16.
Francalanza, A., Seychell, A.: Synthesising correct concurrent runtime monitors. In: Formal Methods in System Design (FMSD), pp. 1–36 (2014)
17.
Geilen, M.: On the construction of monitors for temporal logic properties. In: RV. ENTCS, vol. 55, pp. 181–199 (2001)
18.
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)MATH
19.
20.
Leucker, M., Schallhart, C.: A brief account of runtime verification. JLAP 78(5), 293–303 (2009)MATH
21.
22.
Milner, R.: A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1982) MATH
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) CrossRef
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)
25.
Metadata
Title
On Verifying Hennessy-Milner Logic with Recursion at Runtime
Authors
Adrian Francalanza
Luca Aceto
Anna Ingolfsdottir
Copyright Year
2015
Book
Runtime Verification

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

Electronic ISBN: 978-3-319-23820-3

Copyright Year: 2015

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

Premium Partner

    Image Credits