Critical trees: counterexamples in model checking of CSM systems using CBS algorithm

TL;DR

This paper discusses the generation of counterexamples, called critical trees, in model checking of CSM systems using the CBS algorithm, highlighting challenges and the output of the TempoRG model checker for QsCTL logic.

Contribution

It describes requirements for critical tree generation in CSM system model checking and analyzes the output of TempoRG for QsCTL logic, addressing contradictions with state space reduction.

Findings

Critical trees are essential for understanding counterexamples in CSM model checking.

TempoRG produces specific counterexamples for QsCTL logic.

Contradictions exist between counterexample generation and state space reduction.

Abstract

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.