Extracting Counterexamples from Transitive-Closure-Based Model Checking
Loading...
Date
Authors
Kember, Mitchell
Tran, Lynn
Gao, George
Day, Nancy
Advisor
Journal Title
Journal ISSN
Volume Title
Publisher
IEEE
Abstract
We address the problem of how to extract counterexamples for the transitive-closure-based model checking (TCMC) technique. TCMC is a representation of the CTLFC (CTL with fairness constraints) model checking problem in first-order logic with transitive closure (FOLTC) and has been implemented in the Alloy Analyzer. It is a declarative, symbolic model checking method. As a CTL model checking method, TCMC is defined over transition systems and states (rather than paths) and therefore, returns a transition system with a bug as a counterexample. Our contribution is to isolate a counterexample path/subgraph in a declarative manner by adding constraints that do not depend on the property. Our method does not require extensions to Alloy.
Description
© 2019 IEEE
Keywords
model checking, counterexamples, subgraphs, TCMC, CTLFC, formal verification, temporal logic, transitive-closure-based model checking, CTL with fairness constraints, symbolic model checking, CTL model checking, counterexamples extraction, CTLFC model checking, first-order logic with transitive closure, temporal logic property, Alloy, Alloy Analyzer