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

research-article

Open access

Adventures in monitorability: from branching to linear time and back again

Authors:

Antonis Achilleos,

Adrian Francalanza,

Anna Ingólfsdóttir,

Karoliina LehtinenAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 3, Issue POPL

Article No.: 52, Pages 1 - 29

https://doi.org/10.1145/3290365

Published: 02 January 2019 Publication History

Abstract

This paper establishes a comprehensive theory of runtime monitorability for Hennessy-Milner logic with recursion, a very expressive variant of the modal µ-calculus. It investigates the monitorability of that logic with a linear-time semantics and then compares the obtained results with ones that were previously presented in the literature for a branching-time setting. Our work establishes an expressiveness hierarchy of monitorable fragments of Hennessy-Milner logic with recursion in a linear-time setting and exactly identifies what kinds of guarantees can be given using runtime monitors for each fragment in the hierarchy. Each fragment is shown to be complete, in the sense that it can express all properties that can be monitored under the corresponding guarantees. The study is carried out using a principled approach to monitoring that connects the semantics of the logic and the operational semantics of monitors. The proposed framework supports the automatic, compositional synthesis of correct monitors from monitorable properties.

Supplementary Material

WEBM File (a52-aceto.webm)

Download
104.60 MB

References

[1]

Luca Aceto, Antonis Achilleos, Adrian Francalanza, and Anna Ingólfsdóttir. 2017a. Monitoring for silent actions. In FSTTCS (LIPIcs), Satya Lokam and R. Ramanujam (Eds.), Vol. 93. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 7:1–7:14.

[2]

Luca Aceto, Antonis Achilleos, Adrian Francalanza, and Anna Ingólfsdóttir. 2018a. A Framework for Parametrized Monitorability. In FOSSACS (Lecture Notes in Computer Science), Vol. 10803. Springer, 203–220.

[3]

Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Sævar Örn Kjartansson. 2016. Determinizing Monitors for HML with Recursion. CoRR abs/1611.10212 (2016). arXiv: 1611.10212 http://arxiv.org/abs/1611.10212

[4]

Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Sævar Örn Kjartansson. 2017b. On the Complexity of Determinizing Monitors. In Implementation and Application of Automata. Springer International Publishing, 1–13.

[5]

Luca Aceto, Ian Cassar, Adrian Francalanza, and Anna Ingólfsdóttir. 2018b. On Runtime Enforcement via Suppressions. In CONCUR (LIPIcs), Vol. 118. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 34:1–34:17.

[6]

Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen, and Jiri Srba. 2007. Reactive Systems: Modelling, Specification and Verification . Cambridge Univ. Press, New York, NY, USA.

Digital Library

[7]

Antonis Achilleos. 2016. Modal Logics with Hard Diamond-Free Fragments. In Logical Foundations of Computer Science, Sergei Artemov and Anil Nerode (Eds.). Springer International Publishing, Cham, 1–13.

[8]

Bowen Alpern and Fred B. Schneider. 1985. Defining Liveness. Inform. Process. Lett. 21, 4 (1985), 181–185.

[9]

Duncan Paul Attard, Ian Cassar, Adrian Francalanza, Luca Aceto, and Anna Ingolfsdottir. 2017. Behavioural Types: from Theory to Tools . River Publishers, Chapter A Runtime Monitoring Tool for Actor-Based Systems, 49–74.

[10]

Duncan Paul Attard and Adrian Francalanza. 2016. A Monitoring Tool for a Branching-Time Logic. Springer International Publishing, Cham, 473–481.

[11]

Christel Baier, Joost-Pieter Katoen, and Kim Guldstrand Larsen. 2008. Principles of model checking. MIT press.

Digital Library

[12]

Howard Barringer, Allen Goldberg, Klaus Havelund, and Koushik Sen. 2004. Rule-based runtime verification. In VMCAI, Vol. 2937. Springer, 44–57.

[13]

Ezio Bartocci, Yliès Falcone, Adrian Francalanza, and Giles Reger. 2018. Introduction to Runtime Verification. Springer, 1–33.

[14]

Andreas Bauer, Martin Leucker, and Christian Schallhart. 2010. Comparing LTL semantics for runtime verification. Logic and Computation 20, 3 (2010), 651–674.

Digital Library

[15]

Andreas Bauer, Martin Leucker, and Christian Schallhart. 2011. Runtime verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology (TOSEM) 20, 4 (2011), 14.

Digital Library

[16]

Nathalie Bertrand, Serge Haddad, and Engel Lefaucheux. 2014. Foundation of Diagnosis and Predictability in Probabilistic Systems. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’14). New Delhi, India. https://hal.inria.fr/hal-01088117

[17]

Julian Bradfield and Colin Stirling. 2001. CHAPTER 4 - Modal Logics and mu-Calculi: An Introduction. In Handbook of Process Algebra, J.A. Bergstra, A. Ponse, and S.A. Smolka (Eds.). Elsevier Science, Amsterdam, 293 – 330.

[18]

Ashok K. Chandra, Dexter C. Kozen, and Larry J. Stockmeyer. 1981. Alternation. Journal of the ACM 28, 1 (jan 1981), 114–133.

Digital Library

[19]

Edward Chang, Zohar Manna, and Amir Pnueli. 1992. Characterization of Temporal Property Classes. In Automata, Languages and Properties (LNCS), Vol. 623. Springer-Verlag, 474–486.

Digital Library

[20]

Clare Cini and Adrian Francalanza. 2015. An LTL Proof System for Runtime Verification. In TACAS, Vol. 9035. Springer, 581–595.

Digital Library

[21]

Edmund M Clarke, Orna Grumberg, and Doron Peled. 1999. Model Checking. MIT press.

Digital Library

[22]

Ben d’Angelo, Sriram Sankaranarayanan, César Sánchez, Will Robinson, Bernd Finkbeiner, Henny B Sipma, Sandeep Mehrotra, and Zohar Manna. 2005. LOLA: Runtime monitoring of synchronous systems. In Temporal Representation and Reasoning, 2005. TIME 2005. 12th International Symposium on . IEEE, 166–174.

Digital Library

[23]

Rocco De Nicola and Frits Vaandrager. 1990. Action versus state based logics for transition systems. In Semantics of Systems of Concurrent Processes, Irène Guessarian (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 407–419.

Digital Library

[24]

Volker Diekert and Martin Leucker. 2014. Topology, monitorable properties and runtime verification. Theoretical Computer Science 537 (2014), 29–41.

[25]

Volker Diekert, Anca Muscholl, and Igor Walukiewicz. 2015. A Note on Monitors and Büchi Automata. In Theoretical Aspects of Computing - ICTAC 2015, 12th International Colloquium (Lecture Notes in Computer Science), Martin Leucker, Camilo Rueda, and Frank D. Valencia (Eds.), Vol. 9399. Springer, 39–57.

Digital Library

[26]

Doron Drusinsky. 2003. Monitoring temporal rules combined with time series. In CAV, Vol. 3. Springer, 114–118.

[27]

Sonali Dutta, Moshe Y. Vardi, and Deian Tabakov. 2014. CHIMP: A Tool for Assertion-Based Dynamic Verification of SystemC Models. In Proceedings of the Second International Workshop on Design and Implementation of Formal Tools and Systems (CEUR Workshop Proceedings), Malay K. Ganai and Alper Sen (Eds.), Vol. 1130. CEUR-WS.org. http: //ceur-ws.org/Vol-1130/paper_8.pdf

[28]

Yliès Falcone, Jean-Claude Fernandez, and Laurent Mounier. 2012a. What can you verify and enforce at runtime? STTT 14, 3 (2012), 349–382.

[29]

Yliès Falcone, Jean-Claude Fernandez, and Laurent Mounier. 2012b. What can you verify and enforce at runtime? International Journal on Software Tools for Technology Transfer 14, 3 (01 Jun 2012), 349–382.

[30]

A. Fellah, H. Jürgensen, and S. Yu. 1990. Constructions for alternating finite automata∗. International Journal of Computer Mathematics 35, 1-4 (jan 1990), 117–132.

[31]

Bernd Finkbeiner and Henny Sipma. 2004. Checking finite traces using alternating automata. Formal Methods in System Design 24, 2 (2004), 101–127.

Digital Library

[32]

Adrian Francalanza. 2016. A Theory of Monitors. In FoSSaCS (LNCS), Vol. 9634. 145–161.

[33]

Adrian Francalanza. 2017. Consistently-Detecting Monitors. In CONCUR (LIPIcs), Vol. 85. Schloss Dagstuhl, Dagstuhl, Germany, 8:1–8:19.

[34]

Adrian Francalanza, Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Ian Cassar, Dario Della Monica, and Anna Ingólfsdóttir. 2017a. A Foundation for Runtime Monitoring. In RV. 8–29.

[35]

Adrian Francalanza, Luca Aceto, and Anna Ingólfsdóttir. 2015. On Verifying Hennessy-Milner Logic with Recursion at Runtime. In RV (LNCS), Vol. 9333. 71–86.

[36]

Adrian Francalanza, Luca Aceto, and Anna Ingolfsdottir. 2017b. Monitorability for the Hennessy–Milner logic with recursion. FMSD (2017), 1–30.

Digital Library

[37]

Adrian Francalanza and Aldrin Seychell. 2015. Synthesising correct concurrent runtime monitors. Formal Methods in System Design 46, 3 (2015), 226–261.

Digital Library

[38]

Dimitra Giannakopoulou and Klaus Havelund. 2001. Runtime analysis of linear temporal logic specifications. In Proceedings of the 16th IEEE International Conference on Automated Software Engineering, San Diego, California .

[39]

Klaus Havelund and Grigore Rosu. 2002. Synthesizing monitors for safety properties. In TACAS, Vol. 2. Springer, 342–356.

Digital Library

[40]

Matthew Hennessy and Robin Milner. 1985. Algebraic Laws for Nondeterminism and Concurrency. J. ACM 32, 1 (1985), 137–161.

Digital Library

[41]

Robert M. Keller. 1976. Formal Verification of Parallel Programs. Commun. ACM 19, 7 (1976), 371–384.

Digital Library

[42]

Dexter C. Kozen. 1983. Results on the Propositional µ-calculus. Theoretical Computer Science 27 (1983), 333–354.

[43]

Orna Kupferman, Moshe Y Vardi, and Pierre Wolper. 2000. An automata-theoretic approach to branching-time model checking. Journal of the ACM (JACM) 47, 2 (2000), 312–360.

Digital Library

[44]

Martin Lange. 2005. Weak Automata for the Linear Time µ-Calculus. In Verification, Model Checking, and Abstract Interpretation, Radhia Cousot (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 267–281.

Digital Library

[45]

Kim G. Larsen. 1990. Proof Systems for Satisfiability in Hennessy-Milner Logic with recursion. Theoretical Computer Science (TCS) 72, 2 (1990), 265 – 288.

Digital Library

[46]

Zohar Manna and Amir Pnueli. 1991. Completing the Temporal Picture. TCS 83, 1 (1991), 97–130.

Digital Library

[47]

Nicolas Markey and Philippe Schnoebelen. 2006. Mu-calculus path checking. Inform. Process. Lett. 97, 6 (March 2006), 225–230.

Digital Library

[48]

R. Milner. 1989. Communication and Concurrency. Prentice-Hall.

Digital Library

[49]

A. Pnueli and A. Zaks. 2006. PSL Model Checking and Run-time Verification via Testers. In FM. Springer, 573–586.

Digital Library

[50]

Meera Sampath, Raja Sengupta, Stephane Lafortune, Kasim Sinnamohideen, and Demosthenis Teneketzis. 1995. Diagnosability of discrete-event systems. IEEE Transactions on automatic control 40, 9 (1995), 1555–1575.

[51]

Fred B. Schneider. 1997. On Concurrent Programming. Springer-Verlag.

Digital Library

[52]

Deian Tabakov, Kristin Y. Rozier, and Moshe Y. Vardi. 2012. Optimized temporal monitors for SystemC. Formal Methods in System Design 41, 3 (2012), 236–268.

Digital Library

[53]

M. Y. Vardi. 1988. A Temporal Fixpoint Calculus. In Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’88) . ACM, New York, NY, USA, 250–259.

Digital Library

[54]

Mahesh Viswanathan and Moonzoo Kim. 2004. Foundations for the run-time monitoring of reactive systems–fundamentals of the MaC language. In International Colloquium on Theoretical Aspects of Computing. Springer, 543–556.

Digital Library

[55]

Thomas Wilke. 2001. Alternating Tree Automata, Parity Games, and Modal m-Calculus. Bulletin of the Belgian Mathematical Society Simon Stevin 8, 2 (2001), 359.

Cited By

Ferrando ACardoso R(2025)Towards partial monitoring: Never too early to give inScience of Computer Programming10.1016/j.scico.2024.103220240(103220)Online publication date: Feb-2025
https://doi.org/10.1016/j.scico.2024.103220
Amjad Rvan Glabbeek RO'Connor L(2024)Semantics for Linear-time Temporal Logic with Finite ObservationsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.412.4412(35-50)Online publication date: 22-Nov-2024
https://doi.org/10.4204/EPTCS.412.4
Aceto LAchilleos AAttard DExibard LFrancalanza AIngólfsdóttir A(2024)A monitoring tool for linear-time μHMLScience of Computer Programming10.1016/j.scico.2023.103031232(103031)Online publication date: Jan-2024
https://doi.org/10.1016/j.scico.2023.103031
Show More Cited By

Index Terms

Adventures in monitorability: from branching to linear time and back again
1. Theory of computation

Recommendations

Monitorability for the Hennessy---Milner logic with recursion

We study $$\mu $$μ HML, a branching-time logic with least and greatest fixpoints, from a runtime verification perspective. The logic may be used to specify properties of programs whose behaviour may be expressed as a labelled transition system. We ...
Linear time datalog and branching time logic
Logic-based artificial intelligence

We survey recent results about the relation between Datalog and temporal verification logics. Datalog is a well-known database query language relying on the logic programming paradigm. We introduce Datalog LITE, a fragment of Datalog with Well-founded ...
Constructive linear-time temporal logic: Proof systems and Kripke semantics

In this paper we study a version of constructive linear-time temporal logic (LTL) with the ''next'' temporal operator. The logic is originally due to Davies, who has shown that the proof system of the logic corresponds to a type system for binding-time ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 3, Issue POPL

January 2019

2275 pages

EISSN:2475-1421

DOI:10.1145/3302515

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 02 January 2019

Published in PACMPL Volume 3, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

34
Total Citations
View Citations
860
Total Downloads

Downloads (Last 12 months)154
Downloads (Last 6 weeks)17

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ferrando ACardoso R(2025)Towards partial monitoring: Never too early to give inScience of Computer Programming10.1016/j.scico.2024.103220240(103220)Online publication date: Feb-2025
https://doi.org/10.1016/j.scico.2024.103220
Amjad Rvan Glabbeek RO'Connor L(2024)Semantics for Linear-time Temporal Logic with Finite ObservationsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.412.4412(35-50)Online publication date: 22-Nov-2024
https://doi.org/10.4204/EPTCS.412.4
Aceto LAchilleos AAttard DExibard LFrancalanza AIngólfsdóttir A(2024)A monitoring tool for linear-time μHMLScience of Computer Programming10.1016/j.scico.2023.103031232(103031)Online publication date: Jan-2024
https://doi.org/10.1016/j.scico.2023.103031
Pitsikalis MLisitsa ATotzke P(2023)Handling of Past and Future with Phenesthe+Electronic Proceedings in Theoretical Computer Science10.4204/EPTCS.390.3390(33-49)Online publication date: 30-Sep-2023
https://doi.org/10.4204/EPTCS.390.3
Alman AMaggi FMontali MPatrizi FRivkin A(2023)Monitoring hybrid process specifications with conflict management: An automata-theoretic approachArtificial Intelligence in Medicine10.1016/j.artmed.2023.102512139(102512)Online publication date: May-2023
https://doi.org/10.1016/j.artmed.2023.102512
Aceto LCassar IFrancalanza AIngólfsdóttir A(2023)On first-order runtime enforcement of branching-time propertiesActa Informatica10.1007/s00236-023-00441-960:4(385-451)Online publication date: 1-Dec-2023
https://dl.acm.org/doi/10.1007/s00236-023-00441-9
Cimini M(2022)Lang-n-Send Extended: Sending Regular Expressions to MonitorsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.365.5365(69-84)Online publication date: 9-Aug-2022
https://doi.org/10.4204/EPTCS.365.5
Aceto LAchilleos AAnastasiadi EIngolfsdottir A(2022)Axiomatizing recursion-free, regular monitorsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2022.100778127(100778)Online publication date: Jun-2022
https://doi.org/10.1016/j.jlamp.2022.100778
Pinisetty SPradhan ARoop PTripakis S(2022)Compositional runtime enforcement revisitedFormal Methods in System Design10.1007/s10703-022-00401-y59:1-3(205-252)Online publication date: 26-Oct-2022
https://dl.acm.org/doi/10.1007/s10703-022-00401-y
Aceto LAchilleos AAnastasiadi EFrancalanza AIngólfsdóttir ALehtinen KPedersen M(2022)On Probabilistic MonitorabilityPrinciples of Systems Design10.1007/978-3-031-22337-2_16(325-342)Online publication date: 29-Dec-2022
https://doi.org/10.1007/978-3-031-22337-2_16
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents