We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

cs

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Semilinear Home-space is Decidable for Petri Nets

Abstract: A set of configurations $\mathbf{H}$ is an home-space for a set of configurations $\mathbf{X}$ of a Petri net if every configuration reachable from $\mathbf{X}$ can reach $\mathbf{H}$. The semilinear home-space problem for Petri nets asks, given a Petri net $A$, and semilinear sets of configurations $\mathbf{X},\mathbf{H}$ if $\mathbf{H}$ is an home-space for $\mathbf{X}$. In 1989, Davide de Frutos Escrig and Colette Johnen proved that the problem is decidable when $\mathbf{X}$ is a singleton and $\mathbf{H}$ is a finite union of linear sets using the same periods. In this paper, we show that the general problem is decidable. This result is obtained by proving a duality between the reachability problem and the non-home-space problem. More formally, we prove that for any Petri net $A$ and for any linear set of configurations $\mathbf{L}$, we can effectively compute a semilinear set $\mathbf{W}$ of configurations such that for every set $\mathbf{X}$, the set $\mathbf{L}$ is not an home-space for $\mathbf{X}$ if, and only if $\mathbf{W}$ is reachable from $\mathbf{X}$.
Subjects: Logic in Computer Science (cs.LO)
Cite as: arXiv:2207.02697 [cs.LO]
  (or arXiv:2207.02697v1 [cs.LO] for this version)

Submission history

From: Jérôme Leroux [view email]
[v1] Wed, 6 Jul 2022 14:07:43 GMT (12kb)

Link back to: arXiv, form interface, contact.