科研之友
微信
新浪微博
Facebook
分享链接
摘要
为了提高基于Petri网表示的嵌入式模型(PRES+)验证的效率,对模型进行了保性变换,给出了一组关于PRES+模型的化简规则,这些化简规则在原模型和简化模型之间保持完全等价关系。对两个系统模型的化简结果进一步说明了这些化简规则的有效性。
-
单位中国科学院软件研究所; 计算机科学国家重点实验室; 山东建筑大学
为了提高基于Petri网表示的嵌入式模型(PRES+)验证的效率,对模型进行了保性变换,给出了一组关于PRES+模型的化简规则,这些化简规则在原模型和简化模型之间保持完全等价关系。对两个系统模型的化简结果进一步说明了这些化简规则的有效性。
