Advertisement

Minimizing Counterexample of ACTL Property

  • ShengYu Shen
  • Ying Qin
  • SiKun Li
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)

Abstract

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.

Keywords

Model Check Terminal Node Variable Node Kripke Structure Symbolic Model Check 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    McMillan, K.L.: Symbolic model checking. Kluwer Academic Publishers, Dordrecht (1993)zbMATHGoogle Scholar
  2. 2.
    Ravi, K., Somenzi, F.: Minimal assignments for bounded model checking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 31–45. Springer, Heidelberg (2004)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • ShengYu Shen
    • 1
  • Ying Qin
    • 1
  • SiKun Li
    • 1
  1. 1.School of Computer ScienceNational University of Defense Technology of China 

Personalised recommendations