常见的几种动态行为语义模型 基于逻辑的形式化方法 一阶线性/分支时序逻辑、模态μ演算、分布时序逻辑、TLA以及 线性逻辑 用来描述系统的生命期约束性质，如系统的安全性、活性、公平性及不 变性等 在逻辑的形式公理系统上，还可以进行系统的特性推理 基于刻画系统并发行为的模型和方法 CCS,CSP,ACP等基于进程代数 I/O自动机、Buchi自动机等自动机模型 Petri nets 口Actor模型 Tian Zhang Nanjing UniversityTian Zhang @ Nanjing University 4 常见的几种动态行为语义模型 „ 基于逻辑的形式化方法 ‰ 一阶线性/分支时序逻辑、模态μ演算、分布时序逻辑、TLA以及 线性逻辑 – 用来描述系统的生命期约束性质,如系统的安全性、活性、公平性及不 变性等 – 在逻辑的形式公理系统上,还可以进行系统的特性推理 „ 基于刻画系统并发行为的模型和方法 ‰ CCS,CSP,ACP等基于进程代数 ‰ I/O自动机、Büchi自动机等自动机模型 ‰ Petri nets ‰ Actor模型