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.
Similar content being viewed by others
Notes
This was done without a proof, hence, for completeness we detail the proof here.
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 }\).)
References
Alpern B, Schneider FB (1987) Recognizing safety and liveness. Distrib Comput 2(3):117–126
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–23
Basin DA, Jiménez CC, Klaedtke F, Zalinescu E (2014) Deciding safety and liveness in TPTL. Inf. Process. Lett. 114(12):680–688
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
Bauer A, Leucker M, Schallhart C (2011) Runtime verification for LTL and TLTL. ACM Trans Softw Eng Methodol 20(4):1–64
Bloem R, Könighofer B, Könighofer R, Wang C (2015) Shield synthesis: runtime enforcement for reactive systems. In: TACAS, pp 533–548
Bouajjani A, Esparza J, Maler O (1997) Reachability analysis of pushdown automata: application to model-checking. In: CONCUR, pp 135–150
Clarke EM, Emerson EA (1981) Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of programs, pp 52–71
Clarke EM, Grumberg O, Peled D (2000) Model checking. MIT Press, Cambridge
Diekert V, Leucker M (2014) Topology, monitorable properties and runtime verification. Theor Comput Sci 537:29–41
Drissi-Kaitouni O, Jard C (1988) Compiling temporal logic specifications into observers. INRIA Research Report RR-0881
Emerson EA, Clarke EM (1980) Characterizing correctness properties of parallel programs using fixpoints. In: ICALP, pp 169–181
Falcone Y, Fernandez J-C, Mounier L (2009) Runtime verification of safety/progress properties. In: RV’09, LNCS, vol 5779. Springer, pp 40–59
Falcone Y, Fernandez J-C, Mounier L (2012) What can you verify and enforce at runtime? STTT 14(3):349–382
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–146
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
Gerth R, Peled DA, Vardi MY, Wolper P (1995) Simple on-the-fly automatic verification of linear temporal logic. In: PSTV, pp 3–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
Havelund K, Rosu G (2002) Synthesizing monitors for safety properties. IN: TACAS’02, LNCS, vol 2280. Springer, pp 342–356
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
Isberner M, Howar F, Steffen B (2014) Learning register automata: from languages to program structures. Mach Learn 96:65–98
Isberner M, Howar F, Steffen B (2015) The open-source LearnLib. In: CAV’15, LNCS, vol 9206. Springer, pp 487–495
Kupferman O, Vardi G (2018) On relative and probabilistic finite counterability. Formal Methods Syst Des 52(2):117–146
Kupferman O, Vardi MY (2001) Model checking of safety properties. Formal Methods Syst Des 19(3):291–314
Lamport L (1977) Proving the correctness of multiprocess programs. IEEE Trans Softw Eng 3(2):125–143
Larsen KG, Legay A (2016) Statistical model checking: past, present, and future. In: ISoLA’16, LNCS, vol 9953. Springer, pp 3–15
Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems-specification. Springer, Berlin
Meredith PO, Jin D, Griffith D, Chen F, Rosu G (2011) An overview of the MOP runtime verification framework. STTT 14:249–289
Peled D, Havelund K (2018) Refining the safety-liveness classification of temporal properties according to monitorability. Models, mindsets, meta. Springer, Cham, pp 218–234
Peled DA, Vardi MY, Yannakakis M (1999) Black box checking, FORTE/PSTV’99.In: IFIP conference proceedings, vol 156. Kluwer, pp 225–240
Pnueli A, Zaks A (2006) PSL model checking and run-time verification via testers. In: FM’06, LNCS, vol 4085. Springer, pp 573–586
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
Safra S (1988) On the complexity of omega-automata. In: FOCS, pp 319–327
Sistla AP (1994) Safety, liveness and fairness in temporal logic. Formal Asp Comput 6(5):495–512
Sistla AP, Clarke EM (1982) The complexity of propositional linear temporal logics. In: STOC, pp 159–168
Thomas W (1990) Automata on infinite objects, handbook of theoretical computer science, volume B. Formal Models and Semantics. Elsevier, Amsterdam, pp 133–192
Vardi MY, Wolper P (1986) Automata-theoretic techniques for modal logics of programs. J Comput Syst Sci 32(2):183–221
Acknowledgements
The authors would like to thank Moran Omer for useful comments on the manuscript. The research performed by Klaus Havelund was carried out at Jet Propulsion Laboratory, California Institute of Technology, under a contract with the National Aeronautics and Space Administration. The research performed by Doron Peled was partially funded by Israeli Science Foundation grant 1464/18: “Efficient Runtime Verification for Systems with Lots of Data and its Applications”.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.
About this article
Cite this article
Havelund, K., Peled, D. On monitoring linear temporal properties. Form Methods Syst Des 60, 405–425 (2022). https://doi.org/10.1007/s10703-023-00429-8
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10703-023-00429-8