On the Decidability Status of Reachability and Coverability in Graph Transformation Systems
On the Decidability Status of Reachability and Coverability in Graph Transformation Systems
复制标题
论图转换系统中可达性和覆盖性的可判定性现状
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Jan Stückrath
中科院分区：
文献类型：
--
作者：
N. Bertrand;G. Delzanno;B. König;Arnaud Sangnier;Jan Stückrath
我们研究图变换系统，一个强大的无限状态模型的可达性问题的可判定性问题。对于一个固定的初始配置，我们考虑一个完全指定的配置和配置，满足给定的模式（覆盖性）的可达性。前者是任何计算模型的一个基本问题，后者是严格相关的安全性能的验证，其中的模式指定了一个坏的配置的无限集。在本文中，我们重新制定的结果，例如，的上下文无关的图形文法和并发模型，如Petri网，在更一般的设置图转换系统和研究新的结果，通过增加约束的形式减少规则的模型类。
We study decidability issues for reachability problems in graph transformation systems, a powerful infinite-state model. For a fixed initial configuration, we consider reachability of an entirely specified configuration and of a configuration that satisfies a given pattern (coverability). The former is a fundamental problem for any computational model, the latter is strictly related to verification of safety properties in which the pattern specifies an infinite set of bad configurations. In this paper we reformulate results obtained, e.g., for context-free graph grammars and concurrency models, such as Petri nets, in the more general setting of graph transformation systems and study new results for classes of models obtained by adding constraints on the form of reduction rules.