Checking and Sketching Causes on Temporal Sequences
Raven Beutner, Bernd Finkbeiner, Hadar Frenkel, and Julian Siber
Temporal causality describes what concrete input behavior is responsible for some observed output behavior on a trace of a reactive system, and can be used to, e.g., generate explanations for counterexamples uncovered by a model checker. In this paper, we present CATS, the first tool that can automatically verify whether a given temporal property (specified in QPTL) is a cause for some observed omega-regular effect. In addition to checking whether a given property is a cause, CATS can search for potential causes by exhaustively exploring a cause sketch, i.e., a temporal formula in which some parts are left unspecified. Our experiments show that CATS can effectively check causes and search for causes in small reactive systems.
21th International Symposium on Automated Technology for Verification and Analysis (ATVA 2023).