License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2012.301
URN: urn:nbn:de:0030-drops-38688
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3868/
Go to the corresponding LIPIcs Volume Portal

Bonnet, Rémi ; Finkel, Alain ; Praveen, M.

Extending the Rackoff technique to Affine nets

pdf-format:
29.pdf (0.5 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{bonnet_et_al:LIPIcs:2012:3868,
  author =	{R{\'e}mi Bonnet and Alain Finkel and M.  Praveen},
  title =	{{Extending the Rackoff technique to Affine nets}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012) },
  pages =	{301--312},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{Deepak D'Souza and Telikepalli Kavitha and Jaikumar Radhakrishnan},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2012/3868},
  URN =		{urn:nbn:de:0030-drops-38688},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.301},
  annote =	{Keywords: Complexity of VASS, Affine nets, Rackoff technique, model checking, coverability, boundedness}
}

Keywords: Complexity of VASS, Affine nets, Rackoff technique, model checking, coverability, boundedness
Collection: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)
Issue Date: 2012
Date of publication: 14.12.2012

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI