时间逻辑与模型检查
克里普克结构
K=
符号逻辑
自然语言：
模棱两可的
悖论
代数逻辑
时间逻辑控制*
路径量词
A：对于此状态的每个无限路径（任意路径中的状态）
E：这个状态有一条无限的路径
时间运算符
xp:p保持在下一个状态
FP:P在未来的某些州持有
gp:p将来在所有州都持有
qup:fp，q在所有状态下保持，直到p保持。
时间逻辑控制
A、E和E、F、G、U必须成对站立
时态逻辑LTL（线性时态逻辑）
不e
只有一条路
算法挑战
对称性约简
飞行状态空间探索
部分降阶
假设保证推理
符号方法
BDD
抽象
模型检查的未来
合成（根据规范生成程序）
归纳、模型测量
人工智能？？？？
建模软件
断言
转换：
启用条件：预测
转换：多重分配
A>B->（B，C）：=（C，D）
执行：状态序列
LTL
☐盒子，永远，G
：钻石，最终，F
：下一个时间，x
有限词上的自动机
自动机
非确定性
确定性
正确性条件
我们希望找到一个模型满足规范的正确性条件。
模型语言：L（模型）
规范语言：L（规范）
我们需要：L（型号）L（规格）
程序执行符合规范的序列所有序列