Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
E. Clarke, S. Jha, Y. Lu, H. Veith:
"Tree-Like Counterexamples in Model Cheking";
Vortrag: 17th Annual IEEE Symposium on Logic in Computer Science (LIC'S02),
Copenhagen, Denmark;
22.07.2002
- 25.07.2002; in: "Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science (LICS' 2002)",
(2002),
ISBN: 0-7695-1483-9;
S. 19
- 29.
Kurzfassung englisch:
Counterexamples for specification violations provide etngineers with important debugging information. Although counterexamples are considered one of the main advantages of model checking, state-of the art model checkers are restricted to relatively simple counterexamples, and suprisingly little research effort has been put into counterexamples. In this paper, we introduce a new general framework for counterexamples. The paper has three main contributions: (i) We determine the general form of ACTL counterexamples. To this end, we investigate the notion of counterexample and show that a large class of temporal logics beyond ACTL admits counterexamples with a simple tree-like transition relation. We show that the existence of tree-like counterexamples is related to a universal fragment of extended branching time logic based on w-regular temporal operators. (ii) We present new symbolic algorithms to generate tree-like counterexamples for ACTL specifications. (iii) Based on tree-like counterexamples we extend the abstraction refinement methodology developed recently by Clarke et al. (CAV'2000) to full ACTL. This demonstrates the conceptual simplicity and elegance of tree-like counterexamples.
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.