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

M. Praveen & Kamal Lodaya
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$...
This data center is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.
We found no citations for this text. For information on how to provide citation information, please see our documentation.