Abstract: Attribute graph grammar is widely used in modeling and analysis in software design phase. However, ordinary propositional temporal logic cannot directly express the response specification with associated attributes. This paper proposes a novel approach which supports the verification of such properties with associate attributes in general graph grammar transformation systems. It introduces a special indicator node and attributes as well as a set of rules to translate the properties into common propositional temporal logic properties. Therefore the corresponding properties can be verified. It illustrates the approach via a motivating example with the popular graph based model checker GROOVE. The result demonstrates the feasibility of this approach.

Key words: attribute graph grammar, model checking, associate attributes

摘要： 属性图文法广泛应用在软件设计阶段建模和分析阶段。命题式时序逻辑（propositional temporal logic）无法直接表达建模实体包含随时间演化的关联属性反应式规约，提出一种可支持通用图文法转换系统中相应规约的验证方法，通过引入标记节点及属性，将包含相应关联属性的规约公式等价转换为命题式时序逻辑，从而可以间接支持该类型规约的验证。以流行的对象式属性图文法模型检测工具GROOVE为平台，结合启发案例，验证了所提出方法的有效性。

关键词: 属性图文法, 模型检测, 关联属性