真正的即时LTL模型检查
摘要：基于自动机的LTL模型检测的一种新算法：一方面构建LTL公式的广义B"{u}chi自动机的否定，另一方面进行空集检查。我们的算法首先将LTL公式转化为线性弱交替自动机；交替自动机的配置对应于广义B"{u}chi自动机的位置，并使用Tarjan算法的变体来判断过渡系统和自动机的乘积是否存在接受运行。由于避免了对B"{u}chi自动机的显式构建，我们的方法可以显著提高大型LTL公式的运行时间和内存消耗。该算法已在SPIN模型检查器中实现，我们还对一些基准示例进行了实验结果的呈现。
作者：Moritz Hammer (IFI-LMU), Alexander Knapp (IFI-LMU), Stephan Merz (INRIA Lorraine - LORIA)
论文ID：cs/0511061
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23