A Language-Based Causal Model for Safety

Inspired by the seminal works on causal analysis by Halpern and Pearl, in this paper we introduce a causal model based on counterfactuals, adapted to finite automata models and with safety properties defined by regular expressions. The latter encode undesired execution traces. We devise a framework that computes actual causes, or minimal traces that lead to states enabling hazardous behaviours. Furthermore, our framework exploits counterfactual information and identifies modalites to steer causal executions towards alternative safe ones. This can provide systems engineers with valuable data for actual debugging and fixing erroneous behaviours. Our framework employs standard algorithms from automata theory, thus paving the way to further generalizations from finite automata to richer structures like probabilistic or KAT automata.