Checking and Sketching Causes on Temporal Sequences

Beutner, Raven and Finkbeiner, Bernd and Frenkel, Hadar and Siber, Julian
(2023) Checking and Sketching Causes on Temporal Sequences.
In: ATVA 2023.
Conference: ATVA International Symposium on Automated Technology for Verification and Analysis

Full text not available from this repository.


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.


Actions (login required)

View Item View Item