Petri Net Reachability Graphs: Decidability Status of First Order Properties

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 probl...

Full description

Bibliographic Details

Published in:	Logical Methods in Computer Science
Main Authors:	Philippe Darondeau, Stephane Demri, Roland Meyer, Christophe Morvan
Format:	Article
Language:	English
Published:	Logical Methods in Computer Science e.V. 2012-10-01
Subjects:	computer science - logic in computer science f.1.1 f.4.1
Online Access:	https://lmcs.episciences.org/872/pdf