基于Petri网表示的嵌入式系统模型化简规则(英文)

Reduction Rules for Petri Net Based Representation for Embedded Systems

为了提高基于Petri网表示的嵌入式模型(PRES+)验证的效率,对模型进行了保性变换,给出了一组关于PRES+模型的化简规则,这些化简规则在原模型和简化模型之间保持完全等价关系。对两个系统模型的化简结果进一步说明了这些化简规则的有效性。

The research concentrates on the aspects related to reduction rules for Petri Net based Representation for Embedded Systems （PRES＋）. The major motivation of this work is to give correctness-preservation transformations to improve the verification efficiency. It proposes a set of reduction rules to reduce PRES＋ nets to the equivalent reduced PRES＋ nets. Reductions for two system models demonstrate the efficiency of this reduction rules on practical applications.