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

ABSTRACT. 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 K, 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 K to be a fixed parameter, that is, the space requirement is f (K)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.

• Type: Conference
• Year: 2009
• Where: FSTTCS
• Authors: M. Praveen, Kamal Lodaya
• Keywords: 1-safe Petri Nets, FSTTCS 2009, General Petri Nets, Petri Nets, Theoretical Computer Science