（1）单选题
下面不正确的叙述为（）
A Buchi自动机的语言是由命题构成的无穷序列的集合
B 时间自动机的语言是由命题构成的无穷序列的集合
C 时间自动机能够对系统的时间属性进行建模
D LTL可以转换为Buchi自动机
（2）单选题
软件形式化验证的方法的优点不包括（）
A 能正确理解系统需求
B 能自动验证系统
C 不需要软件理论系统的知识
D 能够更早发现软件中存在的问题，降低修复成本
（3）单选题
模型检测方法不需要（）
A 采用自动机对系统软件建模
B 用逻辑表示系统需求
C 用检测平台自动检测
D 逻辑推理证明
（4）单选题
当前模型检测方法存在的问题不包括（）
A 状态空间爆炸问题
B 自动机建模与转换复杂问题
C 白箱检测与保密问题
D 不可判定验证问题
获取标准答案请阅读全文
未经允许不得转载！第十五章 自动机及应用--习题【含答案】 软件理论基础