2026-07-25T14:26:35Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:2331 2024-03-06T10:33:18Z ddc:004 open_access

Modelchecking counting properties of 1-safe nets with buffers in paraPSPACE Praveen, M. Lodaya, Kamal Petri nets Coverability Boundedness paraPSPACE We consider concurrent systems that can be modelled as $1$-safe Petri nets communicating through a fixed set of buffers (modelled as unbounded places). We identify a parameter $\ben$, which we call ``benefit depth'', formed from the communication graph between the buffers. We show that for our system model, the coverability and boundedness problems can be solved in polynomial space assuming $\ben$ to be a fixed parameter, that is, the space requirement is $f(\ben)p(n)$, where $f$ is an exponential function and $p$ is a polynomial in the size of the input. We then obtain similar complexity bounds for modelchecking a logic based on such counting properties. This means that systems that have sparse communication patterns can be analyzed more efficiently than using previously known algorithms for general Petri nets. Schloss Dagstuhl – Leibniz-Zentrum für Informatik M. Praveen and Kamal Lodaya 2009 Is Part Of LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2009.2331 urn:nbn:de:0030-drops-23314 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2331 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode