Petri Net Reachability Graphs: Decidability Status of First Order Properties

Christophe Morvan (Universit\'e Paris-est Marne-la-Vall\'ee); CNRS; ENS Cachan; INRIA); Philippe Darondeau (INRIA Rennes Bretagne Atlantique); Roland Meyer (University of Kaiserslautern); Stephane Demri (LSV

arxiv: 1210.2972 · v2 · pith:KZXJQMG7new · submitted 2012-10-10 · 💻 cs.LO

Petri Net Reachability Graphs: Decidability Status of First Order Properties

Philippe Darondeau (INRIA Rennes Bretagne Atlantique) , Stephane Demri (LSV , ENS Cachan , CNRS , INRIA) , Roland Meyer (University of Kaiserslautern) , Christophe Morvan (Universit\'e Paris-est Marne-la-Vall\'ee) This is my paper

classification 💻 cs.LO

keywords decidabilitygraphspetriproblemsreachabilitystatusableanalysis

0 comments

read the original abstract

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.

This paper has not been read by Pith yet.

Petri Net Reachability Graphs: Decidability Status of First Order Properties

discussion (0)