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 条
  • [21] Decidability of opacity verification problems in labeled Petri net systems
    Tong, Yin
    Li, Zhiwu
    Seatzu, Carla
    Giua, Alessandro
    AUTOMATICA, 2017, 80 : 48 - 53
  • [22] Basis Marking Representation of Petri Net Reachability Spaces and Its Application to the Reachability Problem
    Ma, Ziyue
    Tong, Yin
    Li, Zhiwu
    Giua, Alessandro
    IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2017, 62 (03) : 1078 - 1093
  • [23] Leveraging polyhedral reductions for solving Petri net reachability problems
    Amat, Nicolas
    Dal Zilio, Silvano
    Le Botlan, Didier
    INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2023, 25 (01) : 95 - 114
  • [24] Petri net reachability checking is polynomial with optimal abstraction hierarchies
    Küngas, P
    ABSTRACTION, REFORMULATION AND APPROXIMATION, PROCEEDINGS, 2005, 3607 : 149 - 164
  • [25] Leveraging polyhedral reductions for solving Petri net reachability problems
    Nicolas Amat
    Silvano Dal Zilio
    Didier Le Botlan
    International Journal on Software Tools for Technology Transfer, 2023, 25 : 95 - 114
  • [26] A graph theoretic approach to reachability problem with Petri net unfoldings
    Miyamoto, T
    Kumagai, S
    IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 1996, E79A (11) : 1809 - 1816
  • [27] LOCAL AREA NETWORK IMPLEMENTATION OF PETRI NET REACHABILITY ANALYSIS
    ANNEBERG, L
    YAPRAK, E
    MICROELECTRONICS AND RELIABILITY, 1991, 31 (2-3): : 491 - 499
  • [28] A Technique for Generating the Reduced Reachability Graph of Petri Net Models
    Ahmad, Farooq
    Huang, Hejiao
    Wang, Xiao-long
    Anwer, Waqas
    2008 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN AND CYBERNETICS (SMC), VOLS 1-6, 2008, : 3635 - 3640
  • [29] Property analysis of logic Petri nets by marking reachability graphs
    Yuyue Du
    Yuhui Ning
    Frontiers of Computer Science, 2014, 8 : 684 - 692
  • [30] A primitive recursive algorithm for the general Petri net reachability problem
    Bouziane, Z
    39TH ANNUAL SYMPOSIUM ON FOUNDATIONS OF COMPUTER SCIENCE, PROCEEDINGS, 1998, : 130 - 136
12345