软件理论基础
逻辑
命题逻辑
谓词逻辑
模态逻辑
LTL(linear 线性时态逻辑)
CTL（component tree logic 分支时态逻辑）
自动机
DFA 确定有限状态自动机
NFA 非确定有限状态自动机
PDA 下推
TM
TA 时间自动机
验证
基于证明的方法
基于模型的方法
验证模型M是否具有性质φ M|=φ
自动机是一种建模方法
参考书：
计算理论导引 机械 （麻省理工）M.sipser 中北六楼中文图书借阅区 TP301.6 X119 2006
教材 打印
计算理论基础 清华 H.Rrewis 已预约
面向计算机科学的数理逻辑——系统建模与推理 机械 M.Huth M.Ryan
数理逻辑引论与归结原理 科学出版社 王国俊 已下载电子版 打印
出版社: 科学出版社; 第2版 (2009年1月1日)
ISBN: 9787030228994, 7030228995