论文标题
关于培养皿网及其Ackermannian复杂性的房屋空间问题
On the Home-Space Problem for Petri Nets and its Ackermannian Complexity
论文作者
论文摘要
一组配置$ h $是一组配置$ x $ apetri net的主页空间，如果可以从$ x $中触及的每种配置（在）$ x $中的任何配置（在）$ h $中的某些配置中。彼得里网的半线性房屋空间问题询问，鉴于培养皿网和半连接的配置$ x $，$ h $，如果$ h $是$ x $的房屋空间。 1989年，戴维·德·弗洛托斯·埃克里格（David de Frutos Escrig）和科莱特·约翰宁（Colette Johnen）证明，当$ x $是单身人士而$ h $是与同一时期的线性套装有限的联盟时，问题是可决定的。在本文中，我们证明了一般的（半线性）问题是可决定的。通过证明可及性问题与非居家空间问题之间的双重性来获得该结果。特别是，我们证明，对于任何Petri网和任何半线性的配置$ h $，我们可以有效地计算一个半连接的$ c $配置的$ c $，称为$ h $的不可访问的核心，因此，对于$ x $，对于$ x $而言，对于$ x $而言，$ x $ nif，$ x $ nif，$ x $ nif，$ c $ nif，$ c $都不是$ c $。我们表明，与达到可达性问题的既定关系产生了（半线性）家庭空间问题的ackermann完整性。为此，我们还表明，鉴于具有初始标记的培养皿网，可以在Ackermannian时期构建一组最小的可触及标记。
A set of configurations $H$ is a home-space for a set of configurations $X$ of aPetri net if every configuration reachable from (any configuration in) $X$ can reach (some configuration in) $H$. The semilinear home-space problem for Petri nets asks, given a Petri net and semilinear sets of configurations $X$, $H$, if $H$ is a home-space for $X$. In 1989, David de Frutos Escrig and Colette Johnen proved that the problem is decidable when $X$ is a singleton and $H$ is a finite union of linear sets with the same periods. In this paper, we show that the general (semilinear) problem is decidable. This result is obtained by proving a duality between the reachability problem and the non-home-space problem. In particular, we prove that for any Petri net and any semilinear set of configurations $H$ we can effectively compute a semilinear set $C$ of configurations, called a non-reachability core for $H$, such that for every set $X$ the set $H$ is not a home-space for $X$ if, and only if, $C$ is reachable from $X$. We show that the established relation to the reachability problem yields the Ackermann-completeness of the (semilinear) home-space problem. For this we also show that, given a Petri net with an initial marking, the set of minimal reachable markings can be constructed in Ackermannian time.
