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
Formal Methods in System Design
Published in: Formal Methods in System Design 3/2022

22-06-2023

On monitoring linear temporal properties

Authors: Klaus Havelund, Doron Peled

Published in: Formal Methods in System Design | Issue 3/2022

Log in

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

search-config
loading …

Abstract

Runtime verification facilitates monitoring the executions of a system against temporal properties, commonly to detect violations. Not every temporal property is fully monitorable however: in some cases, a positive or negative verdict on the monitored execution does not depend on any finite prefix of it. We study the problem of monitoring properties written in linear temporal logic. We provide a complete classification of the temporal properties based on the ability to provide positive and/or negative verdicts in finite time.
previous article Mining definitions in Kissat with Kittens
next article Machine learning and logic: a new frontier in artificial intelligence

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 "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

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
Footnotes
1
This was done without a proof, hence, for completeness we detail the proof here.
 
2
To show that a property is not monitorable, one needs to guess a state of \(\mathcal{B}_\varphi \times \mathcal{B}_{\lnot \varphi }\) and check that (1) it is reachable, and (2) one cannot reach from it an empty component, both for \(\mathcal{B}_\varphi\) and for \(\mathcal{B}_{\lnot \varphi }\). (There is no need to construct \(\mathcal{C}_\varphi\) or \(\mathcal{C}_{\lnot \varphi }\).)
 
Literature
1.
Alpern B, Schneider FB (1987) Recognizing safety and liveness. Distrib Comput 2(3):117–126CrossRefMATH
2.
Bartocci E, Falcone Y, Francalanza A, Leucker M, Reger G (2018) An introduction to runtime verification. Lectures on runtime verification–introductory and advanced topics, LNCS, vol 10457. Springer, Berlin, pp 1–23CrossRef
3.
4.
Bauer A, Leucker M, Schallhart C (2007) The good, the bad, and the ugly, but how ugly is ugly?. In: RV’07, LNCS, vol 4839. Springer, pp 126–138
5.
Bauer A, Leucker M, Schallhart C (2011) Runtime verification for LTL and TLTL. ACM Trans Softw Eng Methodol 20(4):1–64CrossRef
6.
Bloem R, Könighofer B, Könighofer R, Wang C (2015) Shield synthesis: runtime enforcement for reactive systems. In: TACAS, pp 533–548
7.
Bouajjani A, Esparza J, Maler O (1997) Reachability analysis of pushdown automata: application to model-checking. In: CONCUR, pp 135–150
8.
Clarke EM, Emerson EA (1981) Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of programs, pp 52–71
9.
Clarke EM, Grumberg O, Peled D (2000) Model checking. MIT Press, CambridgeMATH
10.
11.
Drissi-Kaitouni O, Jard C (1988) Compiling temporal logic specifications into observers. INRIA Research Report RR-0881
12.
Emerson EA, Clarke EM (1980) Characterizing correctness properties of parallel programs using fixpoints. In: ICALP, pp 169–181
13.
Falcone Y, Fernandez J-C, Mounier L (2009) Runtime verification of safety/progress properties. In: RV’09, LNCS, vol 5779. Springer, pp 40–59
14.
Falcone Y, Fernandez J-C, Mounier L (2012) What can you verify and enforce at runtime? STTT 14(3):349–382CrossRef
15.
Fernandez J-C, Jard C, Jéron T, Viho C (1997) An experiment in automatic generation of test suites for protocols with verification technology. Sci Comput Program 29(1–2):123–146CrossRef
16.
Falcone Y, Havelund K, Reger G (2013) A tutorial on runtime verification. Summer school Marktoberdorf 2012-Engineering dependable software systems. IOS Press, Amsterdam, pp 141–175
17.
Gerth R, Peled DA, Vardi MY, Wolper P (1995) Simple on-the-fly automatic verification of linear temporal logic. In: PSTV, pp 3–18
18.
Havelund K, Reger G, Thoma D, Zălinescu E (2018) Monitoring events that carry data, lectures on runtime verification—introductory and advanced topics, LNCS, vol 10457. Springer, Berlin, pp 61–102
19.
Havelund K, Rosu G (2002) Synthesizing monitors for safety properties. IN: TACAS’02, LNCS, vol 2280. Springer, pp 342–356
20.
Isberner M, Howar F, Steffen B (2014) The TTT algorithm: a redundancy-free approach to active automata learning. In: RV’14, LNCS, vol 8734. Springer, pp 307–322
21.
22.
Isberner M, Howar F, Steffen B (2015) The open-source LearnLib. In: CAV’15, LNCS, vol 9206. Springer, pp 487–495
23.
Kupferman O, Vardi G (2018) On relative and probabilistic finite counterability. Formal Methods Syst Des 52(2):117–146CrossRefMATH
24.
Kupferman O, Vardi MY (2001) Model checking of safety properties. Formal Methods Syst Des 19(3):291–314CrossRefMATH
25.
26.
Larsen KG, Legay A (2016) Statistical model checking: past, present, and future. In: ISoLA’16, LNCS, vol 9953. Springer, pp 3–15
27.
Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems-specification. Springer, BerlinCrossRefMATH
28.
Meredith PO, Jin D, Griffith D, Chen F, Rosu G (2011) An overview of the MOP runtime verification framework. STTT 14:249–289CrossRef
29.
Peled D, Havelund K (2018) Refining the safety-liveness classification of temporal properties according to monitorability. Models, mindsets, meta. Springer, Cham, pp 218–234
30.
Peled DA, Vardi MY, Yannakakis M (1999) Black box checking, FORTE/PSTV’99.In: IFIP conference proceedings, vol 156. Kluwer, pp 225–240
31.
Pnueli A, Zaks A (2006) PSL model checking and run-time verification via testers. In: FM’06, LNCS, vol 4085. Springer, pp 573–586
32.
Queille J-P, Sifakis J (1981) Iterative methods for the analysis of Petri nets. In: Selected papers from the first and the second European workshop on application and theory of Petri nets, pp 161–167
33.
Safra S (1988) On the complexity of omega-automata. In: FOCS, pp 319–327
34.
Sistla AP (1994) Safety, liveness and fairness in temporal logic. Formal Asp Comput 6(5):495–512CrossRefMATH
35.
Sistla AP, Clarke EM (1982) The complexity of propositional linear temporal logics. In: STOC, pp 159–168
36.
Thomas W (1990) Automata on infinite objects, handbook of theoretical computer science, volume B. Formal Models and Semantics. Elsevier, Amsterdam, pp 133–192
37.
Metadata
Title
On monitoring linear temporal properties
Authors
Klaus Havelund
Doron Peled
Publication date
22-06-2023
Publisher
Springer US
Published in
Formal Methods in System Design / Issue 3/2022
Print ISSN: 0925-9856
Electronic ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-023-00429-8

Other articles of this Issue 3/2022

Formal Methods in System Design 3/2022 Go to the issue

OriginalPaper

Achieving high coverage in hardware equivalence checking via concolic verification

OriginalPaper

Machine learning and logic: a new frontier in artificial intelligence

OriginalPaper

Verification modulo theories

EditorialNotes

Edmund Melson Clarke, Jr. (1945–2020)

OriginalPaper

Mining definitions in Kissat with Kittens

OriginalPaper

SMT-based verification of program changes through summary repair

Premium Partner

    Image Credits