Luca Aceto
Skip Abstract Section
Skip Supplemental Material SectionAbstract
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.
Supplemental Material
- 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.Google Scholar
- 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.Google Scholar
- 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.10212Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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. Google ScholarDigital Library
- 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.Google Scholar
- Bowen Alpern and Fred B. Schneider. 1985. Defining Liveness. Inform. Process. Lett. 21, 4 (1985), 181–185.Google ScholarCross Ref
- 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.Google Scholar
- Duncan Paul Attard and Adrian Francalanza. 2016. A Monitoring Tool for a Branching-Time Logic. Springer International Publishing, Cham, 473–481.Google Scholar
- Christel Baier, Joost-Pieter Katoen, and Kim Guldstrand Larsen. 2008. Principles of model checking. MIT press. Google ScholarDigital Library
- Howard Barringer, Allen Goldberg, Klaus Havelund, and Koushik Sen. 2004. Rule-based runtime verification. In VMCAI, Vol. 2937. Springer, 44–57.Google ScholarCross Ref
- Ezio Bartocci, Yliès Falcone, Adrian Francalanza, and Giles Reger. 2018. Introduction to Runtime Verification. Springer, 1–33.Google Scholar
- Andreas Bauer, Martin Leucker, and Christian Schallhart. 2010. Comparing LTL semantics for runtime verification. Logic and Computation 20, 3 (2010), 651–674. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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-01088117Google Scholar
- 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.Google Scholar
- Ashok K. Chandra, Dexter C. Kozen, and Larry J. Stockmeyer. 1981. Alternation. Journal of the ACM 28, 1 (jan 1981), 114–133. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Clare Cini and Adrian Francalanza. 2015. An LTL Proof System for Runtime Verification. In TACAS, Vol. 9035. Springer, 581–595. Google ScholarDigital Library
- Edmund M Clarke, Orna Grumberg, and Doron Peled. 1999. Model Checking. MIT press. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Volker Diekert and Martin Leucker. 2014. Topology, monitorable properties and runtime verification. Theoretical Computer Science 537 (2014), 29–41.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- Doron Drusinsky. 2003. Monitoring temporal rules combined with time series. In CAV, Vol. 3. Springer, 114–118.Google Scholar
- 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.pdfGoogle Scholar
- Yliès Falcone, Jean-Claude Fernandez, and Laurent Mounier. 2012a. What can you verify and enforce at runtime? STTT 14, 3 (2012), 349–382.Google ScholarCross Ref
- 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.Google ScholarCross Ref
- 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.Google ScholarCross Ref
- Bernd Finkbeiner and Henny Sipma. 2004. Checking finite traces using alternating automata. Formal Methods in System Design 24, 2 (2004), 101–127. Google ScholarDigital Library
- Adrian Francalanza. 2016. A Theory of Monitors. In FoSSaCS (LNCS), Vol. 9634. 145–161.Google Scholar
- Adrian Francalanza. 2017. Consistently-Detecting Monitors. In CONCUR (LIPIcs), Vol. 85. Schloss Dagstuhl, Dagstuhl, Germany, 8:1–8:19.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- Adrian Francalanza, Luca Aceto, and Anna Ingolfsdottir. 2017b. Monitorability for the Hennessy–Milner logic with recursion. FMSD (2017), 1–30. Google ScholarDigital Library
- Adrian Francalanza and Aldrin Seychell. 2015. Synthesising correct concurrent runtime monitors. Formal Methods in System Design 46, 3 (2015), 226–261. Google ScholarDigital Library
- 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 .Google Scholar
- Klaus Havelund and Grigore Rosu. 2002. Synthesizing monitors for safety properties. In TACAS, Vol. 2. Springer, 342–356. Google ScholarDigital Library
- Matthew Hennessy and Robin Milner. 1985. Algebraic Laws for Nondeterminism and Concurrency. J. ACM 32, 1 (1985), 137–161. Google ScholarDigital Library
- Robert M. Keller. 1976. Formal Verification of Parallel Programs. Commun. ACM 19, 7 (1976), 371–384. Google ScholarDigital Library
- Dexter C. Kozen. 1983. Results on the Propositional µ-calculus. Theoretical Computer Science 27 (1983), 333–354.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Kim G. Larsen. 1990. Proof Systems for Satisfiability in Hennessy-Milner Logic with recursion. Theoretical Computer Science (TCS) 72, 2 (1990), 265 – 288. Google ScholarDigital Library
- Zohar Manna and Amir Pnueli. 1991. Completing the Temporal Picture. TCS 83, 1 (1991), 97–130. Google ScholarDigital Library
- Nicolas Markey and Philippe Schnoebelen. 2006. Mu-calculus path checking. Inform. Process. Lett. 97, 6 (March 2006), 225–230. Google ScholarDigital Library
- R. Milner. 1989. Communication and Concurrency. Prentice-Hall. Google ScholarDigital Library
- A. Pnueli and A. Zaks. 2006. PSL Model Checking and Run-time Verification via Testers. In FM. Springer, 573–586. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- Fred B. Schneider. 1997. On Concurrent Programming. Springer-Verlag. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Thomas Wilke. 2001. Alternating Tree Automata, Parity Games, and Modal m-Calculus. Bulletin of the Belgian Mathematical Society Simon Stevin 8, 2 (2001), 359.Google ScholarCross Ref
Index Terms
- Adventures in monitorability: from branching to linear time and back again
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 intelligenceWe 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