Monitoring for silent actions. (English) Zbl 1491.68104
Lokam, Satya (ed.) et al., 37th IARCS annual conference on foundations of software technology and theoretical computer science, FSTTCS 2017, IIT Kanpur, India, December 12–14, 2017. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 93, Article 7, 14 p. (2018).
Summary: 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.
For the entire collection see [Zbl 1388.68010].
For the entire collection see [Zbl 1388.68010].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B44 | Temporal logic |
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
References:
| [1] | Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Sævar Örn Kjartansson.Determinizing monitors for HML with recursion.{\it arXiv preprint} {\it arXiv:1611.10212}, 2016. |
| [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, {\it Implementation and Application of Automata - 22nd Interna-} {\it tional Conference, CIAA 2017, Marne-la-Vallée, France, June 27-30, 2017, Proceed-} {\it ings}, volume 10329 of {\it Lecture Notes in Computer Science}, pages 1-13. Springer, 2017. doi:10.1007/978-3-319-60134-2_1. · Zbl 1489.68149 |
| [3] | Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen, and Jiri Srba. {\it Reactive Systems:} {\it Modelling, Specification and Verification}. Cambridge University Press, New York, NY, USA, 2007. doi:10.1017/cbo9780511814105. · Zbl 1141.68043 |
| [4] | S. Arun-Kumar and Matthew Hennessy. An efficiency preorder for processes. {\it Acta Inf.}, 29(8):737-760, 1992. doi:10.1007/BF01191894. · Zbl 0790.68039 |
| [5] | David A. Basin, Felix Klaedtke, Srdjan Marinovic, and Eugen Zalinescu. Monitoring com pliance policies over incomplete and disagreeing logs. In Shaz Qadeer and Serdar Tasiran, editors, {\it Runtime Verification, Third International Conference, RV 2012, Istanbul, Turkey,} {\it September 25-28, 2012, Revised Selected Papers}, volume 7687 of {\it Lecture Notes in Computer} {\it Science}, pages 151-167. Springer, 2012. doi:10.1007/978-3-642-35632-2_17. |
| [6] | David A. Basin, Felix Klaedtke, and Eugen Zalinescu.Failure-aware runtime verific ation of distributed systems.In Prahladh Harsha and G. Ramalingam, editors, {\it 35th} {\it IARCS Annual Conference on Foundation of Software Technology and Theoretical Com-} {\it puter Science, FSTTCS 2015, December 16-18, 2015, Bangalore, India}, volume 45 of {\it LIPIcs}, pages 590-603. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. doi: 10.4230/LIPIcs.FSTTCS.2015.590. · Zbl 1366.68010 |
| [7] | :14 |
| [8] | Laura Bocchi, Tzu-Chun Chen, Romain Demangeon, Kohei Honda, and Nobuko Yoshida. Monitoring networks through multiparty session types. {\it Theor. Comput. Sci.}, 669:33-58, 2017. doi:10.1016/j.tcs.2017.02.009. · Zbl 1359.68215 |
| [9] | Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. {\it Model Checking}. MIT Press, Cambridge, MA, USA, 1999. |
| [10] | Matthew B. Dwyer, Madeline Diep, and Sebastian G. Elbaum. Reducing the cost of path property monitoring through sampling. In {\it 23rd IEEE/ACM International Conference on} {\it Automated Software Engineering (ASE 2008), 15-19 September 2008, L’Aquila, Italy}, pages 228-237. IEEE Computer Society, 2008. doi:10.1109/ASE.2008.33. |
| [11] | Adrian Francalanza. A theory of monitors - (extended abstract). In Bart Jacobs and Chris tof Löding, editors, {\it Foundations of Software Science and Computation Structures - 19th} {\it International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences} {\it on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-} {\it 8, 2016, Proceedings}, volume 9634 of {\it Lecture Notes in Computer Science}, pages 145-161. Springer, 2016. doi:10.1007/978-3-662-49630-5_9. · Zbl 1476.68172 |
| [12] | Adrian Francalanza. Consistently-detecting monitors. In Roland Meyer and Uwe Nestmann, editors, {\it 28th International Conference on Concurrency Theory, CONCUR 2017, Septem-} {\it ber 5-8, 2017, Berlin, Germany}, volume 85 of {\it LIPIcs}, pages 8:1-8:19. Schloss Dagstuhl Leibniz-Zentrum fuer Informatik, 2017. doi:10.4230/LIPIcs.CONCUR.2017.8. · Zbl 1442.68107 |
| [13] | Adrian Francalanza, Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Ian Cas sar, Dario Della Monica, and Anna Ingólfsdóttir.A foundation for runtime monitor ing.In Shuvendu K. Lahiri and Giles Reger, editors, {\it Runtime Verification - 17th In-} {\it ternational Conference, RV 2017, Seattle, WA, USA, September 13-16, 2017, Proceed-} |
| [14] | 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, {\it Runtime} {\it Verification - 6th International Conference, RV 2015 Vienna, Austria, September 22-} {\it 25, 2015. Proceedings}, volume 9333 of {\it Lecture Notes in Computer Science}, pages 71-86. Springer, 2015. doi:10.1007/978-3-319-23820-3_5. |
| [15] | Adrian Francalanza, Luca Aceto, and Anna Ingólfsdóttir. Monitorability for the hennessy milner logic with recursion. {\it Formal Methods in System Design}, 51(1):87-116, 2017. doi: 10.1007/s10703-017-0273-z. · Zbl 1370.68203 |
| [16] | Adrian Francalanza and Aldrin Seychell.Synthesising correct concurrent runtime monitors.{\it Formal Methods in System Design}, 46(3):226-261, 2015.doi:10.1007/ s10703-014-0217-9. · Zbl 1323.68373 |
| [17] | Matthew Hennessy. {\it Algebraic Theory of Processes}. Foundations of Computing. MIT Press, 1988. · Zbl 0744.68047 |
| [18] | Dexter Kozen. Results on the propositional mu-calculus. {\it Theor. Comput. Sci.}, 27:333-354, 1983. doi:10.1016/0304-3975(82)90125-6. · Zbl 0553.03007 |
| [19] | Kim Guldstrand Larsen.Proof systems for satisfiability in hennessy-milner logic with recursion. {\it Theor. Comput. Sci.}, 72(2&3):265-288, 1990. doi:10.1016/0304-3975(90) 90038-J. · Zbl 0698.68014 |
| [20] | Martin Leucker and Christian Schallhart. A brief account of runtime verification. {\it J. Log.} {\it Algebr. Program.}, 78(5):293-303, 2009. doi:10.1016/j.jlap.2008.08.004. · Zbl 1192.68433 |
| [21] | Robin Milner. {\it Communication and Concurrency}. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1989. · Zbl 0683.68008 |
| [22] | Jinghao Shi, Shuvendu K. Lahiri, Ranveer Chandra, and Geoffrey Challen. Wireless pro tocol validation under uncertainty. In Yliès Falcone and César Sánchez, editors, {\it Runtime} {\it Verification - 16th International Conference, RV 2016, Madrid, Spain, September 23-30,} {\it 2016, Proceedings}, volume 10012 of {\it Lecture Notes in Computer Science}, pages 351-367. Springer, 2016. doi:10.1007/978-3-319-46982-9_22. |
| [23] | 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, {\it Runtime Verification - 16} |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
