Checking and Sketching Causes on Temporal Sequences

Summary

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 w -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.