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.

翻译：我们提出一种基于自动机的算法，用于综合反应系统执行轨迹上ω-正则效应（例如模型检测器发现的违反示例）的ω-正则原因。该理论是对时间因果性的一般化推广——后者最近被提出作为在给定轨迹上建立迹性质间因果关系的一种框架。目前，仅存在验证单一因果关系的算法，而作为扩展，通过枚举法进行原因综合仅对一小类效应性质具有完备性。本文提出首个针对ω-正则效应类别的完备原因综合算法。我们证明在此情形下，原因本身必定是ω-正则的，且可计算为例如非确定性Büchi自动机等形式。通过原型工具验证了该算法的实际可行性，并评估了其在原因综合与原因检测方面的性能表现。