Causal Reasoning for Safety in Hennessy Milner Logic

• Autorzy: Caltais Georgiana , Mousavi Mohammad Reza , Singh Hargurbir

Identyfikatory

DOI

10.3233/FI-2020-1922

• Języki publikacji: EN

Abstrakty

EN

Determining and computing root causes in system failures is a significant issue in science and engineering. In this paper, we introduce a notion of causality for explaining counter-examples in system analysis based on formal models. The counter-examples are produced by checking for hazardous situations expressed in the Hennessy-Milner Logic, in the context of Labelled Transition System models. We also introduce CauseJMu, a tool for automatically identifying such causal computations within a system model. CauseJMu relies on encoding causality in terms of an extension of Hennessy-Milner Logic to recursive formulae with data. The encodings enable deciding whether a certain computation is causal or not, using the mCRL2 model checker.

Słowa kluczowe

EN

cauality; concurrency; counterfactual causal reasoning; Hennessy Milner Logic; labelled transition systems; mCRL2; model checking; process algebra; safety

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2020
• Tom: Vol. 173, nr 2-3
• Strony: 217--251
• Opis fizyczny: Bibliogr. 49 poz., rys., tab.

Twórcy

autor

Caltais Georgiana

• University of Konstanz, Germany

autor

Mousavi Mohammad Reza

• University of Leicester, UK

autor

Singh Hargurbir

• University of Konstanz, Germany

Bibliografia

• [1] Lewis D. Counterfactuals. Blackwell Publishers, 1973.
• [2] Halpern JY, Pearl J. Causes and Explanations: A Structural-Model Approach: Part 1: Causes. In: Breese and Koller [48], 2001 pp. 194-202. URL https://dslpitt.org/uai/displayArticleDetails.jsp?mmnu=1&smnu=2&article_id=100&proceeding_id=17.
• [3] Halpern JY. A Modification of the Halpern-Pearl Definition of Causality. In: Yang and Wooldridge [49], 2015 pp. 3022-3033. URL http://ijcai.org/Abstract/15/427.
• [4] Leitner-Fischer F, Leue S. Probabilistic fault tree synthesis using causality computation. IJCCBS, 2013. 4(2):119-143. doi:10.1504/IJCCBS.2013.056492.
• [5] Leitner-Fischer F, Leue S. Causality Checking for Complex System Models. In: Giacobazzi et al. [37], 2013 pp. 248-267. doi:10.1007/978-3-642-35873-9_16.
• [6] Caltais G, Leue S, Mousavi MR. (De-)Composing Causality in Labeled Transition Systems. In: Gößler and Sokolsky [36], 2016 pp. 10-24. doi:10.4204/EPTCS.224.3.
• [7] Hennessy M, Milner R. On Observing Nondeterminism and Concurrency. In: de Bakker and van Leeuwen [39], 1980 pp. 299-309. URL http://dx.doi.org/10.1007/3-540-10003-2_79.
• [8] Zeller A. Why Programs Fail: A Guide to Systematic Debugging. Elsevier, 2009.
• [9] Renieris M, Reiss S. Fault localization with nearest neighbor queries. In: 18th International Conference on Automated Software Engineering. Montreal, Canada, 2003.
• [10] Groce A, Visser W. What Went Wrong: Explaining Counterexamples. In: Workshop on Software Model Checking (SPIN), Lecture Notes in Computer Science 2648. Springer, 2003 pp. 121-135.
• [11] Groce A, Chaki S, Kroening D, Strichman O. Error explanation with distance metrics. International Journal on Software Tools for Technology Transfer (STTT), 2006. 8(3):229-247. doi:10.1007/s10009-005-0202-0.
• [12] Ladkin P, Loer K. Analysing Aviation Accidents Using WB-Analysis - an Application of Multimodal Reasoning. In: AAAI Spring Symposium. AAAI, 1998 URL https://www.aaai.org/Papers/Symposia/Spring/1998/SS-98-04/SS98-04-031.pdf.
• [13] Gößler G, Le Métayer D, Raclet J. Causality Analysis in Contract Violation. In: Runtime Verification - First International Conference, RV 2010, volume 6418 of Lecture Notes in Computer Science. Springer, 2010 pp. 270-284. doi:10.1007/978-3-642-16612-9_21.
• [14] Gößler G, Astefanoaei L. Blaming in component-based real-time systems. In: 2014 International Conference on Embedded Software, EMSOFT 2014. ACM Press, 2014 pp. 7:1-7:10. doi:10.1145/2656045.2656048.
• [15] Gößler G, Le Métayer D. A general framework for blaming in component-based systems. Sci. Comput. Program., 2015. 113:223-235. doi:10.1016/j.scico.2015.06.010.
• [16] Gößler G, Stefani J. Fault Ascription in Concurrent Systems. In: Trustworthy Global Computing - 10th International Symposium, TGC, volume 9533 of Lecture Notes in Computer Science. Springer, 2016 pp. 79-94. doi:10.1007/978-3-319-28766-9.
• [17] Befrouei MT, Wang C, Weissenbacher G. Abstraction and Mining of Traces to Explain Concurrency Bugs. In: Bonakdarpour and Smolka [35], 2014 pp. 162-177. URL http://dx.doi.org/10.1007/978-3-319-11164-3_14.
• [18] Milner R. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer, 1980. ISBN: 3-540-10235-3. doi:10.1007/3-540-10235-3.
• [19] Arbach Y, Karcher DS, Peters K, Nestmann U. Dynamic Causality in Event Structures. Logical Methods in Computer Science, 2018. 14(1). doi:10.23638/LMCS-14(1:17)2018.
• [20] Nielsen M, Plotkin GD, Winskel G. Petri Nets, Event Structures and Domains, Part I. Theor. Comput. Sci., 1981. 13:85-108. doi:10.1016/0304-3975(81)90112-2.
• [21] Groote JF, Mousavi MR. Modeling and Analysis of Communicating Systems. MIT Press, 2014. ISBN: 9780262027717. URL https://mitpress.mit.edu/books/modeling-and-analysis-communicating-systems.
• [22] Saberi AK, Groote JF, Keshishzadeh S. Analysis of Path Planning Algorithms: a Formal Verification-based Approach. In: Liò et al. [41], 2013 pp. 232-239. doi:10.7551/978-0-262-31709-2-ch035.
• [23] Aceto L, Inglfsdttir A, Larsen KG, Srba J. Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, 2007. doi:10.1017/CBO9780511814105.
• [24] Plotkin GD. A structural approach to operational semantics. J. Log. Algebr. Program., 2004. 60-61:17-139. doi:10.1016/j.jlap.2004.05.001.
• [25] Bloom B, Istrail S, Meyer AR. Bisimulation Can’t be Traced. J. ACM, 1995. 42(1):232-268. doi:10.1145/200836.200876.
• [26] Baier C, Katoen J. Principles of model checking. MIT Press, 2008. ISBN: 978-0-262-02649-9.
• [27] Caltais G, Guetlein SL, Leue S. Causality for General LTL-definable Properties. https://www.sen.uni-konstanz.de/typo3temp/secure_downloads/76523/0/d21a67cb313b43ca396aa4c0be674c37f89e7fea/Causality_Checking_for_Liveness_Properties.pdf. To appear in EPTCS.
• [28] Bergstra JA, Ponse A, Smolka SA (eds.). Handbook of Process Algebra. North-Holland / Elsevier, 2001. ISBN: 978-0-444-82830-9. doi:10.1016/b978-0-444-82830-9.x5017-6.
• [29] Stevens P, Stirling C. Practical Model-Checking Using Games. In: Steffen [40], 1998 pp. 85-101. doi:10.1007/BFb0054166.
• [30] Cranen S, Keiren JJA, Willemse TAC. Parity game reductions. Acta Inf., 2018. 55(5):401-444. doi:10.1007/s00236-017-0301-x.
• [31] Beer A, Heidinger S, Kühne U, Leitner-Fischer F, Leue S. Symbolic Causality Checking Using Bounded Model Checking. In: Fischer and Geldenhuys [34], 2015 pp. 203-221. doi:10.1007/978-3-319-23404-5_14.
• [32] Bradfield JC, Stirling C. Modal Logics and mu-Calculi: An Introduction. In: Bergstra et al. [28], pp. 293-330, 2001. doi:10.1016/b978-044482830-9/50022-9.
• [33] Fischer MJ, Ladner RE. Propositional Dynamic Logic of Regular Programs. J. Comput. Syst. Sci., 1979. 18(2):194-211. doi:10.1016/0022-0000(79)90046-1.
• [34] Fischer B, Geldenhuys J (eds.). Model Checking Software - 22nd International Symposium, SPIN 2015, Stellenbosch, South Africa, August 24-26, 2015, Proceedings, volume 9232 of Lecture Notes in Computer Science. Springer, 2015. ISBN: 978-3-319-23403-8. doi:10.1007/978-3-319-23404-5.
• [35] Bonakdarpour B, Smolka SA (eds.). Runtime Verification - 5th International Conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014. Proceedings, volume 8734 of Lecture Notes in Computer Science. Springer, 2014. ISBN: 978-3-319-11163-6.
• [36] Gößler G, Sokolsky O (eds.). Proceedings First Workshop on Causal Reasoning for Embedded and safety-critical Systems Technologies, CREST@ETAPS 2016, Eindhoven, The Netherlands, 8th April 2016, volume 224 of EPTCS. 2016. doi:10.4204/EPTCS.224.
• [37] Giacobazzi R, Berdine J, Mastroeni I (eds.). Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings, volume 7737 of Lecture Notes in Computer Science. Springer, 2013. ISBN: 978-3-642-35872-2. doi:10.1007/978-3-642-35873-9.
• [38] Lewis D. Causation. Journal of Philosophy, 1973. 70:556-567. doi:10.2307/2025310.
• [39] de Bakker JW, van Leeuwen J (eds.). Automata, Languages and Programming, 7th Colloquium, Noordweijkerhout, The Netherland, July 14-18, 1980, Proceedings, volume 85 of Lecture Notes in Computer Science. Springer, 1980. ISBN: 3-540-10003-2.
• [40] Steffen B (ed.). Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS ’98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings, volume 1384 of Lecture Notes in Computer Science. Springer, 1998. ISBN: 3-540-64356-7. doi:10.1007/BFb0054159.
• [41] Liò P, Miglino O, Nicosia G, Nolfi S, Pavone M (eds.). Proceedings of the Twelfth European Conference on the Synthesis and Simulation of Living Systems: Advances in Artificial Life, ECAL 2013, Sicily, Italy, September 2-6, 2013. MIT Press, 2013. ISBN: 9780262317092. URL https://mitpress.mit.edu/books/advances-artificial-life-ecal-2013.
• [42] Cleaveland R. Tableau-Based Model Checking in the Propositional Mu-Calculus. Acta Inf., 1990. 27(8):725-747. doi:10.1007/BF00264284.
• [43] Andersen H. Verification of Temporal Properties of Concurrent Systems. DAIMI Report Series, 1993. 22(445). doi:10.7146/dpb.v22i445.6762.
• [44] Bradfield JC, Walukiewicz I. The mu-calculus and Model Checking. In: Clarke et al. [45], pp. 871-919, 2018. doi:10.1007/978-3-319-10575-8_26.
• [45] Clarke EM, Henzinger TA, Veith H, Bloem R (eds.). Handbook of Model Checking. Springer, 2018. ISBN: 978-3-319-10574-1. doi:10.1007/978-3-319-10575-8.
• [46] Cranen S, Groote JF, Keiren JJA, Stappers FPM, de Vink EP, Wesselink W, Willemse TAC. An Overview of the mCRL2 Toolset and Its Recent Advances. In: Piterman and Smolka [47], 2013 pp. 199-213. doi:10.1007/978-3-642-36742-7_15.
• [47] Piterman N, Smolka SA (eds.). Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, volume 7795 of Lecture Notes in Computer Science. Springer, 2013. ISBN: 978-3-642-36741-0. doi:10.1007/978-3-642-36742-7.
• [48] Breese JS, Koller D (eds.). UAI ’01: Proceedings of the 17th Conference in Uncertainty in Artificial Intelligence, University of Washington, Seattle, Washington, USA, August 2-5, 2001. Morgan Kaufmann, 2001. ISBN: 1-55860-800-1.
• [49] Yang Q, Wooldridge M (eds.). Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015. AAAI Press, 2015. ISBN:978-1-57735-738-4.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2020).