Model Checking Causality

Model Checking Causality

Tiago de Lima, Emiliano Lorini

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence
Main Track. Pages 3324-3332. https://doi.org/10.24963/ijcai.2024/368

We present a novel modal language for causal reasoning and interpret it by means of a semantics in which causal information is represented using causal bases in propositional form. The language includes modal operators of conditional causal necessity where the condition is a causal change operation. We provide a succinct formulation of model checking for our language and a model checking procedure based on a polysize reduction to QBF. We illustrate the expressiveness of our language through some examples and show that it allows us to represent and to formally verify a variety of concepts studied in the field of explainable AI including abductive explanation, intervention and actual cause.
Keywords:
Knowledge Representation and Reasoning: KRR: Causality
Knowledge Representation and Reasoning: KRR: Knowledge representation languages