Don't know in the μ-calculus

被引：0
作者：
Grumberg, O [1 ]
Lange, M
Leucker, M
Shoham, S
机构：
[1] Technion Israel Inst Technol, Dept Comp Sci, IL-32000 Haifa, Israel
[2] Univ Munich, Inst Informat, D-8000 Munich, Germany
[3] Tech Univ Munich, Inst Informat, D-8000 Munich, Germany
来源：
VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, PROCEEDINGS | 2005年 / 3385卷
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
This work presents game-based model checking for abstract models with respect to specifications in A-calculus, interpreted over a 3-valued semantics. If the model checking result is indefinite (don't know), the abstract model is refined, based on an analysis of the cause for this result. For finite concrete models our abstraction-refinement is fully automatic and guaranteed to terminate with a definite result true or false.
引用
收藏
页码：233 / 249
页数：17
相关论文
共 23 条
  • [1] SYMBOLIC MODEL CHECKING - 1020 STATES AND BEYOND
    BURCH, JR
    CLARKE, EM
    MCMILLAN, KL
    DILL, DL
    HWANG, LJ
    [J]. INFORMATION AND COMPUTATION, 1992, 98 (02) : 142 - 170
  • [2] Clarke E., 2002, CAV
  • [3] Clarke E. M., 2000, LNCS, V1855
  • [4] Clarke EM, 1999, MODEL CHECKING, P1
  • [5] CLEAVELAND R, 1990, ACTA INFORM, V27, P725, DOI 10.1007/BF00264284
  • [6] DAMS D, 1997, ACM T PROGRAMMING LA, V19
  • [7] EMERSON EA, 1991, PROCEEDINGS - 32ND ANNUAL SYMPOSIUM ON FOUNDATIONS OF COMPUTER SCIENCE, P368, DOI 10.1109/SFCS.1991.185392
  • [8] EMERSON EA, 1986, LOGIC COMPUTER SCI
  • [9] Godefroid P, 2003, LECT NOTES COMPUT SC, V2575, P206
  • [10] GODEFROID P, 2002, LECT NOTES COMPUTER, V2404, P137
123