Petri Net Reachability Graphs: Decidability Status of First Order Properties

摘要

We investigate the decidability and complexity status of model-checkingproblems on unlabelled reachability graphs of Petri nets by consideringfirst-order and modal languages without labels on transitions or atomicpropositions on markings. We consider several parameters to separate decidableproblems from undecidable ones. Not only are we able to provide precise bordersand a systematic analysis, but we also demonstrate the robustness of our prooftechniques.