Synthesis of Temporal Causality
Bernd Finkbeiner, Hadar Frenkel, Niklas Metzger, Julian Siber

TL;DR
This paper introduces a complete automata-based algorithm for synthesizing omega-regular causes of omega-regular effects in reactive systems, advancing causal analysis beyond existing limited methods.
Contribution
It presents the first complete cause-synthesis algorithm for omega-regular effects, ensuring causes are also omega-regular and automata-computable.
Findings
Algorithm successfully synthesizes causes as omega-regular automata.
Prototype tool demonstrates practical feasibility and performance.
Method extends causal analysis capabilities in reactive systems.
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\"uchi automata. We demonstrate the practical feasibility of this algorithm with a prototype tool and…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsCognitive Science and Mapping
