摘要

我们展示了用于计算带有标签的图的相似性的算法。相似关系适用于不同的激活系统模式。对于有限图，我们提出了一种用于计算n个点m条边的图（假设m≥nm\ge nm≥n）的相似关系的O(mn)算法。为了高效地表示无限图，我们提出了一个标志性的相似性检查过程，如果有无限关系存在则停止。我们证明了2D矩形自动机，它对具有连续环境的离散反应系统进行建模，定义了具有有限相似关系的有效呈现的无限图。因此，对于2D矩形自动机，精化问题和CTL模型检查问题是可判定的。(We show that 2D rectangular automata, which model discrete reactive systems with continuous environments, define effectively presented infinite graphs with finite similarity relations.It follows that the refinement problem and the CTL model-checking problem are decidable for 2D rectangular automata.)

1. Introduction

一个带有标签的图G=(V,E,A,⟨⋅⟩)G=(V,E,A,\langle\cdot\rangle)G=(V,E,A,⟨⋅⟩)由（可能无限的）节点集合VVV，边集E⊆V2E \subseteq V^2E⊆V2，节点标签集合AAA和将节点映射到标签的函数⟨⋅⟩\langle\cdot\rangle⟨⋅⟩组成。我们将post(v)={u∣(v,u)∈E}post(v)=\lbrace u|(v,u)\in E \rbracepost(v)={u∣(v,u)∈E} 作为节点vvv的后继集合. 节点集上的二元关系≤⊆V2\leq\subseteq V^2≤⊆V2