(2023) Checking and Sketching Causes on Temporal Sequences.
In: ATVA 2023.
Conference:
ATVA International Symposium on Automated Technology for Verification and Analysis
Abstract
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.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Divisions: | Bernd Finkbeiner (Reactive Systems Group, RSG) |
| Conference: | ATVA International Symposium on Automated Technology for Verification and Analysis |
| Depositing User: | Hadar Frenkel |
| Date Deposited: | 08 Sep 2023 13:48 |
| Last Modified: | 08 Sep 2023 13:48 |
| Primary Research Area: | NRA1: Trustworthy Information Processing |
| URI: | https://publications.cispa.saarland/id/eprint/4029 |
Actions
Actions (login required)
 |
View Item |