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
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.
Download to read the full chapter text
Chapter PDF
References
McMillan, K.L.: Symbolic model checking. Kluwer Academic Publishers, Dordrecht (1993)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Shen, S., Qin, Y., Li, S. (2005). Minimizing Counterexample of ACTL Property. In: Borrione, D., Paul, W. (eds) Correct Hardware Design and Verification Methods. CHARME 2005. Lecture Notes in Computer Science, vol 3725. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11560548_39
Download citation
DOI: https://doi.org/10.1007/11560548_39
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29105-3
Online ISBN: 978-3-540-32030-2
eBook Packages: Computer ScienceComputer Science (R0)