Symbolic model checking APSL

被引：0
|
作者：
Liu, Wanwei [1 ]
Wang, Ji [1 ]
Chen, Huowang [1 ]
Ma, Xiaodong [1 ]
机构：
[1] Natl Univ Def Technol, Sch Comp, Natl Lab Parallel & Distributed Proc, Hunan, Peoples R China
来源：
TASE 2008: SECOND IFIP/IEEE INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS | 2008年
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
PSL is a kind of temporal logic which uses SEREs as additional formula constructs. We present a variant of PSL, namely APSL, which replaces SEREs with finite automata. APSL and PSL are of the exactly same expressiveness. In this paper we extend the LTL symbolic model checking algorithm to that of APSL, and present a tableau based APSL verification approach. Moreover we show how to implement this algorithm via the BDD based symbolic approach.
引用
收藏
页码：39 / 46
页数：8
相关论文
共 50 条
  • [21] Distributed symbolic model checking for μ-calculus
    Grumberg, O
    Heyman, T
    Schuster, A
    FORMAL METHODS IN SYSTEM DESIGN, 2005, 26 (02) : 197 - 219
  • [22] Bayesian Inference by Symbolic Model Checking
    Salmani, Bahare
    Katoen, Joost-Pieter
    QUANTITATIVE EVALUATION OF SYSTEMS (QEST 2020), 2020, 12289 : 115 - 133
  • [23] A symbolic semantics for abstract model checking
    Levi, F
    STATIC ANALYSIS, 1998, 1503 : 134 - 151
  • [24] Design constraints in symbolic model checking
    Kaufmann, M
    Martin, A
    Pixley, C
    COMPUTER AIDED VERIFICATION, 1998, 1427 : 477 - 487
  • [25] Symbolic model checking of logics with actions
    Pecheur, Charles
    Raimondi, Franco
    MODEL CHECKING AND ARTIFICIAL INTELLIGENCE, 2007, 4428 : 113 - +
  • [26] Symbolic model checking of biochemical networks
    Chabrier, N
    Fages, F
    COMPUTATIONAL METHODS IN SYSTEMS BIOLOGY, PROCEEDINGS, 2003, 2602 : 149 - 162
  • [27] ON SYMBOLIC MODEL CHECKING IN PETRI NETS
    HIRAISHI, K
    NAKANO, M
    IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 1995, E78A (11) : 1479 - 1486
  • [28] Distributed Symbolic Model Checking for μ-Calculus
    Orna Grumberg
    Tamir Heyman
    Assaf Schuster
    Formal Methods in System Design, 2005, 26 : 197 - 219
  • [29] Optimizing symbolic model checking for statecharts
    Chan, W
    Anderson, RJ
    Beame, P
    Jones, DH
    Notkin, D
    Warner, WE
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2001, 27 (02) : 170 - 190
  • [30] Distributed symbolic model checking for μ-calculus
    Grumberg, O
    Heyman, T
    Schuster, A
    COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2001, 2102 : 350 - 362
12345