E-mail senden E-Mail Adresse kopieren

Checking and Sketching Causes on Temporal Sequences


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.

Konferenz / Medium

ATVA 2023



Letztes Änderungsdatum

2023-09-08 13:48:50