DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2017.18

Goal-Driven Unfolding of Petri Nets

Authors: Thomas Chatain and Loïc Paulevé

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

Abstract

Unfoldings provide an efficient way to avoid the state-space explosion due to interleavings of concurrent transitions when exploring the runs of a Petri net. The theory of adequate orders allows one to define finite prefixes of unfoldings which contain all the reachable markings. In this paper we are interested in reachability of a single given marking, called the goal. We propose an algorithm for computing a finite prefix of the unfolding of a 1-safe Petri net that preserves all minimal configurations reaching this goal. Our algorithm combines the unfolding technique with on-the-fly model reduction by static analysis aiming at avoiding the exploration of branches which are not needed for reaching the goal. We present some experimental results.

Cite as

Thomas Chatain and Loïc Paulevé. Goal-Driven Unfolding of Petri Nets. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 18:1-18:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{chatain_et_al:LIPIcs.CONCUR.2017.18,
  author =	{Chatain, Thomas and Paulev\'{e}, Lo\"{i}c},
  title =	{{Goal-Driven Unfolding of Petri Nets}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{18:1--18: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.18},
  URN =		{urn:nbn:de:0030-drops-77730},
  doi =		{10.4230/LIPIcs.CONCUR.2017.18},
  annote =	{Keywords: model reduction; reachability; concurrency; unfoldings; Petri nets; automata networks}
}

Search Results

Documents authored by Chatain, Thomas

Goal-Driven Unfolding of Petri Nets

Abstract

Cite as

Thanks for your feedback!

Could not send message