Causal Reasoning for Safety in Hennessy Milner Logic

Issue title: Special Issue on The Working Formal Methods Symposium (FROM 2018)

Guest editors: Jetty Kleijn, Laurenţiu Leuştean and Dorel Lucanu

Article type: Research Article

Authors: Caltais, Georgiana^{a; *; †} | Mousavi, Mohammad Reza^b | Singh, Hargurbir^c

Affiliations: [a] University of Konstanz, Germany. georgiana.caltais@uni-konstanz.de | [b] University of Leicester, UK. mm789@leicester.ac.uk | [c] University of Konstanz, Germany. hargurbir.singh@uni-konstanz.de

Correspondence: [†] Address for correspondence: University of Konstanz, Germany

Note: [*] The work of Georgiana Caltais and Hargurbir Singh was supported by the DFG project “CRENKAT”, proj. no. 398056821.

Abstract: 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 counterexamples 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.

Keywords: Cauality, Counterfactual causal reasoning, Concurrency, Labelled Transition Systems, Hennessy Milner Logic, Safety, Model-checking, Process algebra, mCRL2

DOI: 10.3233/FI-2020-1922

Journal: Fundamenta Informaticae, vol. 173, no. 2-3, pp. 217-251, 2020