Darondeau, Philippe and Demri, Stephane and Meyer, Roland and Morvan, Christophe - Petri Net Reachability Graphs: Decidability Status of First Order Properties

lmcs:872 - Logical Methods in Computer Science, October 22, 2012, Volume 8, Issue 4
Petri Net Reachability Graphs: Decidability Status of First Order Properties

Authors: Darondeau, Philippe and Demri, Stephane and Meyer, Roland and Morvan, Christophe

We investigate the decidability and complexity status of model-checking problems on unlabelled reachability graphs of Petri nets by considering first-order and modal 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.


Source : oai:arXiv.org:1210.2972
DOI : 10.2168/LMCS-8(4:9)2012
Volume: Volume 8, Issue 4
Published on: October 22, 2012
Submitted on: March 22, 2012
Keywords: Computer Science - Logic in Computer Science,F.1.1,F.4.1


Share

Consultation statistics

This page has been seen 52 times.
This article's PDF has been downloaded 91 times.