University of Leicester
Browse
fi-173(2-3)06.pdf (659.39 kB)

Causal Reasoning for Safety in Hennessy Milner Logic

Download (659.39 kB)
journal contribution
posted 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.

Funding

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

History

Citation

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

Version

  • AM (Accepted Manuscript)

Published in

Fundamenta Informaticae

Volume

173

Issue

2-3

Pagination

217 - 251

Publisher

IOS Press

issn

0169-2968

eissn

1875-8681

Copyright date

2020

Available date

2020-03-31

Publisher version

https://content.iospress.com/articles/fundamenta-informaticae/fi1922

Language

en

Usage metrics

    University of Leicester Publications

    Categories

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC