论文部分内容阅读
形式化模型的行为语义确定了系统行为的执行方式，是系统性质验证的基础。本文基于Petri网模型，提出行为的一种描述方式——标准变迁集语义。这种语义提供了Petri网发生行为的一种等价类划分:等价的发生序列具有相同的标准集序列。我们证明这种语义是良定义的、对划分是可靠和完备的。其良定义性适用于所有长度可数的发生序列，并产生一种向前的移动操作。我们发现，这种语义是对安全网系统下Foata范式的一种扩展，其对行为发生的次序无关性进行抽象，从而可以在次序无关性的任意子集上产生变体;其次，和Foata范式不同的是，它必须显式地说明建立在行为动态使能的条件上。
我们对标准变迁集语义下的性质判定进行考察，这些性质包括可达性（包含死锁状态）、活性、家态等Petri网的基本性质。我们发现，对于这些性质，标准变迁集语义相比传统的交错语义可以在较短的路径上进行验证，因此，标准变迁集语义可以作为交错语义的替代，我们将之与偏序规约技术相结合进行状态空间的缩减。我们进一步考察了这种缩减技术在一种特殊的网系统-自由选择网上的缩减效果。
我们构造了标准变迁集语义下的Petri网状态迁移图，即其标准状态空间，继而在该语义下就宽度搜索树和深度搜索树的构造做出初步探索。我们发现，标准变迁集语义下的状态空间压缩了到达所有状态的路径长度，但由于状态重访问题的存在，这种构造式的空间探索相比交错语义下的探索并不总占有优势。同时，相关研究工作告诉我们，寻找行为空间的符号化是研究标准变迁集语义的一个有效方法。