A symbolic semantics for abstract model checking

被引：1
作者：
Levi, F [1 ]
机构：
[1] Univ Pisa, Dipartimento Informat, I-56100 Pisa, Italy
来源：
SCIENCE OF COMPUTER PROGRAMMING | 2001年 / 39卷 / 01期
关键词：
model checking; mu-calculus; abstract interpretation;
D O I：
10.1016/S0167-6423(00)00015-0
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
In this paper we present a symbolic semantics of value-passing concurrent processes where classical branching is replaced by separate relations of non-deterministic branch and alternative choice. The obtained symbolic graph is finite for regular processes and can suitably be interpreted over abstract values to effectively compute a safe abstract model for full mu -calculus model checking. The representation of non-determinism and alternative choice in symbolic transitions allows to achieve more precise approximations of the two dual next modalities. (C) 2001 Elsevier Science B.V. All rights reserved.
引用
收藏
页码：93 / 123
页数：31
相关论文
共 22 条
  • [1] BENSALEM S, 1992, LECT NOTES COMPUTER, V663, P260
  • [2] Burch JR, 1990, P 5 ANN IEEE S LOG C, P428, DOI DOI 10.1109/LICS.1990.113767
  • [3] MODEL CHECKING AND ABSTRACTION
    CLARKE, EM
    GRUMBERG, O
    LONG, DE
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1994, 16 (05): : 1512 - 1542
  • [4] CLARKE EM, 1992, P 19 ANN ACM S PRINC, P343
  • [5] Cleaveland R, 1994, LECT NOTES COMPUT SC, V836, P417
  • [6] CLEAVELAND R, 1996, LECT NOTES COMPUTER, V1055, P107
  • [7] CLEAVELAND R, 1995, LECT NOTES COMPUTER, V983, P51
  • [8] ABSTRACT INTERPRETATION AND APPLICATION TO LOGIC PROGRAMS
    COUSOT, P
    COUSOT, R
    [J]. JOURNAL OF LOGIC PROGRAMMING, 1992, 13 (2-3): : 103 - 179
  • [9] Cousot P., 1977, P 4 ACM SIGACT SIGPL, DOI DOI 10.1145/512950.512973
  • [10] Cousot Patrick, 1979, POPL, P269, DOI DOI 10.1145/567752.567778
123