Synthesis of Temporal Causality
| Autor: | Finkbeiner, Bernd, Frenkel, Hadar, Metzger, Niklas, Siber, Julian |
|---|---|
| Rok vydání: | 2024 |
| Předmět: | |
| Zdroj: | Computer Aided Verification: 36th International Conference, CAV 2024, Proceedings, Part III, Lecture Notes in Computer Science, vol 14683, Springer |
| Druh dokumentu: | Working Paper |
| DOI: | 10.1007/978-3-031-65633-0_5 |
| Popis: | 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 evaluate its performance for cause synthesis and cause checking. Comment: Full version with appendix |
| Databáze: | arXiv |
| Externí odkaz: |
|