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 ω-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.
ATVA 2023
2023-10-24
2023-09-08 13:48:50