Petri网连接过程中的行为关系

THE BEHAVIOR RELATION IN CONNECTION PROCESS FOR THE PETRI NET MODEL

先前的Petri网模型的综合研究着重在性质的保持性方面,象活性、可达性和回归性.然而,系统行为关系的保持性研究应该更为重要.本文研究了Petri网模型自环连接、抑止弧连接和同步连接三种操作的行为关系,获得他们的语言关系公式,这些结果为Petri网模型综合过程中的动态行为分析提供了形式工具.

Existing research on the synthesis of Petri net models focuses on preserving system properties,such as liveness,reachability,and reversibility.Such research overlooked the importance of system behavior relation preservation models.In this paper,we discuss three important connection operations:self loops,inhibitor arcs and synchronisation,in order to model system behavior characteristics.Their behavior relation formulas have been obtained by two transformations to these operations.Furthermore,we formally prove that these three connection operations satisfy the behavior invariance.These results support a formal tool for dynamic analysis of Petri net models in synthesis process.