Synthesis of Temporal Causality

2024/05/17 by Bernd Finkbeiner, Finkbeiner, Bernd, Hadar Frenkel +5 · 3 citations
Computer Science · #Cognitive Science and Mapping #FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · pdf · doi:10.48550/arxiv.2405.10912

openalex publication_date 2024/05/17 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

We present an automata-based algorithm to synthesize omega-regular causes for omega-regular effects on executions of a reactive system, such as counterexamples uncovered by a model checker. Our theory is a generalization of temporal causality, which has recently been proposed as a framework for drawing causal relationships between trace properties on a given trace. So far, algorithms exist only for verifying a single causal relationship and, as an extension, cause synthesis through enumeration, which is complete only for a small fragment of effect properties. This work presents the first complete cause-synthesis algorithm for the class of omega-regular effects. We show that in this case, causes are guaranteed to be omega-regular themselves and can be computed as, e.g., nondeterministic Büchi automata. We demonstrate the practical feasibility of this algorithm with a prototype tool and evaluate its performance for cause synthesis and cause checking.

Cited by

• TempoBench: Evaluating Temporal Causal Reasoning in Large Language Models
• Explainability Requirements as Hyperproperties
• Probability-Raising Causality for Uncertain Parametric Markov Decision Processes with PAC Guarantees

Related

• Efficient Discovery of Actual Causality using Abstraction-Refinement
• Closure and Complexity of Temporal Causality
• Discovering Mechanistic Causality from Time Series: A Behavioral-System Approach
• The Temporal Logic of Causal Structures
• Generating Counterfactual Explanations Under Temporal Constraints