Petri Net 定义
定义 1.1 如果三元组 (S, T, W) 称为一个 Petri 网图,那么
- S 是库所的有限集合
- T 是变迁的有限集合
-
S ∪ T ≠ Φ,且 S ∩ T = Φ
- W: (S × T) ∪ (T × S) → N 为弧的多重集
流关系是弧的集合:F = {(x, y) | W(x, y) > 0}。在一些介绍 Petri 网相关文献中,弧的重度只定义为 1,并在定义 Petri 网图时使用 F 代替了 W。
定义 1.3 设 N = (S, T, F) 为一个 Petri 网图,∑ = (S, T, F, M) 称为一个标记网,其中
- M ⊆ S,称为 N 的一个标记或一个瞬态
- 若 S ∈ T,且 .x ⊆ M,x. ∩ M = Φ,称事件 x 为可触发的
- 若事件 x 被触发(称为点火),则标记网 ∑ 转化为 ∑' = (S, T, F, M'),其中 M' = (M - .x) ∪ x.,M' 也是 N 的一个标记,∑' 也是一个标记网
定义 1.2 设 N = (S, T, F) 为一个 Petri 网图,x ∈ S ∪ T,则
-
.x = {y ∈ S ∪ T | (y, x) ∈ F}
- x. = {y ∈ S ∪ T | (x, y) ∈ F}
-
.x.= .x ∪ x.
其中,.x 称为 x 的前提,x. 称为 x 的后提,.x. 称为 x 的前后提。
定义 1.4 六元组 ∑ = (S, T, F, K, W, M) 称为一个库所 / 变迁系统,简称为 P / T 系统,如果下列条件成立
- (S, T, F) 是一个 Petri 网图,S 是库所的有限集合,T 是变迁的有限集合,F 是有向弧的有限集合
-
K: S → N ∪ {ω} 是一个映射,使 S 中的每个元素 x 与一个自然数或无穷大值相对应,称为 x 的容量
- W: F → N - {0} 是一个映射,使 F 中的每条弧 f 与一个正整数对应,称为 f 的流量
- M: S → N ∪ {ω} 是一个映射,使 S 中的每个元素与一个有穷或无穷的初始标码数相对应,整个 M 称为 ∑ 的初始标记,满足 M(x) ≤ K(x)
定义 1.5 P / T 系统 ∑ = (S, T, F, K, W, M) 的运行规则如下:
- T 中任一变迁 t 被允许发生的条件是:
∀ s ∈ .t,M(s)
≥ W(s, t)
∀ s ∈ t.,M(s) ≤ K(s) - W(t, s)
其中 W(s, t) 表示从 s 到 t 的弧的流量
- 如果变迁发生前的标记为 M,则变迁发生后的标记 M' 是
M(s) - W(s, t), 若 s ∈ .t - t.
M'(s) = { M(s) + W(t, s),若 s ∈ t. - .t }
M(s), 其他
注意,这里恒要求 .t ∩ t. = Φ
- 初始标记是标记,任一标记经过变迁以后仍然变为标记
参考
[1] 李彤, 孔兵, 王黎霞等. 软件并行开发过程. 北京:科学出版社, 2003
[2] http://en.wikipedia.org/wiki/Petri_net
well-formatted doc:
http://docs.google.com/Doc?id=ddrm6c35_512f45hshcz
分享到:
相关推荐
高级软件工程(第5章形式化开发方法1Petri网定义).pptx
高级软件工程(第5章形式化开发方法1_Petri网定义).pptx
介绍了表征变迁记忆的变迁标识矩阵,用于表达故障传播路径,在此基础上从新型故障Petri网定义、关联矩阵改进、状态方程、变迁记忆表达等几个方面,论述了基于变迁记忆的掘进机故障Petri网的理论定义及技术实现。...
为了对语义Web服务组合进行形式化验证,提出一种语义Weh服务组合模型到着色Petri网组合模型的转换方法,定义了语义Web服务着色Petri网(SWS-net)。转换后的模型不仅能清晰表示服务组合中各子过程之间的逻辑关系,而且能...
建立了基于随机Petri网的装备维修排队问题的形式化描述模型, 研究了模型的简化解析分析和仿真分析方法. 结合实例分析了改进系统性能的途径, 验证了解析方法的有效性. 研究表明, 提高维修小组能力和备件满足率是提高...
为了将数据流和控制流在同一个模型中明确标识,将经典Petri嗣的4元组结构扩展为7元组,定义一 ...用UPPAAL进行形式化验证。验证结果表明火车控制系统具有可达性和安全性,说明 建立的模型是台理有效的。
基于面向对象Petri网的UML建模技术,折建峰,简炜,UML作为通用面向对象建模语言缺乏形式化的模型验证和分析工具,Petri网有严格的数学定义和多种模型的验证方法。本文提出一种从UML的�
首先对陶瓷企业能量碳流模型进行分析, 然后给出模型的形式化定义及规则说明, 建立了基于广义模糊Petri网的陶瓷生产过程能量碳流模型, 最后以典型的烧成系统为例加以说明模型的运用, 对整个过程的能量碳流进行了动态...
针对一些复杂知识系统的知识不确定性及知识规则数量多的特点,在模糊Petri网(FPN)的基础上给出了面向对象模糊Petri网(object-oriented fuzzy Petri net, OOFPN)的形式化定义及其知识表示和知识推理。通过面向对象...
首先给出仿真剧情的形式化定义, 并分析仿真剧情可能存在的错误类型;其次给出仿真剧情到高级Petri网的映射途径, 并给出基于高级Petri网的仿真剧情校核准则和算法,此外,还给出实现仿真剧情动态校核的推理规则和机制;...
给出了基于有色Petri网的混合安全策略的形式化定义;并通过一个系统实例阐述了如何利用该方法对系统的混合安全性进行分析和验证。无论是在系统的设计阶段还是实现阶段,该方法都能够有效地提升系统的混合安全性。
为解决目前UCON模型和策略规范存在系统应用功能与安全策略集成性差、缺少事后义务和无并发性控制问题,通过定义行为、安全和并发规则,提出了一种扩展的使用控制策略,采用有色Petri网技术,达到形式化定义、分析的...
提出一种在模型驱动开发过程中的形式化语义描述方法。该方法利用元建模技术,形式化...将描述框架用于模型转换规则的定义以及元模型的分析与验证,并以简单Petri网为例,说明该方法可以有效地支持模型转换和代码生成。
扩展了Petri网的形式语义,区别定义了状态型和数值型库所,区别定义了变迁的激发和抑制状态,引入了无前置、一元和组合判断规则,同时根据形式化定义将模型自动转换为检验程序实施安全性验证。最后给出了以上方法在...
工作流模型的语义定义采用Petri网表达,给出工作流网的形式化描述。工作流系统的设计模型采用UML进行定义,对于业务逻辑、执行过程、数据结构分别采用用户实例图、顺序图、类图进行描述。在工作流的实现上,采用软...
将车-地通信场景抽象为MAS,给出了场景中车-地主体Agent的内部推理过程和形式化定义,采用CPN Tools工具建立了层次化结构HCPN模型,使车-地通信过程、MAS整体行为以及车-地主体内部推理流程可视化。通过对模型状态...
首先给出仿真剧情的形式化定义,并分析仿真剧情可能存在的错误类型;其次给出仿真剧情到高级Petri网的映射途径,并给出基于高级Petri网的仿真剧情校核准则和算法,此外,还给出实现仿真剧情动态校核的推理规则和机制...
使用分层Petri网进行建模,利用顺序图对消息传递进行分析,采用SOFL对非形式化和半形式化的系统描述逐步求精。讨论了基于分层Petri网的Web服务,定义了分层服务网、分层Web服务相关概念,描述了用于Web服务软件需求...