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.FSTTCS.2019.47
URN: urn:nbn:de:0030-drops-116094
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11609/
Go to the corresponding LIPIcs Volume Portal

Leroux, Jérôme

Distance Between Mutually Reachable Petri Net Configurations

pdf-format:
LIPIcs-FSTTCS-2019-47.pdf (0.5 MB)

Abstract

Petri nets are a classical model of concurrency widely used and studied in formal verification with many applications in modeling and analyzing hardware and software, data bases, and reactive systems. The reachability problem is central since many other problems reduce to reachability questions. In 2011, we proved that a variant of the reachability problem, called the reversible reachability problem is exponential-space complete. Recently, this problem found several unexpected applications in particular in the theory of population protocols. In this paper we revisit the reversible reachability problem in order to prove that the minimal distance in the reachability graph of two mutually reachable configurations is linear with respect to the Euclidean distance between those two configurations.

BibTeX - Entry

@InProceedings{leroux:LIPIcs:2019:11609,
  author =	{J{\'e}r{\^o}me Leroux},
  title =	{{Distance Between Mutually Reachable Petri Net Configurations}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{47:1--47:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Arkadev Chattopadhyay and Paul Gastin},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2019/11609},
  URN =		{urn:nbn:de:0030-drops-116094},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.47},
  annote =	{Keywords: Petri nets, Vector addition systems, Formal verification, Reachability problem}
}

Keywords: Petri nets, Vector addition systems, Formal verification, Reachability problem
Collection: 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)
Issue Date: 2019
Date of publication: 04.12.2019

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