Semilinear Home-space is Decidable for Petri Nets

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}$.