Minimizing Counterexample of ACTL Property
Counterexample minimization tries to remove irrelevant variables from counterexamples, such that they are easier to be understood. For the first time, we proposes a novel approach to minimize loop-like and path-like counterexamples of ACTL properties. For a counterexample s 0... s k , our algorithm tries to extract a succinct cube sequence c 0... c k , such that paths run through c 0... c k are all valid counterexamples. Experimental result shows that our algorithm can significantly minimize ACTL counterexamples.
KeywordsModel Check Terminal Node Variable Node Kripke Structure Symbolic Model Check