形式化方法与程序验证 · 小纸条

选一章打印。双面打印（按长边翻页）后沿虚线剪开，每张卡片正面题目、背面答案。

第 1 页 · 正面（题目）

1Kripke结构与可达状态

闭卷重建Kripke结构与可达状态的对象、公式、算例、算法与失败边界。

2线性时间与分支时间

闭卷重建线性时间与分支时间的对象、公式、算例、算法与失败边界。

3LTL的X、F、G、U

闭卷重建LTL的X、F、G、U的对象、公式、算例、算法与失败边界。

4CTL算子与不动点

闭卷重建CTL算子与不动点的对象、公式、算例、算法与失败边界。

5公平性约束

闭卷重建公平性约束的对象、公式、算例、算法与失败边界。

6性质模式与自然语言翻译

闭卷重建性质模式与自然语言翻译的对象、公式、算例、算法与失败边界。

7反例路径与循环后缀

闭卷重建反例路径与循环后缀的对象、公式、算例、算法与失败边界。

第 1 页 · 背面（答案）

对象：LTL对每条执行路径谈时间顺序；CTL可量化“存在/所有”分支。；公式：LTL:□◇p；CTL:AG EF p。；算例：一个状态有成功和失败两后继：EF success真，AF success未必真。；边界：把存在路径说成所有路径；混写A/E到LTL公式。。

对象：模型检测以带标签的状态转移系统表示并只检查初态可达部分。；公式：K=(S,S0,R,L)。；算例：4状态中从s0只能到s1,s2，s3孤立，可达状态3个。；边界：把不可达坏状态当实现反例；转移关系不全。。

对象：CTL模型检查可用前驱算子和最小/最大不动点计算满足状态集合。；公式：EF p=μZ.(p∨EX Z)。；算例：若s0→s1→s2且p只在s2，反向迭代三轮覆盖s2,s1,s0。；边界：方向反成后继搜索；在环上错误提前停止。。

对象：X下一步、F最终、G始终、U直到；无限路径语义需逐位置解释。；公式：p U q要求未来某时q且此前p持续。；算例：序列p,p,q中p U q成立；永远p但无q时强until不成立。；边界：把F理解为有限时间上界；弱until与强until混同。。

对象：常见模式有不变、响应、先行、缺席和存在；先选作用域再实例化事件。；公式：response:□(P→◇Q)。；算例：“每次请求最终应答”是全局响应；不是◇(P→Q)。；边界：公式比需求强/弱却未用示例路径检查。。

对象：公平性排除永远忽略已持续启用动作的不合理路径，但属于额外环境假设。；公式：weak fairness: continuously enabled⇒eventually taken。；算例：锁请求一直可用却调度永不执行，在弱公平模型中被排除。；边界：用公平假设掩盖实际饥饿调度器。。

对象：LTL反例通常是有限前缀加循环后缀lasso，表示无限坏执行。；公式：ρ=s0…sk(sl…sk)^ω。；算例：前缀3状态、循环2状态的存储表示含5个状态条目。；边界：只展示最后坏状态，丢失为何永不满足活性。。