Search Results

Documents authored by Lime, Didier

Document
DOI: 10.4230/LIPIcs.CONCUR.2017.14
Coverability Synthesis in Parametric Petri Nets

Authors: Nicolas David, Claude Jard, Didier Lime, and Olivier H. Roux

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

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.
Cite as

Nicolas David, Claude Jard, Didier Lime, and Olivier H. Roux. Coverability Synthesis in Parametric Petri Nets. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 14:1-14:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{david_et_al:LIPIcs.CONCUR.2017.14,
  author =	{David, Nicolas and Jard, Claude and Lime, Didier and Roux, Olivier H.},
  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 =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.14},
  URN =		{urn:nbn:de:0030-drops-77831},
  doi =		{10.4230/LIPIcs.CONCUR.2017.14},
  annote =	{Keywords: Petri net, Parameters, Coverability, Unboundedness, Synthesis}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.17
Lazy Reachability Analysis in Distributed Systems

Authors: Loïg Jezequel and Didier Lime

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
We address the problem of reachability in distributed systems, modelled as networks of finite automata and propose and prove a new algorithm to solve it efficiently in many cases. This algorithm allows to decompose the reachability objective among the components, and proceeds by constructing partial products by lazily adding new components when required. It thus constructs more and more precise over-approximations of the complete product. This permits early termination in many cases, in particular when the objective is not reachable, which often is an unfavorable case in reachability analysis. We have implemented this algorithm in an early prototype and provide some very encouraging experimental results.
Cite as

Loïg Jezequel and Didier Lime. Lazy Reachability Analysis in Distributed Systems. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 17:1-17:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{jezequel_et_al:LIPIcs.CONCUR.2016.17,
  author =	{Jezequel, Lo\"{i}g and Lime, Didier},
  title =	{{Lazy Reachability Analysis in Distributed Systems}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{17:1--17:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.17},
  URN =		{urn:nbn:de:0030-drops-61545},
  doi =		{10.4230/LIPIcs.CONCUR.2016.17},
  annote =	{Keywords: Reachability analysis, Compositional verification, Automata}
}
Document
Informal Presentation
DOI: 10.4230/OASIcs.SynCoP.2015.103
Discrete Parameters in Petri Nets (Informal Presentation)

Authors: Nicolas David, Claude Jard, Didier Lime, and Olivier H. Roux

Published in: OASIcs, Volume 44, 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) (2015)

Abstract
With the aim of significantly increasing the modeling capability of Petri nets, we suggest models that involve parameters to represent the weights of arcs, or the number of tokens in places. We call these Petri nets parameterised nets or PPNs. Indeed, the introduction of parameters in models aims to improve genericity. It therefore allows the designer to leave unspecified aspects, such as those related to the modeling of the environment. This increase in modeling power usually results in greater complexity in the analysis and verification of the model. Here, we consider the property of coverability of markings. Two general questions arise: "Is there a parameter value for which the property is satisfied?" and "Does the property hold for all possible values of the parameters?". We first study the decidability of these issues, which we show to be undecidable in the general case. Therefore, we also define subclasses of parameterised networks, based on restriction of the use of parameters, depending on whether the parameters are used on places, input or output arcs of transitions or combinations of them. Those subclasses have therefore a dual interest. From a modeling point of view, restrict the use of parameters to tokens, outputs or inputs can be seen as respectively processes or synchronisation of a given number of processes. From a theoretical point of view, it is interesting to introduce those subclasses of PPN in a concern of completeness of the study. We study the relations between those subclasses and prove that, for some subclasses, certain problems become decidable, making these subclasses more usable in practice.
Cite as

Nicolas David, Claude Jard, Didier Lime, and Olivier H. Roux. Discrete Parameters in Petri Nets (Informal Presentation). In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, p. 103, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{david_et_al:OASIcs.SynCoP.2015.103,
  author =	{David, Nicolas and Jard, Claude and Lime, Didier and Roux, Olivier H.},
  title =	{{Discrete Parameters in Petri Nets}},
  booktitle =	{2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
  pages =	{103--103},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-82-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{44},
  editor =	{Andr\'{e}, \'{E}tienne and Frehse, Goran},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.103},
  URN =		{urn:nbn:de:0030-drops-56046},
  doi =		{10.4230/OASIcs.SynCoP.2015.103},
  annote =	{Keywords: Petri nets, Parameters, Coverability}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact