Document Open Access Logo

Monitoring for Silent Actions

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

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2017.7.pdf
  • Filesize: 0.51 MB
  • 14 pages

Document Identifiers

Author Details

Luca Aceto
Antonis Achilleos
Adrian Francalanza
Anna Ingólfsdóttir

Cite As Get BibTex

Luca Aceto, Antonis Achilleos, Adrian Francalanza, and Anna Ingólfsdóttir. Monitoring for Silent Actions. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 7:1-7:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.FSTTCS.2017.7

Abstract

Silent actions are an essential mechanism for system modelling and specification. They are used to abstractly report the occurrence of computation steps without divulging their precise details, thereby enabling the description of important aspects such as the branching structure of a system.  Yet, their use rarely features in specification logics used in runtime verification.  We study monitorability aspects of a branching-time logic that employs silent actions, identifying which formulas are monitorable for a number of instrumentation setups. We also consider defective instrumentation setups that imprecisely report silent events, and establish monitorability results for tolerating these imperfections.

Subject Classification

Keywords
  • Runtime Verification
  • Monitorability
  • Hennessy-Milner Logic with Recursion
  • Silent Actions

Metrics

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

References

  1. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Sævar Örn Kjartansson. Determinizing monitors for HML with recursion. arXiv preprint arXiv:1611.10212, 2016. Google Scholar
  2. 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, Marne-la-Vallée, France, June 27-30, 2017, Proceedings, volume 10329 of Lecture Notes in Computer Science, pages 1-13. Springer, 2017. URL: http://dx.doi.org/10.1007/978-3-319-60134-2_1.
  3. Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen, and Jiri Srba. Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, New York, NY, USA, 2007. URL: http://dx.doi.org/10.1017/cbo9780511814105.
  4. S. Arun-Kumar and Matthew Hennessy. An efficiency preorder for processes. Acta Inf., 29(8):737-760, 1992. URL: http://dx.doi.org/10.1007/BF01191894.
  5. David A. Basin, Felix Klaedtke, Srdjan Marinovic, and Eugen Zalinescu. Monitoring compliance policies over incomplete and disagreeing logs. In Shaz Qadeer and Serdar Tasiran, editors, Runtime Verification, Third International Conference, RV 2012, Istanbul, Turkey, September 25-28, 2012, Revised Selected Papers, volume 7687 of Lecture Notes in Computer Science, pages 151-167. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-35632-2_17.
  6. David A. Basin, Felix Klaedtke, and Eugen Zalinescu. Failure-aware runtime verification of distributed systems. In Prahladh Harsha and G. Ramalingam, editors, 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2015, December 16-18, 2015, Bangalore, India, volume 45 of LIPIcs, pages 590-603. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2015.590.
  7. Laura Bocchi, Tzu-Chun Chen, Romain Demangeon, Kohei Honda, and Nobuko Yoshida. Monitoring networks through multiparty session types. Theor. Comput. Sci., 669:33-58, 2017. URL: http://dx.doi.org/10.1016/j.tcs.2017.02.009.
  8. Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. Model Checking. MIT Press, Cambridge, MA, USA, 1999. Google Scholar
  9. Matthew B. Dwyer, Madeline Diep, and Sebastian G. Elbaum. Reducing the cost of path property monitoring through sampling. In 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008), 15-19 September 2008, L'Aquila, Italy, pages 228-237. IEEE Computer Society, 2008. URL: http://dx.doi.org/10.1109/ASE.2008.33.
  10. Adrian Francalanza. A theory of monitors - (extended abstract). In Bart Jacobs and Christof Löding, editors, Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9634 of Lecture Notes in Computer Science, pages 145-161. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-662-49630-5_9.
  11. Adrian Francalanza. Consistently-detecting monitors. In Roland Meyer and Uwe Nestmann, editors, 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany, volume 85 of LIPIcs, pages 8:1-8:19. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2017.8.
  12. 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, Seattle, WA, USA, September 13-16, 2017, Proceedings, volume 10548 of Lecture Notes in Computer Science, pages 8-29. Springer, 2017. URL: http://dx.doi.org/10.1007/978-3-319-67531-2_2.
  13. Adrian Francalanza, Luca Aceto, and Anna Ingólfsdóttir. On verifying hennessy-milner logic with recursion at runtime. In Ezio Bartocci and Rupak Majumdar, editors, Runtime Verification - 6th International Conference, RV 2015 Vienna, Austria, September 22-25, 2015. Proceedings, volume 9333 of Lecture Notes in Computer Science, pages 71-86. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-23820-3_5.
  14. 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: http://dx.doi.org/10.1007/s10703-017-0273-z.
  15. Adrian Francalanza and Aldrin Seychell. Synthesising correct concurrent runtime monitors. Formal Methods in System Design, 46(3):226-261, 2015. URL: http://dx.doi.org/10.1007/s10703-014-0217-9.
  16. Matthew Hennessy. Algebraic Theory of Processes. Foundations of Computing. MIT Press, 1988. Google Scholar
  17. Dexter Kozen. Results on the propositional mu-calculus. Theor. Comput. Sci., 27:333-354, 1983. URL: http://dx.doi.org/10.1016/0304-3975(82)90125-6.
  18. Kim Guldstrand Larsen. Proof systems for satisfiability in hennessy-milner logic with recursion. Theor. Comput. Sci., 72(2&3):265-288, 1990. URL: http://dx.doi.org/10.1016/0304-3975(90)90038-J.
  19. Martin Leucker and Christian Schallhart. A brief account of runtime verification. J. Log. Algebr. Program., 78(5):293-303, 2009. URL: http://dx.doi.org/10.1016/j.jlap.2008.08.004.
  20. Robin Milner. Communication and Concurrency. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1989. Google Scholar
  21. Jinghao Shi, Shuvendu K. Lahiri, Ranveer Chandra, and Geoffrey Challen. Wireless protocol validation under uncertainty. In Yliès Falcone and César Sánchez, editors, Runtime Verification - 16th International Conference, RV 2016, Madrid, Spain, September 23-30, 2016, Proceedings, volume 10012 of Lecture Notes in Computer Science, pages 351-367. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-46982-9_22.
  22. Yoriyuki Yamagata, Cyrille Artho, Masami Hagiya, Jun Inoue, Lei Ma, Yoshinori Tanabe, and Mitsuharu Yamamoto. Runtime monitoring for concurrent systems. In Yliès Falcone and César Sánchez, editors, Runtime Verification - 16th International Conference, RV 2016, Madrid, Spain, September 23-30, 2016, Proceedings, volume 10012 of Lecture Notes in Computer Science, pages 386-403. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-46982-9_24.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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