Modelchecking counting properties of 1-safe nets with buffers in paraPSPACE

Authors M. Praveen, Kamal Lodaya

Thumbnail PDF


  • Filesize: 264 kB
  • 12 pages

Document Identifiers

Author Details

M. Praveen
Kamal Lodaya

Cite AsGet BibTex

M. Praveen and Kamal Lodaya. Modelchecking counting properties of 1-safe nets with buffers in paraPSPACE. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 347-358, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)


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.
  • Petri nets
  • Coverability
  • Boundedness
  • paraPSPACE


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads