可重构位置/转换系统与图语法的显式状态模型检查

### 可重构位置/转换系统与图语法的显式状态模型检查 #### 可重构位置/转换系统的转换 在可重构位置/转换系统中，存在多种类型的网络转换。位置/转换（P/T）系统的范畴PTSys，即带有标记的位置/转换网，对于严格P/T态射的类Mstrict而言，是一个弱粘合HLR范畴。这使得诸如局部丘奇 - 罗瑟定理、并行性定理和并发定理等丰富的粘合HLR系统理论能够应用于可重构P/T系统内的网络转换。 网络转换可以从多种方式进行考量： - **不同Petri网类或建模形式之间的转换**：将Petri网转换为不同的Petri网类（如从一种类型的Petri网转换到另一种），或者转换为其他建模形式，反之亦然。这类转换已经得到了深入研究，并产生了许多重要成果。 - **同一网类内的转换**：在不改变网类的情况下，将一个网转换为另一个网，常用于构建层次结构（如通过约简或抽象），或者用于检测网络的特定属性。 - **直接改变网络的转换**：类似于图转换中直接以任意方式改变网络的转换，是HLR系统的一种特殊情况。这种一般方法可以限制为保留特定属性（如安全性或活性）的转换。 还有一些相关的转换方法，例如提出以特定方式改变网络以保留特定语义属性，像开放Petri网的行为保留重构、等效（I/O -）行为、不变量或活性等。“网和规则作为令牌”的概念也被引入，用于在系统运行时对网络结构的变化进行建模。 #### 图语法的显式状态模型检查 我们主要关注软件模型检查，特别是面向对象程序的模型检查。虽然模型检查在硬件验证方面取得了很大成功，并且在软件领域也得到了广泛研究，但软件中存在一些硬件中没有的方面，现有模型检查理论对这些方面的覆盖较差，例如堆和栈上的动态（去）分配。 经典的模型检查方法基于具有固定数量命题的命题逻辑，无法直接表示可能涉及可变、可能无界数量对象的系统。而图是建模相关结构的自然选择，因为面向对象编程的教科书通常使用图进行说明。通过采用图转换，可以直接在图上使用规则来建模面向对象系统的计算步骤，而不是通过中间建模语言。 这一见解启发了GROOVE项目和工具的诞生。该项目基于图语法直接生成状态空间，与其他方法不同，既不使用现有模型检查器的输入语言来翻译图规则，也不尝试在图语法层面证明属性。 #### 简单图的转换 在建模系统状态时，我们面临图形式主义的选择。为了充分利用现有的图转换理论，特别是代数方法，选择能产生（弱）粘合HLR范畴的定义是比较理想的，如多排序图或属性图。但在GROOVE项目中，我们选择了简单图和单推出来转换，原因如下： - 在面向对象系统的操作语义领域，带标识的边用处不大。 - 与一阶逻辑最直接的联系是将边解释为二元谓词，这也忽略了边的标识。 下面是简单图的相关定义： - **简单图**：简单图是一个元组⟨V, E⟩，其中V ⊆ Node是节点的集合，E ⊆ V × Label × V是边的集合。对于边e = (v, a, w) ∈ EG，我们分别用src(e) = v、lab(e) = a和tgt(e) = w表示其源、标签和目标。 - **（部分）图态射**：给定