Choice-free Petri nets: A model for deterministic concurrent systems with bulk services and arrivals
Choice-free Petri nets: A model for deterministic concurrent systems with bulk services and arrivals
复制标题
DOI：
10.1109/3468.553226
复制
发表时间：
1997-01-01
影响因子：
--
通讯作者：
Silva, M
中科院分区：
文献类型：
--
作者：
Teruel, E;Colom, JM;Silva, M
在离散事件系统中，那些表现出并发性的系统尤其具有挑战性，需要使用形式化方法来处理它们，Petri网是一种完善的形式化方法。结构理论旨在通过连接结构和行为特性来克服并发系统分析所固有的状态空间爆炸问题。迄今为止，这主要是对普通网络的一些子类成功地实现了，然而，权重在许多情况下是一种建模方便，本文研究了具有批量服务和到达的并发系统子类的形式化模型，该模型在结构上避免了冲突。介绍了结构结果和处理这些结果的技术，包括正确行为属性的结构条件和通过仅在结构上推理来检查一般行为属性的统一框架。
Among discrete event systems, those exhibiting concurrency are especially challenging, requiring the use of formal methods to deal with them, Petri nets are a well-established such formalism. Structure theory aims at overcoming the state space explosion problem, inherent to the analysis of concurrent systems, by bridging structural and behavioral properties. To date, this has been successfully achieved mainly for some subclasses of ordinary nets, Nevertheless weights are a modeling convenience in many situations, In this paper we study a formal model for a subclass of concurrent systems with bulk services and arrivals which structurally avoids conflicts. Structural results and techniques for dealing with them are introduced, These include structural conditions on properties of correct behavior and a unified framework for checking general behavioral properties by reasoning solely on the structure.