【发布时间】：2022-10-06 16:06:06
【问题描述】：
我是模型检查领域的新手。我想知道为什么在插值和有界模型检查中更喜欢使用线性时间逻辑属性。为什么不能直接使用命题逻辑？
标签： logic temporal model-checking
【发布时间】：2022-10-06 16:06:06
【问题描述】：
您也可以将自己限制在命题逻辑中，但是您无法表达模型的有趣属性。
命题逻辑比时间逻辑更不具表现力。在命题逻辑中，您只能描述一种情况/状态/世界，并且模型检查非常容易：给定当前状态（即一组真命题），您只需要评估一个命题公式。
相比之下，时间逻辑像LTL 这样可以谈论未来和过去，像 Gφ 这样的运营商说“φ 在未来永远是真的”。时间逻辑模型不仅是当前状态，而且是对之前情况以及它将如何发展的描述（过渡关系）。
【讨论】：