【摘要】线性时态逻辑(LTL)现今已被广泛运用于计算机科学领域(CS)。它常作为描述系统行为的性质语言,用在程序验证、程序综合与人工智能(AI)等研究方向。比方说,为了验证给定的系统是否满足其对应的性质规范(通常是用LTL来书写的),模型检测技术会将该性质的否定转成与其等价的Buchi自动机,把它与系统模型求交得到新的自动机,并在这新的自动机上检查其接收的语言是否为空,从而可以判定系统是否满足该性 […]