License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2017.14
URN: urn:nbn:de:0030-drops-77831
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7783/
Go to the corresponding LIPIcs Volume Portal

David, Nicolas ; Jard, Claude ; Lime, Didier ; Roux, Olivier H.

Coverability Synthesis in Parametric Petri Nets

pdf-format:
LIPIcs-CONCUR-2017-14.pdf (0.6 MB)

Abstract

We study Parametric Petri Nets (PPNs), i.e., Petri nets for which some arc weights can be parameters. In that setting, we address a problem of parameter synthesis, which consists in computing the exact set of values for the parameters such that a given marking is coverable in the instantiated net.

Since the emptiness of that solution set is already undecidable for general PPNs, we address a special case where parameters are used only as input weights (preT-PPNs), and consequently for which the solution set is
downward-closed. To this end, we invoke a result for the representation of
upward closed set from Valk and Jantzen.
To use this procedure, we show we need to decide universal coverability,
that is decide if some marking is coverable for every possible values of the parameters.
We therefore provide a proof of its EXPSPACE-completeness,
thus settling the previously open problem of its decidability.

We also propose an adaptation of this reasoning to the case of
parameters used only as output weights (postT-PPNs).
In this case, the condition to use this procedure can be reduced to the decidability of the existential coverability,
that is decide if there exists values of the parameters making a given marking coverable.
This problem is known decidable but we provide here a cleaner proof, providing its EXPSPACE-completeness, by reduction to Omega Petri Nets.

BibTeX - Entry

@InProceedings{david_et_al:LIPIcs:2017:7783,
  author =	{Nicolas David and Claude Jard and Didier Lime and Olivier H. Roux},
  title =	{{Coverability Synthesis in Parametric Petri Nets}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{14:1--14:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Roland Meyer and Uwe Nestmann},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7783},
  URN =		{urn:nbn:de:0030-drops-77831},
  doi =		{10.4230/LIPIcs.CONCUR.2017.14},
  annote =	{Keywords: Petri net, Parameters, Coverability, Unboundedness, Synthesis}
}

Keywords: Petri net, Parameters, Coverability, Unboundedness, Synthesis
Collection: 28th International Conference on Concurrency Theory (CONCUR 2017)
Issue Date: 2017
Date of publication: 01.09.2017

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