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 条
  • [1] PETRI NET REACHABILITY GRAPHS: DECIDABILITY STATUS OF FIRST-ORDER PROPERTIES
    Darondeau, Philippe
    Demri, Stephane
    Meyer, Roland
    Morvan, Christophe
    LOGICAL METHODS IN COMPUTER SCIENCE, 2012, 8 (04)
  • [2] DECIDABILITY OF THE PETRI NET REACHABILITY PROBLEM
    BUDINAS, BL
    AUTOMATION AND REMOTE CONTROL, 1988, 49 (11) : 1393 - 1422
  • [3] SOME CONSEQUENCES OF THE DECIDABILITY OF THE REACHABILITY PROBLEM FOR PETRI NETS
    LAMBERT, JL
    LECTURE NOTES IN COMPUTER SCIENCE, 1988, 340 : 266 - 282
  • [4] On reachability graphs of Petri nets
    Ye, XM
    Zhou, HT
    Song, XY
    COMPUTERS & ELECTRICAL ENGINEERING, 2003, 29 (02) : 263 - 272
  • [5] Relevant Timed Schedules Clock Valuations for Constructing Time Petri Net Reachability Graphs
    Boucheneb, Hanifa
    Barkaoui, Kamel
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, PROCEEDINGS, 2008, 5215 : 265 - +
  • [6] Relevant Timed Schedules/Clock Vectors for Constructing Time Petri Net Reachability Graphs
    Boucheneb, Hanifa
    Barkaoui, Kamel
    DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2011, 21 (02): : 171 - 204
  • [7] Relevant Timed Schedules/Clock Vectors for Constructing Time Petri Net Reachability Graphs
    Hanifa Boucheneb
    Kamel Barkaoui
    Discrete Event Dynamic Systems, 2011, 21 : 171 - 204
  • [8] Lean Reachability Tree for Petri Net Analysis
    Li, Jun
    Yu, Xiaolong
    Zhou, MengChu
    2016 IEEE 13TH INTERNATIONAL CONFERENCE ON NETWORKING, SENSING, AND CONTROL (ICNSC), 2016,
  • [9] A Sufficient Condition for Reachability in a General Petri Net
    Parthasarathy Ramachandran
    Manjunath Kamath
    Discrete Event Dynamic Systems, 2004, 14 : 251 - 266
  • [10] AN ALGORITHM FOR THE GENERAL PETRI NET REACHABILITY PROBLEM
    MAYR, EW
    SIAM JOURNAL ON COMPUTING, 1984, 13 (03) : 441 - 460
12345