Publication Date:
2007
abstract:
Witness and counterexample automata (WCA) are automata that recognize the set of finite linear witnesses and counterexamples, respectively. ACTL is an action-based CTL. Program takes the model (subset of standard CCS) and the set of ACTL formulae on the input and produces a textual representation of a corresponding WCA.
Iris type:
05.11 Software
Keywords:
Automatic verification; Temporal logic; Model checking; Binary decision diagrams; Counterexamples
List of contributors: