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

2017/10/26 by Wiktor B. Daszczuk, Daszczuk, Wiktor B.
Computer Science · #68N30 #D.2.4 #FOS: Computer and information sciences #Software Engineering (cs.SE) #acm:68N30 #cs.SE #msc:68N30

paper · pdf · doi:10.48550/arxiv.1710.09887

20 pages, 12 figures

arxiv created 2017/10/26 · arxiv updated 2017/10/30

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.

Related

• Model Checking
• State Space Reduction for Reachability Graph of CSM Automata
• Experimental Study on CTL model checking using Machine Learning
• Soundness and Completeness of a Model-Checking Proof System for CTL
• Graded CTL Model Checking for Test Generation