高效的无穷状态系统一阶时态逻辑
摘要：使用时态逻辑考虑无限状态系统的规范化和验证。我们特别描述了使用一种新颖的一阶时态逻辑的参数化系统，在规范化方面即强大又切实可行以进行演绎验证。时态语言的强大之处在于它允许描述（并验证）异步系统、通讯延迟以及更复杂的性质，比如活力性和公平性。这些方面对于许多其他方法来说似乎非常困难。
作者：Clare Dixon, Michael Fisher, Boris Konev, Alexei Lisitsa
论文ID：cs/0702036
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23