A Temporal Graph Logic for Verification of Graph Transformation Systems
A Temporal Graph Logic for Verification of Graph Transformation Systems
复制标题
用于验证图转换系统的时态图逻辑
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Alberto Lluch
中科院分区：
文献类型：
--
作者：
Paolo Baldan;A. Corradini;B. König;Alberto Lluch
我们使用合适的抽象扩展了验证图转换系统属性的方法。在原始方法中，属性被指定为命题时序逻辑的公式，其原子谓词是一元二阶图公式。我们通过考虑更具表现力的逻辑来概括这一方面，其中边缘量词和时间模态可以交织，该特征允许例如及时追踪对象的历史。在描述了可以在近似值上安全检查的逻辑片段之后，我们展示了如何将图转换系统上的逻辑验证简化为适当定义的 Petri 网上的逻辑验证。
We extend our approach for verifying properties of graph transformation systems using suitable abstractions. In the original approach properties are specified as formulae of a propositional temporal logic whose atomic predicates are monadic second-order graph formulae. We generalize this aspect by considering more expressive logics, where edge quantifiers and temporal modalities can be interleaved, a feature which allows, e.g., to trace the history of objects in time. After characterizing fragments of the logic which can be safely checked on the approximations, we show how the verification of the logic over graph transformation systems can be reduced to the verification of a logic over suitably defined Petri nets.