Vector Addition Systems (VAS) or equivalently petri-nets are a popular model for representing concurrent systems. Many important decidability results about VAS were obtained by considering geometric properties of their reachability sets, i.e. the set of configurations reachable from some initial configuration $c_0$. For example, in 2012 Jerome Leroux proved that if a configuration $c_t$ is not reachable, then there exists a semilinear inductive invariant separating the reachability set from $c_t$. This gave an alternative proof of decidability of the reachability problem. The paper introduced the class of petri-sets, proved that reachability sets are petri-sets, and that petri-sets have this property. In a follow-up paper in 2013, Jerome Leroux again used the class of petri-sets to prove that if a reachability set is semilinear, then a representation of it can be computed. In this paper, we utilize the class of petri-sets to answer the opposite type of question: Even if the reachability set is non-semilinear, what form can it have? We give another proof that semilinearity of the reachability set is decidable, which was first shown by Hauschildt in 1990. We prove that reachability sets can be partitioned into nicely shaped sets we call almost-hybridlinear, and how to utilize this to decide semilinearity.
翻译:矢量添加系统( VAS) 或等效的花瓣内网系统( VAS) 是代表并行系统的流行模式。 VAS 的许多重要变异性结果都是通过考虑其可达性组的几何特性而获得的, 即从某些初始配置 $c_ 0 美元中可以达到的一组配置。 例如, 2012 Gerome Lerouux 证明, 如果配置 $c_ t 美元无法达到, 那么就会存在一个半线性导引导性, 将可达性从 $c_ tline 中分离出来。 这给出了可达性问题的可变性的替代证据。 纸张引入了类 石油套, 证明可达性组是固定的, 证明可达性组是固定的, 而在2013 年的后续文件中, Gerem Loux再次使用类 来证明, 如果可达性组是半线性, 然后可以计算出它的可达标值 。 在本文中, 我们使用该类的花状组可以回答相反的问题: 即使可达性组的可达性组是固定的, 也显示为可达标的可达性。