More Web Proxy on the site http://driver.im/

Article

An LTL Proof System for Runtime Verification

Authors:

Adrian FrancalanzaAuthors Info & Claims

Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 9035

Pages 581 - 595

https://doi.org/10.1007/978-3-662-46681-0_54

Published: 11 April 2015 Publication History

Abstract

We propose a local proof system for LTL formalising deductions within the constraints of Runtime Verification RV, and show how such a system can be used as a basis for the construction of online runtime monitors. Novel soundness and completeness results are proven for this system. We also prove decidability and incrementality properties for a monitoring algorithm constructed from it. Finally, we relate its expressivity to existing symbolic analysis techniques used in RV.

References

[1]

Bauer, A., Falcone, Y.: Decentralised LTL Monitoring. In: Giannakopoulou, D., Méry, D. eds. FM 2012. LNCS, vol. 7436, pp. 85---100. Springer, Heidelberg 2012

[2]

Brunnler, K., Lange, M.: Cut-free sequent systems for temporal logic. JLAP 762, 216---225 2008

[3]

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

Digital Library

[4]

Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. Logic and Comput. 203, 651---674 2010

Digital Library

[5]

Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. TOSEM 204, 14 2011

Digital Library

[6]

Bradfield, J., Stirling, C.: Local model-checking for infinite state spaces. TCS 96, 157---174 1992

Digital Library

[7]

Buss, S.R. ed.: Handbook of Proof Theory. Elsevier 1998

[8]

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

[9]

Geilen, M.: On the construction of monitors for temporal logic properties. ENTCS 552, 181---199 2001

[10]

Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: POPL, pp. 163---173. ACM, New York 1980

Digital Library

[11]

Havelund, K., Rosu, G.: Monitoring programs using rewriting. In: ASE, pp. 135---143. IEEE, Wash., DC 2001

Digital Library

[12]

Kojima, K., Igarashi, A.: Constructive linear-time temporal logic: Proof systems and kripke semantics. Inf. Comput. 20912, 1491---1503 2011

Digital Library

[13]

Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Form. Methods Syst. Des. 193, 291---314 2001

Digital Library

[14]

Leucker, M., Schallhart, C.: A brief account of Runtime Verification. JLAP 785, 293---303 2009

[15]

Manna, Z., Pnueli, A.: Completing the Temporal Picture. Theoretical Computer Science 831, 97---130 1991

Digital Library

[16]

Pnueli, A.: The Temporal Logic of Programs. In: SFCS, pp. 46---57. IEEE, Wash., DC 1977

Digital Library

[17]

Roşu, G., Havelund, K.: Rewriting-based techniques for runtime verification. Automated Software Engg. 122, 151---197 2005

Digital Library

[18]

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

[19]

Stirling, C., Walker, D.: Local model-checking in the modal mu-calculus. TCS 89, 161---177 1991

Digital Library

[20]

Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press 2000

Digital Library

Cited By

Ziemek RPiribauer JFunke FJantsch SBaier C(2022)Probabilistic causes in Markov chainsInnovations in Systems and Software Engineering10.1007/s11334-022-00452-818:3(347-367)Online publication date: 1-Sep-2022
https://dl.acm.org/doi/10.1007/s11334-022-00452-8
Baier CFunke FJantsch SPiribauer JZiemek R(2021)Probabilistic Causes in Markov ChainsAutomated Technology for Verification and Analysis10.1007/978-3-030-88885-5_14(205-221)Online publication date: 18-Oct-2021
https://dl.acm.org/doi/10.1007/978-3-030-88885-5_14
Aceto LAchilleos AFrancalanza AIngólfsdóttir ALehtinen K(2019)Adventures in monitorability: from branching to linear time and back againProceedings of the ACM on Programming Languages10.1145/32903653:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290365
Show More Cited By

An LTL Proof System for Runtime Verification
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
2. Theory of computation
  1. Logic

Recommendations

Runtime Verification for LTL and TLTL

This article studies runtime verification of properties expressed either in lineartime temporal logic (LTL) or timed lineartime temporal logic (TLTL). It classifies runtime verification in identifying its distinguishing features to model checking and ...
Comparing LTL Semantics for Runtime Verification

When monitoring a system w.r.t. a property defined in a temporal logic such as LTL, a major concern is to settle with an adequate interpretation of observable system events; that is, models of temporal logic formulae are usually infinite words of events,...
A lightweight LTL runtime verification tool for java
OOPSLA '04: Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications

Runtime verification is a special form of runtime testing, employing formal methods and languages. In this work, we utilize next-time free linear-time temporal logic (LTL\textbackslash X) as formal framework. The discipline serves the purpose of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 9035

April 2015

692 pages

ISBN:9783662466803

Editors:
Christel Baier
Technical University of Dresden, Dresden, Germany
,
Cesare Tinelli
The University of Iowa, Iowa City, USA

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 11 April 2015

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ziemek RPiribauer JFunke FJantsch SBaier C(2022)Probabilistic causes in Markov chainsInnovations in Systems and Software Engineering10.1007/s11334-022-00452-818:3(347-367)Online publication date: 1-Sep-2022
https://dl.acm.org/doi/10.1007/s11334-022-00452-8
Baier CFunke FJantsch SPiribauer JZiemek R(2021)Probabilistic Causes in Markov ChainsAutomated Technology for Verification and Analysis10.1007/978-3-030-88885-5_14(205-221)Online publication date: 18-Oct-2021
https://dl.acm.org/doi/10.1007/978-3-030-88885-5_14
Aceto LAchilleos AFrancalanza AIngólfsdóttir ALehtinen K(2019)Adventures in monitorability: from branching to linear time and back againProceedings of the ACM on Programming Languages10.1145/32903653:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290365
Aceto LAchilleos AFrancalanza AIngólfsdóttir ALehtinen K(2019)An Operational Guide to MonitorabilitySoftware Engineering and Formal Methods10.1007/978-3-030-30446-1_23(433-453)Online publication date: 18-Sep-2019
https://dl.acm.org/doi/10.1007/978-3-030-30446-1_23
Francalanza AAceto LIngolfsdottir A(2017)Monitorability for the Hennessy---Milner logic with recursionFormal Methods in System Design10.1007/s10703-017-0273-z51:1(87-116)Online publication date: 1-Aug-2017
https://dl.acm.org/doi/10.1007/s10703-017-0273-z

View Options

View options

Media

Figures

Other

Tables

View Table of Contents