Petri Net Reachability Graphs: Decidability Status of FO Properties

被引：2
|
作者：
Darondeau, Philippe [1 ]
Demri, Stephane [2 ]
Meyer, Roland [3 ]
Morvan, Christophe [4 ]
机构：
[1] INRIA, IRISA, Campus Beaulieu, Rennes, France
[2] INRIA, CNRS, ENS Cachan, LSV, Cachan, France
[3] Univ Kaiserslautern, D-67663 Kaiserslautern, Germany
[4] Univ Paris Est, Marne La Vallee, France
来源：
IARCS ANNUAL CONFERENCE ON FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE (FSTTCS 2011) | 2011年 / 13卷
关键词：
Petri nets; First order logic; Reachability graph;
D O I：
10.4230/LIPIcs.FSTTCS.2011.140
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We investigate the decidability and complexity status of model-checking problems on unlabelled reachability graphs of Petri nets by considering first-order, modal and pattern-based languages without labels on transitions or atomic propositions on markings. We consider several parameters to separate decidable problems from undecidable ones. Not only are we able to provide precise borders and a systematic analysis, but we also demonstrate the robustness of our proof techniques.
引用
收藏
页码：140 / 151
页数：12
相关论文
共 50 条
  • [31] Property analysis of logic Petri nets by marking reachability graphs
    Du, Yuyue
    Ning, Yuhui
    FRONTIERS OF COMPUTER SCIENCE, 2014, 8 (04) : 684 - 692
  • [32] Verification of Reachability Properties for Time Petri Nets
    Klai, Kais
    Aber, Naim
    Petrucci, Laure
    REACHABILITY PROBLEMS, 2013, 8169 : 159 - 170
  • [33] Decidability of properties of timed-arc Petri nets
    Escrig, DD
    Ruiz, VV
    Alonso, OM
    APPLICATION AND THEORY OF PETRI NETS 2000, PROCEEDINGS, 2000, 1825 : 187 - 206
  • [34] Approximating Petri Net Reachability Along Context-free Traces
    Atig, Mohamed Faouzi
    Ganty, Pierre
    IARCS ANNUAL CONFERENCE ON FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE (FSTTCS 2011), 2011, 13 : 152 - 163
  • [35] Classifications of Petri net transitions and their application to firing sequence and reachability problems
    Huang, JS
    Murata, T
    SMC '97 CONFERENCE PROCEEDINGS - 1997 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN, AND CYBERNETICS, VOLS 1-5: CONFERENCE THEME: COMPUTATIONAL CYBERNETICS AND SIMULATION, 1997, : 263 - 268
  • [36] Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability
    Amat, Nicolas
    Dal Zilio, Silvano
    Le Botlan, Didier
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2024, PT I, 2024, 14499 : 101 - 123
  • [37] Finite symbolic reachability graphs for high-level Petri nets
    Hameurlain, N
    Sibertin-Blanc, C
    ASIA PACIFIC SOFTWARE ENGINEERING CONFERENCE AND INTERNATIONAL COMPUTER SCIENCE CONFERENCE, PROCEEDINGS, 1997, : 150 - 159
  • [38] Parallel computation of the reachability graph of petri net models with semantic information
    de Murillas, Eduardo Gonzalez-Lopez
    Fabra, Javier
    Alvarez, Pedro
    Ezpeleta, Joaquin
    SOFTWARE-PRACTICE & EXPERIENCE, 2017, 47 (05): : 647 - 668
  • [39] A New Approach to Analyze the Reachability of Petri Net and Its Use in Maintenance
    Fang, Hualing
    Dong, Chuandai
    PROCEEDINGS OF 2009 8TH INTERNATIONAL CONFERENCE ON RELIABILITY, MAINTAINABILITY AND SAFETY, VOLS I AND II: HIGHLY RELIABLE, EASY TO MAINTAIN AND READY TO SUPPORT, 2009, : 630 - +
  • [40] Marking Estimation in Petri Nets Using Hierarchical Basis Reachability Graphs
    Ma, Ziyue
    Zhu, Guanghui
    Li, Zhiwu
    IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2021, 66 (02) : 810 - 817
12345