Document Open Access Logo

The Best a Monitor Can Do

Authors Luca Aceto , Antonis Achilleos , Adrian Francalanza , Anna Ingólfsdóttir , Karoliina Lehtinen

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2021.7.pdf
  • Filesize: 0.7 MB
  • 23 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Software and its engineering → Formal software verification
Keywords
  • monitorability
  • branching-time logics
  • runtime verification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Existing notions of monitorability for branching-time properties are fairly restrictive. This, in turn, impacts the ability to incorporate prior knowledge about the system under scrutiny - which corresponds to a branching-time property - into the runtime analysis. We propose a definition of optimal monitors that verify the best monitorable under- or over-approximation of a specification, regardless of its monitorability status. Optimal monitors can be obtained for arbitrary branching-time properties by synthesising a sound and complete monitor for their strongest monitorable consequence. We show that the strongest monitorable consequence of specifications expressed in Hennessy-Milner logic with recursion is itself expressible in this logic, and present a procedure to find it. Our procedure enables prior knowledge to be optimally incorporated into runtime monitors.

Cite As Get BibTex

Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. The Best a Monitor Can Do. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 7:1-7:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.CSL.2021.7

Author Details

Luca Aceto
  • Reykjavik University, Iceland
  • Gran Sasso Science Institute, L'Aquila, Italy
Antonis Achilleos
  • Reykjavik University, Iceland
Adrian Francalanza
  • University of Malta, Malta
Anna Ingólfsdóttir
  • Reykjavik University, Iceland
Karoliina Lehtinen
  • University of Liverpool, UK

Funding

Research supported by the Icelandic Research Fund projects "Theoretical Foundations for Monitorability" (No:163406-051) and "Epistemic Logic for Distributed Runtime Monitoring" (No:184940-051), the MIUR project PRIN 2017FTXR7S IT MATTERS, project BehAPI, funded by the EU H2020 RISE programme under the Marie Skłodowska-Curie grant agreement No:778233, and project FouCo, funded by EU H2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No:892704.

References

  1. Luca Aceto, Antonis Achilleos, Adrian Francalanza, and Anna Ingólfsdóttir. Monitoring for silent actions. In Satya Lokam and R. Ramanujam, editors, FSTTCS, volume 93 of LIPIcs, pages 7:1-7:14, Dagstuhl, Germany, 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Google Scholar
  2. Luca Aceto, Antonis Achilleos, Adrian Francalanza, and Anna Ingólfsdóttir. A framework for parameterized monitorability. In Christel Baier and Ugo Dal Lago, editors, Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, volume 10803 of Lecture Notes in Computer Science, pages 203-220. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89366-2_11.
  3. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Sævar Örn Kjartansson. On the complexity of determinizing monitors. In Arnaud Carayol and Cyril Nicaud, editors, Implementation and Application of Automata - 22nd International Conference, CIAA 2017, volume 10329 of Lecture Notes in Computer Science, pages 1-13. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-60134-2_1.
  4. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. Adventures in monitorability: From branching to linear time and back again. Proceedings of the ACM on Programming Languages, 3(POPL):52:1-52:29, 2019. URL: https://dl.acm.org/citation.cfm?id=3290365.
  5. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. An operational guide to monitorability. In Software Engineering and Formal Methods - 17th International Conference, SEFM 2019, Oslo, Norway, September 18-20, 2019, Proceedings, volume 11724 of LNCS, pages 433-453. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-30446-1_23.
  6. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Sævar Örn Kjartansson. Determinizing monitors for HML with recursion. Journal of Logical and Algebraic Methods in Programming, 111:100515, February 2020. URL: https://doi.org/10.1016/j.jlamp.2019.100515.
  7. Bowen Alpern and Fred B Schneider. Defining liveness. Information processing letters, 21(4):181-185, 1985. Google Scholar
  8. Duncan Paul Attard, Ian Cassar, Adrian Francalanza, Luca Aceto, and Anna Ingolfsdottir. Behavioural Types: from Theory to Tools, chapter A Runtime Monitoring Tool for Actor-Based Systems, pages 49-74. River Publishers, 2017. Google Scholar
  9. Duncan Paul Attard and Adrian Francalanza. A monitoring tool for a branching-time logic. In Yliès Falcone and César Sánchez, editors, Runtime Verification - 16th International Conference, RV 2016, volume 10012 of Lecture Notes in Computer Science, pages 473-481. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-46982-9_31.
  10. Christel Baier, Joost-Pieter Katoen, and Kim Guldstrand Larsen. Principles of model checking. MIT press, 2008. Google Scholar
  11. Ezio Bartocci, Yliès Falcone, Adrian Francalanza, and Giles Reger. Introduction to Runtime Verification, pages 1-33. Springer International Publishing, Cham, 2018. URL: https://doi.org/10.1007/978-3-319-75632-5_1.
  12. Andreas Bauer, Martin Leucker, and Christian Schallhart. The good, the bad, and the ugly, but how ugly is ugly? In Oleg Sokolsky and Serdar Taşıran, editors, Runtime Verification, pages 126-138, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. Google Scholar
  13. Julian Bradfield and Colin Stirling. Chapter 4 - Modal logics and mu-calculi: An introduction. In J.A. Bergstra, A. Ponse, and S.A. Smolka, editors, Handbook of Process Algebra, pages 293-330. Elsevier Science, Amsterdam, 2001. URL: https://doi.org/10.1016/B978-044482830-9/50022-9.
  14. Julian Bradfield and Colin Stirling. Modal μ-calculi. Studies in Logic and Practical Reasoning, 3:721-756, 2007. Google Scholar
  15. Julian Bradfield and Igor Walukiewicz. The mu-calculus and Model Checking, pages 871-919. Springer, May 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_26.
  16. Ashok K. Chandra, Dexter C. Kozen, and Larry J. Stockmeyer. Alternation. Journal of the ACM, 28(1):114-133, January 1981. URL: https://doi.org/10.1145/322234.322243.
  17. Alessandro Cimatti, Chun Tian, and Stefano Tonetta. Assumption-based runtime verification with partial observability and resets. In International Conference on Runtime Verification, pages 165-184. Springer, 2019. Google Scholar
  18. Edmund M Clarke, Orna Grumberg, and Doron Peled. Model Checking. MIT press, 1999. Google Scholar
  19. Volker Diekert and Martin Leucker. Topology, monitorable properties and runtime verification. Theoretical Computer Science, 537:29-41, 2014. Theoretical Aspects of Computing (ICTAC 2011). URL: https://doi.org/10.1016/j.tcs.2014.02.052.
  20. E Allen Emerson and Charanjit S Jutla. Tree automata, mu-calculus and determinacy. In FoCS, volume 91, pages 368-377. Citeseer, 1991. Google Scholar
  21. Yliès Falcone, Jean-Claude Fernandez, and Laurent Mounier. What can you verify and enforce at runtime? International Journal on Software Tools for Technology Transfer, 14(3):349-382, 2012. URL: https://doi.org/10.1007/s10009-011-0196-8.
  22. Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, and Leander Tentrup. Monitoring hyperproperties. Formal Methods in System Design, 54(3):336-363, 2019. Google Scholar
  23. Adrian Francalanza. A Theory of Monitors (Extended Abstract). In FoSSaCS, volume 9634 of LNCS, pages 145-161, 2016. Google Scholar
  24. Adrian Francalanza. Consistently-detecting monitors. In Roland Meyer and Uwe Nestmann, editors, 28superscriptth International Conference on Concurrency Theory (CONCUR 2017), volume 85 of LIPIcs, pages 8:1-8:19, Dagstuhl, Germany, 2017. Schloss Dagstuhl. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.8.
  25. Adrian Francalanza, Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Ian Cassar, Dario Della Monica, and Anna Ingólfsdóttir. A foundation for runtime monitoring. In Shuvendu K. Lahiri and Giles Reger, editors, Runtime Verification - 17th International Conference, RV 2017, volume 10548 of Lecture Notes in Computer Science, pages 8-29. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-67531-2_2.
  26. Adrian Francalanza, Luca Aceto, and Anna Ingólfsdóttir. Monitorability for the Hennessy-Milner logic with recursion. Formal Methods in System Design, 51(1):87-116, 2017. URL: https://doi.org/10.1007/s10703-017-0273-z.
  27. M.C.W. Geilen. On the construction of monitors for temporal logic properties. Electronic Notes in Theoretical Computer Science, 55(2):181-199, 2001. RV'2001, Runtime Verification (in connection with CAV '01). URL: https://doi.org/10.1016/S1571-0661(04)00252-X.
  28. Klaus Havelund and Doron Peled. Runtime Verification: From Propositional to First-Order Temporal Logic. In Runtime Verification - 18th International Conference, RV 2018, Limassol, Cyprus, November 10-13, 2018, Proceedings, volume 11237 of LNCS, pages 90-112. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-03769-7_7.
  29. Klaus Havelund and Grigore Rosu. Synthesizing monitors for safety properties. In TACAS, volume 2, pages 342-356. Springer, 2002. Google Scholar
  30. Thomas A Henzinger and N Ege Saraç. Monitorability under assumptions. In International Conference on Runtime Verification, pages 3-18. Springer, 2020. Google Scholar
  31. David Janin and Igor Walukiewicz. On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In International Conference on Concurrency Theory, pages 263-277. Springer, 1996. Google Scholar
  32. David Janin and Igor Walukiewicz. On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In CONCUR quotesingle96: Concurrency Theory, pages 263-277. Springer Berlin Heidelberg, 1996. URL: https://doi.org/10.1007/3-540-61604-7_60.
  33. Robert M. Keller. Formal verification of parallel programs. Commun. ACM, 19(7):371-384, 1976. URL: https://doi.org/10.1145/360248.360251.
  34. Dexter C. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333-354, 1983. Google Scholar
  35. Orna Kupferman and Moshe Y. Vardi. Model checking of safety properties. Formal Methods in System Design, 19(3):291-314, 2001. Google Scholar
  36. Orna Kupferman, Moshe Y Vardi, and Pierre Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2):312-360, 2000. Google Scholar
  37. Kim G. Larsen. Proof Systems for Satisfiability in Hennessy-Milner Logic with recursion. Theoretical Computer Science, 72(2):265-288, 1990. URL: https://doi.org/10.1016/0304-3975(90)90038-J.
  38. Martin Leucker. Sliding between model checking and runtime verification. In International Conference on Runtime Verification, pages 82-87. Springer, 2012. Google Scholar
  39. Martin Leucker, César Sánchez, Torben Scheffel, Malte Schmitz, and Daniel Thoma. Runtime verification for timed event streams with partial information. In Bernd Finkbeiner and Leonardo Mariani, editors, Runtime Verification - 19th International Conference, RV 2019, Porto, Portugal, October 8-11, 2019, Proceedings, volume 11757 of LNCS, pages 273-291. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-32079-9_16.
  40. Grgur Petric Maretić, Mohammad Torabi Dashti, and David Basin. Ltl is closed under topological closure. Information Processing Letters, 114(8):408-413, 2014. Google Scholar
  41. Grgur Petric Maretić, Mohammad Torabi Dashti, and David Basin. Ltl is closed under topological closure. Information Processing Letters, 114(8):408-413, 2014. Google Scholar
  42. Tiziana Margaria, A. Prasad Sistla, Bernhard Steffen, and Lenore D. Zuck. Taming interface specifications. In Martín Abadi and Luca de Alfaro, editors, CONCUR 2005 - Concurrency Theory, pages 548-561, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  43. R Milner. A calculus of communicating systems. Lecture Notes in Comput. Sci. 92, 1980. Google Scholar
  44. Doron Peled and Klaus Havelund. Refining the safety-liveness classification of temporal properties according to monitorability. In Models, Mindsets, Meta: The What, the How, and the Why Not?, pages 218-234. Springer, 2019. Google Scholar
  45. A Peuli and Lenore Zuck. In and out of temporal logic. In [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, pages 124-135. IEEE, 1993. Google Scholar
  46. Fred B. Schneider. Enforceable security policies. ACM Transactions on Information and System Security, 3(1):30-50, 2000. Google Scholar
  47. A Prasad Sistla and Abhigna R Srinivas. Monitoring temporal properties of stochastic systems. In International Workshop on Verification, Model Checking, and Abstract Interpretation, pages 294-308. Springer, 2008. Google Scholar
  48. A Prasad Sistla, Min Zhou, and Lenore D Zuck. Monitoring off-the-shelf components. In International Workshop on Verification, Model Checking, and Abstract Interpretation, pages 222-236. Springer, 2006. Google Scholar
  49. Sandro Stucki, César Sánchez, Gerardo Schneider, and Borzoo Bonakdarpour. Gray-box monitoring of hyperproperties. In Formal Methods-The Next 30 Years: Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings, volume 11800, page 406. Springer Nature, 2019. Google Scholar
  50. Mahesh Viswanathan and Moonzoo Kim. Foundations for the run-time monitoring of reactive systems - fundamentals of the MaC language. In Zhiming Liu and Keijiro Araki, editors, Theoretical Aspects of Computing - ICTAC 2004, First International Colloquium, volume 3407 of Lecture Notes in Computer Science, pages 543-556. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-31862-0_38.
  51. Igor Walukiewicz. Completeness of Kozenquotesingles axiomatisation of the propositional μ-calculus. Information and Computation, 157(1-2):142-182, February 2000. URL: https://doi.org/10.1006/inco.1999.2836.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact