Liveness of Safe Object Nets

Issue title: Concurrency Specification and Programming (CS&P)

Article type: Research Article

Authors: Köhler-Bußmeier, Michael | Heitmann, Frank

Affiliations: University of Hamburg, Department for Informatics, Vogt-Kölln-Straße 30, D-22527 Hamburg. koehler@informatik.uni-hamburg.de

Note: [] Address for correspondence: University of Hamburg, Department for Informatics, Vogt-Kölln-Straße 30, D-22527 Hamburg

Abstract: In this paper we study the complexity of the liveness problem for safe Elementary Object Nets (EOS). Object nets are Petri nets which have Petri nets as tokens. They are called elementary if the net system has a two levelled structure. The concept of safeness bounds the number of tokens which may reside on a place. PSPACE-hardness of the liveness problem for safe EOS directly follows from the related result for safe p/t nets. We then devise a polynomial space algorithm for this problem and indeed for every property that can be expressed in the temporal logic CTL.

DOI: 10.3233/FI-2011-579

Journal: Fundamenta Informaticae, vol. 112, no. 1, pp. 73-87, 2011