### 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$...