摘要：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.
