This paper addresses the following verification task: Given a graph transformation system and a class of initial graphs, can we guarantee (non-)reachability of a given other class of graphs that characterizes bad or erroneous states? Both initial and bad states are characterized by nested conditions (having first-order expressive power). Such systems typically have an infinite state space, causing the problem to be undecidable. We use abstract interpretation to obtain a finite approximation of that state space, and employ counter-example guided abstraction refinement to iteratively obtain suitable predicates for automated verification. Although our primary application is the analysis of graph transformation systems, we state our result in the general setting of reactive systems.

翻译：本文探讨以下验证任务：给定一个图变换系统及一类初始图，能否确保特定表征错误或异常状态的另一类图（不可）可达？初始状态与错误状态均通过具有一阶表达能力的嵌套条件进行描述。此类系统通常具有无限状态空间，导致该问题不可判定。我们采用抽象解释方法获取该状态空间的有限近似，并运用反例引导抽象精化技术迭代生成适用于自动化验证的谓词。尽管我们的主要应用场景是图变换系统分析，但研究结论在反应式系统的通用框架中同样成立。