动态优先系统及其Petri网语义  

Petri Net Semantics of Dynamic Priority Systems

作　　者：李文军[1] 周晓聪[1] 李师贤[1] 马建[2] 

机构地区：[1]中山大学计算机科学系,广州510275 [2]香港城市大学商学院BPR技术中心

出　　处：《计算机学报》2001年第10期1085-1094,共10页Chinese Journal of Computers

基　　金：国家自然科学基金 ( 79910 16 1989);高等学校博士点基金 ( 99-0 18-4 1170 3)资助

摘　　要：优先关系是并发系统控制的重要手段 .文中提出一种动态优先系统 (Σ,D) ,其中 Σ是有界 Petri网 ,D是描述变迁之间优先关系的动态结构 .然后采用变换技术分别给出安全的和有界的动态优先系统的 Petri网语义 :通过引入广义补位置和优先变迁 ,并对非安全系统的某些变迁进行分解 ,根据 (Σ,D)构造相应的 Petri网 ΣD.最后利用步序列证明了 ΣD 在不破坏动态优先结构 D的规格说明约束的前提下 ,尽可能地保持了 Σ的并发语义 .We develop the concept of dynamic priority system and provide the Petri net semantics for both the safe and the bounded systems. In a dynamic priority system (Σ, D), Σ is a bounded Petri net and D is a dynamic structure describing the priorities between the transitions of Σ. Given a system (Σ, D), we construct a Petri net ΣD by adding generalized complemental places, priority transitions and additional arcs, and splitting some transitions of Σ if necessary. The aim of the construction of ΣD is that ΣD keeps the concurrent semantics of (Σ, D) as much as possible, mean-while the constraints of the specification imposed by the dynamic priority structure D will not be violated. Complemental places are useful tools to tackle bounded Petri nets. The generalized complemental place proposed is a complement of a subset of places. The number of tokens in the complement and related arcs can be amplified. The capacity of the complement can be augmented and some redundant tokens can be put into the complement. For a safe dynamic priority system, ΣD is constructed in 3 steps. Using the step sequences of net systems, we prove that ΣD has a good semantic property. For a bounded dynamic priority systems, we construct ΣD in 5 steps and its semantic property is also proved. Since there exists a counterexample showing that the reverse inclusion is not true, we also find a sufficiency condition that satisfies the reverse inclusion. Dynamic priority systems can be used as both modeling tools to build concurrent and distributed systems and semantic foundations to define prioritized operators in concurrent programming languages.

关 键 词：并发模型 动态优先系统 Petni网 形式语义 程序设计语言 

分 类 号：TP312[自动化与计算机技术—计算机软件与理论]