Coverability synthesis in parametric Petri nets. (English) Zbl 1442.68133
Meyer, Roland (ed.) et al., 28th international conference on concurrency theory. CONCUR 2017, Berlin, Germany, September 5–8, 2017. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 85, Article 14, 16 p. (2017).
Summary: 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 R. Valk and M. Jantzen [Lect. Notes Comput. Sci. 188, 234–258 (1985; Zbl 0613.68029)]. 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.
For the entire collection see [Zbl 1372.68016].
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 R. Valk and M. Jantzen [Lect. Notes Comput. Sci. 188, 234–258 (1985; Zbl 0613.68029)]. 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.
For the entire collection see [Zbl 1372.68016].
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
Citations:
Zbl 0613.68029References:
| [1] | Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi. Parametric real-time reasoning. In {\it ACM Symposium on Theory of Computing}, pages 592-601, 1993. · Zbl 1310.68139 |
| [2] | Florent Avellaneda and Rémi Morin. Vector Addition Systems with States vs. Petri Nets. report, Laboratoire d’informatique Fondamentale de Marseille - LIF, October 2012. |
| [3] | Ahmed Bouajjani and Richard Mayr. Model checking lossy vector addition systems. In {\it 16th Annual Symposium on Theoretical Aspects of Computer (STACS’09)}, pages 323-333, Trier, Germany, March 1999. Springer. · Zbl 0926.03035 |
| [4] | Laura Bozzelli and Salvatore La Torre. Decision problems for lower/upper bound paramet ric timed automata. {\it Formal Methods in System Design}, 35(2):121-151, 2009. · Zbl 1186.68245 |
| [5] | Giovanni Chiola, Susanna Donatelli, and Giuliana Franceschinis. On Parametric PT nets and their Modelling Power. {\it 12th International Conference Application and Theory of Petri} {\it Nets (ICATPN’91)}, page 206, 1991. |
| [6] | Jean-Michel Couvreur, Denis Poitrenaud, and Pascal Weil. {\it Branching Processes of General} {\it Petri Nets}, pages 129-148. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011. · Zbl 1330.68199 |
| [7] | Nicolas David, Claude Jard, Didier Lime, and Olivier H. Roux. Discrete parameters in Petri nets. In {\it The 36th International Conference on Application and Theory of Petri Nets and} {\it Concurrency (Petri Nets 2015)}, volume 9115 of {\it LNCS}, pages 137-156. Springer, Brussels, Belgium, June 2015. · Zbl 1432.68303 |
| [8] | Stéphane Demri. On selective unboundedness of VASS. {\it Journal of Computer and System} {\it Sciences}, 79(5):689-713, August 2013. · Zbl 1285.68094 |
| [9] | Leonard Eugene Dickson. Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. {\it American Journal of Mathematics}, 35(4):413-422, 1913. URL: http://www.jstor.org/stable/2370405. · JFM 44.0220.02 |
| [10] | Alain Finkel and Jean Goubault-Larrecq. Forward analysis for WSTS, part I: Comple tions. In {\it 26th Annual Symposium on Theoretical Aspects of Computer Science (STACS’09)}, volume 3 of {\it Leibniz International Proceedings in Informatics}, pages 433-444, Freiburg, Ger many, February 2009. Leibniz-Zentrum für Informatik. · Zbl 1236.68183 |
| [11] | Alain Finkel and Jean Goubault-Larrecq. Forward analysis for WSTS, part II: complete WSTS. {\it Logical Methods in Computer Science}, 8(3), 2012. · Zbl 1248.68352 |
| [12] | Alain Finkel and Jérôme Leroux. Recent and simple algorithms for Petri nets. {\it Software &} {\it Systems Modeling}, 14(2):719-725, 2015. |
| [13] | Gilles Geeraerts, Alexander Heußner, M. Praveen, and Jean-François Raskin. {\it ω}-Petri nets: Algorithms and complexity. {\it Fundam. Inform.}, 137(1):29-60, 2015. · Zbl 1335.68172 |
| [14] | :16 |
| [15] | Jean Goubault-Larrecq. On a Generalization of a Result by Valk and Jantzen. Technical report, LSV, 2009. |
| [16] | Aleksandra Jovanović, Didier Lime, and Olivier H. Roux. Integer Parameter Synthesis for Real-Time Systems. {\it IEEE Transactions on Software Engineering}, 41(5):445-461, May 2015. · Zbl 1381.68121 |
| [17] | Richard M. Karp and Raymond E. Miller. Parallel program schemata. {\it Journal of Computer} {\it and System Sciences}, 3(2):147-195, 1969. · Zbl 0198.32603 |
| [18] | Marco Ajmone Marsan, Gianfranco Balbo, Gianni Conte, Susanna Donatelli, and Giuliana Franceschinis. {\it Modelling with Generalized Stochastic Petri Nets}. John Wiley & Sons, Inc., New York, NY, USA, 1st edition, 1994. |
| [19] | Christophe Reutenauer. {\it The mathematics of Petri nets}. Prentice-Hall, Inc., April 1990. · Zbl 0694.68007 |
| [20] | Walter J. Savitch. Relationships between nondeterministic and deterministic tape complex ities. {\it Journal of Computer and System Sciences}, 4(2):177-192, April 1970. · Zbl 0188.33502 |
| [21] | Rüdiger Valk and Matthias Jantzen. The residue of vector sets with applications to decid ability problems in Petri nets. {\it Acta Informatica}, 21(6):643-674, 1985. · Zbl 0545.68051 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
