模态逻辑是经典命题逻辑和一阶谓词逻辑的拓展形式。
一阶线性时态逻辑（FOLTL）是一阶谓词逻辑的扩展。
计算树逻辑（CTL）是一种离散、分支时间、命题时态逻辑。
Z语言为系统建立基于状态的模型。模型的三个主要组成部分是输入，输出和状态。
Z语言表示抽象的要素总体上可分为两类：基于集合理论的集合、关系、函数、序列和包，以及Z独有的模式。
Z语言中，自由类型用于递归定义新类型。
自由类型：：=常量1|...|常量n|函数1《输入对象1》|...|函数m《输入对象m》
Petri网分为位置/迁移Petri网和高级Petri网两类。
任何系统都可抽象为两类元素：状态和事件。
原文：http://www.cnblogs.com/1305yyf/p/4278430.html