zbMATH — the first resource for mathematics

Modelchecking counting properties of 1-safe nets with buffers in paraPSPACE. (English) Zbl 1248.68356
Kannan, Ravi (ed.) et al., IARCS annual conference on foundations of software technology and theoretical computer science (FSTTCS 2009), December 15–17, 2009, Kanpur, India. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-13-2). LIPIcs – Leibniz International Proceedings in Informatics 4, 347-358, electronic only (2009).
Summary: 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.
For the entire collection see [Zbl 1213.68045].

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q25 Analysis of algorithms and problem complexity
Full Text: DOI Link