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 条
  • [41] A slicing-based approach to enhance Petri net reachability analysis
    Lee, WJ
    Kim, HN
    Cha, SD
    Kwon, YR
    JOURNAL OF RESEARCH AND PRACTICE IN INFORMATION TECHNOLOGY, 2000, 32 (02): : 131 - 143
  • [42] Bouziane's transformation of the Petri net reachability problem and incorrectness of the related algorithm
    Jancar, Petr
    INFORMATION AND COMPUTATION, 2008, 206 (11) : 1259 - 1263
  • [43] Analysis for reachability problem of bounded Petri net using key constraints method
    Lan, Qianyi
    Qin, Haisheng
    Zhang, Xiaoling
    2007 IEEE INTERNATIONAL CONFERENCE ON CONTROL AND AUTOMATION, VOLS 1-7, 2007, : 941 - 945
  • [44] On the Petri net realization of context-free graphs
    Darondeau, P
    THEORETICAL COMPUTER SCIENCE, 2001, 258 (1-2) : 573 - 598
  • [45] A TOOL OF PETRI NET GRAPHS REPRESENTATION IN MANUFACTURING CONTEXT
    HEBRARD, A
    BOUREY, JP
    GENTINA, JC
    RAIRO-AUTOMATIQUE-PRODUCTIQUE INFORMATIQUE INDUSTRIELLE-AUTOMATIC CONTROL PRODUCTION SYSTEMS, 1992, 26 (03): : 209 - 226
  • [46] A new approach to analyze the reachability of Petri net and its use in equipment support
    Wang Yanlei
    Chen Chunliang
    Zhang Danyang
    Proceedings of the First International Conference on Maintenance Engineering, 2006, : 941 - 945
  • [47] A Reachability-Decidable Petri Net Modeling Method for Discrete Event Systems
    Su, Yue
    Zhou, MengChu
    Qi, Liang
    Wisniewski, Remigiusz
    IEEE TRANSACTIONS ON SYSTEMS MAN CYBERNETICS-SYSTEMS, 2025, 55 (01): : 453 - 464
  • [48] Partial Petri Net Languages and their Properties
    Mahadeer A.
    Arulprakasam R.
    Dare V.R.
    International Journal of Information Technology, 2024, 16 (6) : 3663 - 3676
  • [49] STP-based approach to modeling and reachability analysis of a class of petri net systems
    Han X.-G.
    Chen Z.-Q.
    Zhang K.-Z.
    Liu Z.-X.
    Zhang Q.
    1600, Beijing University of Posts and Telecommunications (39): : 72 - 76
  • [50] Proof by model: a new knowledge-based reachability analysis methodology for Petri net
    Chao, Daniel Yuh
    Chi, Yen-Ping
    Yu, Tsung-Hsien
    Yu, Li-Chih
    Lee, Mike Y. J.
    IMA JOURNAL OF MATHEMATICAL CONTROL AND INFORMATION, 2017, 34 (04) : 1277 - 1298
12345