# 系统分析与验证

【系统分析与验证笔记】线性时态逻辑LTL和计算树逻辑CTL线性时态逻辑（Linear temporal logic，简称LTL）计算树逻辑（ Computation tree logic，简称CTL）
# 系统分析与验证 LTL ctl 系统分析与验证线性时态逻辑计算数逻辑
04-24
$【系统分析与验证笔记】关于自动机的规范语言（Specification Language）有限字的自动机（Automata on Finite Words）无限字的自动机（Automata on Finite Words）NBA和 ω \omega ω-正则语言Generalized NBA（简写为GNBA）[图]$
【系统分析与验证笔记】关于自动机的规范语言（Specification Language）有限字的自动机（Automata on Finite Words）无限字的自动机（Automata on Finite Words）NBA和 ω \omega ω-正则语言Generalized NBA（简写为GNBA）
# 系统分析与验证 NFA NBA 自动机模型检测形式化验证
01-16
【系统分析与验证笔记】Data-Dependent Systems和Program Graph讲解有一个自动售货机（Beverage Vending Machine），现在需要设计一个模型，计数苏打水（soda）和啤酒（beer）的数量，如果自动售货机是空的，则返回插入的硬币（coin）
# 系统分析与验证数据以来系统 Data-Dependent Program Graph
12-18