4.1.2 分支时序逻辑（CTL）：状态量化与路径分支建模（E, A前缀）

文档摘要

4.1.2 分支时序逻辑（CTL）：状态量化与路径分支建模（E, A前缀）在形式化验证的深水区里，时间从来不是一条线性的溪流——它是一棵不断分叉的树。你站在某个系统状态上眺望未来，看到的不是唯一的明天，而是无数种可能的轨迹：有的路径上系统永远保持安全，有的路径上故障终将爆发，有的路径上恢复机制必然触发，也有的路径上死锁无可避免。分支时序逻辑（Computation Tree Logic, CTL）正是为这种“站在节点看分叉”的直觉而生的语言。它不满足于说“最终会怎样”，而是执着追问：“是否存在某条执行路径，使得……？”或“是否在所有可能的未来中，都必然……？”。