Petri net unfoldings

Analysis of Petri nets can be performed by means of constructing either reachable state spaces (or reachable markings) or via the process of graph-based unfolding. The prefix of a Petri net unfolding, which is an acyclic Petri net graph, contains the same information about the properties of the Petri net as the reachability graph, plus it contains information about sequence, concurrency and conflict relations between Petri net transitions and Petri net places. The advantages of the use of unfolding in practice are typically associated with the fact that the unfolding prefix is much more compact than the reachability graph of the Petri net being analysed.

Petri net unfoldings were originally introduced by Ken McMillan.[1] Later they were studied by several authors, who improved the original criterion for producing the prefix of the unfolding in terms of its compactness and hence efficient analysis.[2][3]

There are applications of Petri net unfoldings in the analysis and synthesis of concurrent systems and asynchronous circuits.[4][5] The latter is normally achieved through the use of Signal transition graphs (STGs).

References
  1. McMillan, K. L. (1993). "Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits". In von Bochmann, Gregor; Probst, David Karl (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 663. Berlin, Heidelberg: Springer. pp. 164–177. doi:10.1007/3-540-56496-9_14. ISBN 978-3-540-47572-9. S2CID 44597274.
  2. Esparza, Javier; Römer, Stefan; Vogler, Walter (2002-05-01). "An Improvement of McMillan's Unfolding Algorithm". Formal Methods in System Design. 20 (3): 285–310. doi:10.1023/A:1014746130920. ISSN 1572-8102. S2CID 15149333.
  3. Helianko, Keijo (1999). "Minimizing finite complete prefixes" (PDF).
  4. Semenov, Alexei (1997). "Verification and synthesis of asynchronous control circuits using petri net unfoldings, PhD Thesis, Newcastle University".
  5. Khomenko, Victor (2003). "Model checking based on prefixes of petri net unfoldings, PhD thesis, Newcastle University" (PDF).

Further reading
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.