第一部分 Petri网——基本概念 1
第1章 引言 2
第2章 Petri网的实质特征 4
2.1 局部确定性和并发 5
2.2 图形表示和代数表示 7
2.3 并发、冲突和混惑 10
2.4 细化和组合 11
2.5 网射 16
第3章 直观模型 21
3.1 常量弧网 21
3.2 库所／变迁网 23
3.3 有色网 25
3.4 折叠 28
4.1 库所／变迁网的形式化定义 30
第4章 基本定义 30
4.2 常量弧网的形式化定义 31
4.3 有色网的形式化定义 33
第5章 性质 40
5.1 基本性质 40
5.2 分析方法介绍 44
第6章 本书总览 55
第二部分 建模 59
第7章 引言 60
第8章 实例解说建模和分析技术 62
8.1 网、优化和抽象 62
8.2 库所／变迁网和资源管理 67
8.3 有色网、抽象和展开 72
9.1 构建块 77
第9章 技术 77
9.2 结合网 79
9.3 高级网 82
9.4 分解网 85
9.5 小结 85
第10章 方法 86
10.1 面向状态建模 86
10.2 面向事件的建模 97
10.3 面向对象建模 106
第11章 实例研究 115
11.1 面向状态的方法 117
11.2 面向事件的方法 120
11.3 面向对象方法 125
第12章 小结 130
第三部分 验证 131
第13章 引言：验证所涉及的问题 132
13.1 网的分类 132
13.2 性质 135
13.3 方法分类 137
13.4 验证过程 142
13.5 概述 143
第14章 基于状态空间的方法与模型检验 144
14.1 性质、时态逻辑及公平性 144
14.2 on-the-fly方法 155
14.3 基于偏序的方法 158
14.4 符号化和参数化方法 174
14.5 实现问题 192
14.6 综合及一般性总结评注 197
第15章 结构方法 199
15.1 网系统归约 200
15.2 线性代数技术 205
15.3 虹吸和陷阱 214
15.4 网子类的分析 216
15.5 不变量和有色Petri网的归约 222
第16章 演绎与基于进程代数的方法 229
16.1 代数网的重写语义 230
16.2 断言推理 244
16.3 授权逻辑 262
16.4 线性逻辑和Petri网 268
16.5 利用进程代数验证Petri网模型 277
第17章 小结 290
第四部分 确认和执行 291
第18章 引言 292
19.1 软件生命周期和确认 293
第19章 系统工程和确认 293
19.2 确认 294
19.3 一种方法——原型建立 295
19.4 工具 298
第20章 网的运行 301
20.1 集中控制 303
20.2 将控制分发给库所 304
20.3 将控制分发给边 308
20.4 多线程和同步 309
20.5 异步 310
20.6 小结 311
第21章 代码生成 312
21.1 对于代码生成的Petri网方法 313
21.2 Petri网的划分算法 317
21.3 Petri网中代码生成的一些方面 323
21.4 高级网中的代码生成 333
21.5 小结 337
第22章 小结 339
第五部 分应用领域 341
第23章 引言 342
23.1 工作中应用Petri网 342
23.2 应用领域 342
第24章 柔性制造系统 345
24.1 领域概览 345
24.2 在FMS中使用Petri网 348
24.3 设计方法 352
24.4 小结 363
第25章 工作流系统 364
25.1 领域概述 364
25.2 动机 366
25.3 设计方法学 368
25.4 工作流分析 375
25.5 实例学习：Sagitta-2000案例 385
25.6 小结 386
第26章 电信系统 388
26.1 领域概述 388
26.2 动机 391
26.3 设计方法学 392
26.4 分析 401
26.5 小结 404
第27章 小结 405
27.1 公共建模问题 405
27.2 共享的分析结果 406
术语表 407
参考文献 422