Critical trees: counterexamples in model checking of CSM systems using CBS algorithm
This work tackles a specific technical issue in formal verification for CSM systems, but it appears incremental as it builds on existing model checking methods without introducing major innovations.
The paper addresses the generation of counterexamples, called critical trees, in model checking for CSM systems, presenting output from the TempoRG model checker for QsCTL logic and noting a contradiction between counterexample generation and state space reduction.
The important feature of temporal model checking is the generation of counterexamples. In the report, the requirements for generation of counterexample (called critical tree) in model checking of CSM systems are described. The output of TempoRG model checker for QsCTL logic (a version of CTL) is presented. A contradiction between counterexample generation and state space reduction is commented.