Tree-like counterexamples in model checking
Proceedings - Symposium on Logic in Computer Science - Trang 19-29
Tóm tắt
Counter examples for specification violations provide engineers 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 surprisingly 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.
Từ khóa
#Logic #Computer science #Switches #Art #Intelligent networks #Computer networks #Debugging #Contracts #GovernmentTài liệu tham khảo
maidl, 2000, The common fragment of CTL and LTL, Proc 41th Symp on Foundations of Computer Science (FOCS'2000), 643
thomas, 1989, Computation tree logic and regular ?languages, LNCS, 354, 690
10.1093/logcom/6.4.523
10.1007/978-3-642-59126-6_7
kurshan, 1994, Computer-aided Verification of Coordinating Processes
10.1006/inco.1994.1092
hafer, 1987, Computation tree logic CTL* and path quantifiers in the monadic theory of the binary tree, LNCS, 267, 269
hojati, 1993, Bdd-based debugging of designs using language containment and fair ctl, Proc International Conference on Computer Aided Verification (CAV)
10.1109/DAC.1995.249985
10.1016/B978-0-444-88074-1.50021-4
10.1145/186025.186051
10.1016/0304-3975(94)90269-0
sistla, 1983, Theoretical issues in the design and analysis of distributed systems
10.1006/jcss.2000.1734
10.1007/978-1-4615-3190-6
10.1109/TC.1986.1676819
balarin, 1993, An iterative approach to language containment, Computer-Aided Verification
10.1007/3-540-51237-3_7
clarke, 1999, Model checking
10.1109/DAC.1995.249985
clarke, 2000, Counterexample-guided abstraction refinement, LNCS, 1855, 154
10.1016/0890-5401(92)90017-A
10.1007/10722167_15
clarke, 2000, Model checking, Handbook of Automated Reasoning