zbMATH — the first resource for mathematics

Extending the Rackoff technique to affine nets. (English) Zbl 1354.68190
D’Souza, Deepak (ed.) et al., IARCS annual conference on foundations of software technology and theoretical computer science (FSTTCS 2012). Selected papers based on the presentations at the 32nd conference, Hyderabad, India, December 15–17, 2012. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-47-7). LIPIcs – Leibniz International Proceedings in Informatics 18, 301-312 (2012).
Summary: We study the possibility of extending the Rackoff technique to Affine nets, which are Petri nets extended with affine functions. The Rackoff technique has been used for establishing Expspace upper bounds for the coverability and boundedness problems for Petri nets. We show that this technique can be extended to strongly increasing Affine nets, obtaining better upper bounds compared to known results. The possible copies between places of a strongly increasing Affine net make this extension non-trivial. One cannot expect similar results for the entire class of Affine nets since coverability is Ackermann-hard and boundedness is undecidable. Moreover, it can be proved that model checking a logic expressing generalized coverability properties is undecidable for strongly increasing Affine nets, while it is known to be Expspace-complete for Petri nets.
For the entire collection see [Zbl 1256.68007].

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q25 Analysis of algorithms and problem complexity
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI