We introduce the well structured problem as the question of whether a model (here a counter machine) is well structured (here for the usual ordering on integers). We show that it is undecidable for most of the (Presburger-defined) counter machines except for Affine VASS of dimension one. However, the strong well structured problem is decidable for all Presburger counter machines. While Affine VASS of dimension one are not, in general, well structured, we give an algorithm that computes the set of predecessors of a configuration; as a consequence this allows to decide the well structured problem for 1-Affine VASS.
翻译:我们引入良结构问题,即询问一个模型(此处为计数器机)是否具有良结构(此处针对整数的通常序)。我们证明,对于大多数(Presburger定义的)计数器机而言,该问题不可判定,但一维仿射VASS除外。然而,强良结构问题对于所有Presburger计数器机都是可判定的。尽管一维仿射VASS通常并非良结构,我们仍给出一种算法来计算某配置的前驱集;由此,该算法能够判定1-仿射VASS的良结构问题。