基于状态空间等价类的有色Petri网特性验证

在有色Petri网的状态空间中,有时一些状态具有相似的行为,这些状态可以用定义在状态空间上的一致的等价关系来表达,对每个等价状态类只研究它的一个代表状态的行为,这极大地减小了有色Petri网的状态空间。但是,通常对一个给定的等价关系是否为一致的验证都是通过用户的经验人工进行的,这不但容易产生错误,而且效率低下。该文依据普通状态图和等价类状态图的标记迁移系统关系,对状态空间一致性等价定义的计算机辅助验证做了深入的讨论,给出了相应的结果。

Verification of Coloured Petri Nets Based on Equivalence Classes of State Spaces

In state spaces of Coloured Petri Nets,some states induce similar behaviors.The similarity can be expressed by defining an equivalence relation on the set of states.The behavior of a representative can be taken as that of the equivalence class.So the state spaces are often much smaller than the ordinary state spaces.However,the verification of an equivalence specification consistency is generally by user experiences,so it is prone to error and inefficient.Based on the labelled transition systems of the ordinary state spaces and the equivalence classes,this paper introduces the aided-computer verification for consistent equivalence specification,and achieves a few results.