Causal Reasoning for Safety in Hennessy Milner Logic
journal contributionposted on 2020-04-17, 09:07 authored by Georgiana Caltais, Mohammad Reza Mousavi, Hargurbir Singh
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.
The work of Georgiana Caltais and Hargurbir Singh was supported by the DFG project “CRENKAT”, proj. no. 398056821.
CitationFundamenta Informaticae, vol. 173, no. 2-3, pp. 217-251, 2020
- AM (Accepted Manuscript)