Model Checking EGF on Basic Parallel Processes

被引：0
|
作者：
Fu, Hongfei [1 ]
机构：
[1] Rhein Westfal TH Aachen, D-52074 Aachen, Germany
来源：
AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS | 2011年 / 6996卷
关键词：
infinite-state systems; Basic Parallel Processes; model checking; EGF;
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
In this paper we study the problem of model checking the logic EGF over Basic Parallel Processes (BPP). The logic EGF is obtained by extending the logic EF with the CTL* notation EGF, which means that there exists an infinite path on which there are infinitely many entries satisfying certain property. We prove that this problem is PSPACE-complete, and Sigma(p)(d)-complete for certain classes of fixed formula with the nesting depth d of modal operators.
引用
收藏
页码：120 / 134
页数：15
相关论文
共 50 条
  • [21] Complexity of Checking Bisimilarity between Sequential and Parallel Processes
    Czerwinski, Wojciech
    Jancar, Petr
    Kot, Martin
    Sawa, Zdenek
    MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 2013, 2013, 8087 : 302 - 313
  • [22] Model building and model checking for biochemical processes
    Antoniotti, M
    Policriti, A
    Ugel, N
    Mishra, B
    CELL BIOCHEMISTRY AND BIOPHYSICS, 2003, 38 (03) : 271 - 286
  • [23] Model building and model checking for biochemical processes
    Marco Antoniotti
    Alberto Policriti
    Nadia Ugel
    Bud Mishra
    Cell Biochemistry and Biophysics, 2003, 38 : 271 - 286
  • [24] Symbolic model checking for probabilistic processes
    Baier, C
    Clarke, EM
    Hartonas-Garmhausen, V
    Kwiatkowska, M
    Ryan, M
    AUTOMATA, LANGUAGES AND PROGRAMMING, 1997, 1256 : 430 - 440
  • [25] Model Checking Parallel Interval Logic on Parallel Run Structures
    Cao, Zining
    2012 THIRD INTERNATIONAL CONFERENCE ON THEORETICAL AND MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE (ICTMF 2012), 2013, 38 : 390 - 394
  • [26] Model Checking for Communicating Quantum Processes
    Davidson, Tim
    Gay, Simon J.
    Mlnarik, Hynek
    Nagarajan, Rajagopal
    Papanikolau, Nick
    INTERNATIONAL JOURNAL OF UNCONVENTIONAL COMPUTING, 2012, 8 (01) : 73 - 98
  • [27] Bounded model checking of compositional processes
    Sun, Jun
    Liu, Yang
    Dong, Jin Song
    Sun, Jing
    TASE 2008: SECOND IFIP/IEEE INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS, 2008, : 23 - +
  • [28] Model checking PA-processes
    Mayr, R
    CONCUR'97 : CONCURRENCY THEORY, 1997, 1243 : 332 - 346
  • [29] Model Checking Stochastic Branching Processes
    Chen, Taolue
    Draeger, Klaus
    Kiefer, Stefan
    MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 2012, 2012, 7464 : 271 - 282
  • [30] Model-checking processes with data
    Groote, JF
    Willemse, TAC
    SCIENCE OF COMPUTER PROGRAMMING, 2005, 56 (03) : 251 - 273
12345