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 条
  • [11] 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,
  • [12] A sufficient condition for reachability in a general Petri net
    Ramachandran, P
    Kamath, M
    DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2004, 14 (03): : 251 - 266
  • [13] Calculation and Analysis of Petri Net Reachability Graphs by a Think-Globally-Act-Locally Method
    Li, Chengzong
    Jin, Fubao
    Chen, Yufeng
    Li, Zhiwu
    Uzam, Murat
    Ma, Huimin
    MATHEMATICS, 2025, 13 (05)
  • [14] Petri Net Synthesis from a Reachability Set
    Best, Eike
    Devillers, Raymond
    APPLICATION AND THEORY OF PETRI NETS AND CONCURRENCY, PETRI NETS 2024, 2024, 14628 : 223 - 243
  • [15] On reachability in autonomous continuous Petri net systems
    Júlvez, J
    Recalde, L
    Silva, M
    APPLICATIONS AND THEORY OF PETRI NETS 2003, PROCEEDINGS, 2003, 2679 : 221 - 240
  • [16] DECIDABILITY AND CLOSURE-PROPERTIES OF WEAK PETRI-NET LANGUAGES IN SUPERVISORY CONTROL
    GIUA, A
    DICESARE, F
    IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 1995, 40 (05) : 906 - 910
  • [17] Robust Deadlock Control for Automated Manufacturing Systems With Unreliable Resources Based on Petri Net Reachability Graphs
    Liu, Gaiyun
    Li, Pei
    Li, Zhiwu
    Wu, Naiqi
    IEEE TRANSACTIONS ON SYSTEMS MAN CYBERNETICS-SYSTEMS, 2019, 49 (07): : 1371 - 1385
  • [18] Extended Reachability Graph of Petri Net for Cost Estimation
    Davidrajuh, Reggie
    2013 8TH EUROSIM CONGRESS ON MODELLING AND SIMULATION (EUROSIM), 2013, : 378 - 383
  • [19] Analysis of Unbounded Petri Net With Lean Reachability Trees
    Li, Jun
    Yu, Xiaolong
    Zhou, MengChu
    IEEE TRANSACTIONS ON SYSTEMS MAN CYBERNETICS-SYSTEMS, 2020, 50 (06): : 2007 - 2016
  • [20] Decidability analysis of some classes of extended function Petri net
    Ohta, Atsushi
    Tsuji, Kohkichi
    2012 THIRD INTERNATIONAL CONFERENCE ON NETWORKING AND COMPUTING (ICNC 2012), 2012, : 414 - 419
12345