时态并发约束程序的自动验证
摘要：tccp的计时并发约束语言是并发约束编程(cc)范式在时间上的扩展，可以用于指定时间至关重要的并发系统，例如反应系统。tccp可以对具有无限状态的系统进行指定。模型检测是一种能够以自动方式验证具有大量状态的有限状态系统的技术。近年来，已经有多项研究探讨了如何扩展模型检测技术以应用于具有无限状态的系统。在本文中，我们提出了一种利用tccp的计算模型的方法。基于约束的计算使我们能够定义一种方法，将模型检测算法应用于（一类）无限状态系统。我们将经典的LTL模型检测算法扩展到了为验证tccp而定义的特定逻辑和我们在本文中定义的tccp结构上。我们对时间进行了限制，以获得一个有限模型，并开发了一些示例。据我们所知，这是首个为tccp定义模型检测方法的方法。
作者：Moreno Falaschi and Alicia Villanueva
论文ID：cs/0505026
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23