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 条
  • [31] Model checking ACTL constrained processes
    Chen, XJ
    FRONTIERS OF COMBINING SYSTEMS, 1996, 3 : 377 - 388
  • [32] Model checking for communicating quantum processes
    Davidson, T. (tim@dcs.warwick.ac.uk), 1600, Old City Publishing, 628 North 2nd Street, Philadelphia, PA 19123, United States (08):
  • [33] Shared Hash Tables in Parallel Model Checking
    Barnat, Jiri
    Rockai, Petr
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 198 (01) : 79 - 91
  • [34] Parallel and complete model checking with linear complexity
    Wu, Xiaojuan
    Wu, Lijun
    Huang, Huijia
    Xue, Lei
    Journal of Information and Computational Science, 2013, 10 (05): : 1519 - 1529
  • [35] Parallel Model Checking for Temporal Epistemic Logic
    Kwiatkowska, Marta
    Lomuscio, Alessio
    Qu, Hongyang
    ECAI 2010 - 19TH EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2010, 215 : 543 - 548
  • [36] Parallel Bounded Model Checking of Security Protocols
    Kurkowski, Miroslaw
    Siedlecka-Lamch, Olga
    Szymoniak, Sabina
    Piech, Henryk
    PARALLEL PROCESSING AND APPLIED MATHEMATICS (PPAM 2013), PT I, 2014, 8384 : 224 - 234
  • [37] Using Parallel and Distributed Reachability in Model Checking
    Allal, Lamia
    Belalem, Ghalem
    Dhaussy, Philippe
    Teodorov, Ciprian
    AMBIENT COMMUNICATIONS AND COMPUTER SYSTEMS, RACCCS 2017, 2018, 696 : 143 - 154
  • [38] Parallel SAT solving in bounded model checking
    Abraham, Erika
    Schubert, Tobias
    Becker, Bernd
    Fraenzle, Martin
    Herde, Christian
    FORMAL METHODS: APPLICATIONS AND TECHNOLOGY, 2007, 4346 : 301 - 315
  • [39] Parallel SAT Solving in Bounded Model Checking
    Abraham, Erika
    Schubert, Tobias
    Becker, Bernd
    Fraenzle, Martin
    Herde, Christian
    JOURNAL OF LOGIC AND COMPUTATION, 2011, 21 (01) : 5 - 21
  • [40] Decidability of performance equivalence for basic parallel processes
    Lasota, Slawomir
    THEORETICAL COMPUTER SCIENCE, 2006, 360 (1-3) : 172 - 192
12345