Petri net reachability graphs: Decidability status of FO properties

P Darondeau, S Demri, R Meyer… - … Annual Conference on …, 2011 - inria.hal.science
P Darondeau, S Demri, R Meyer, C Morvan
IARCS Annual Conference on Foundations of Software Technology and …, 2011inria.hal.science
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.
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.
inria.hal.science
以上显示的是最相近的搜索结果。 查看全部搜索结果