Formal Reasoning About Causality Analysis

Systems that can immediately react to their inputs may suffer from cyclic dependencies between their actions and the corresponding trigger conditions. For this reason, causality analysis has to be employed to check the constructiveness of the programs which implies the existence of unique and consistent behaviours. In this paper, we describe the embedding of various views of causality analysis into the HOL4 theorem prover to check their equivalence. In particular, we show the equivalence between the classical analysis procedure, which is based on a fixpoint computation, and a formulation as a (bounded) model checking problem.

• Type: Conference
• Year: 2008
• Where: TPHOL
• Authors: Jens Brandt, Klaus Schneider
• Keywords: Artificial Intelligence, Causality Analysis, Classical Analysis Procedure, Corresponding Trigger Conditions, TPHOL 2008