基于自动机的程序终止性检验

Yu-Fang Chen, Matthias Heizmann, Ondrej Lengal, Yong Li, Ming-Hsien Tsai, Andrea Turrini, and Lijun Zhang (2018): Advanced Automata-Based Algorithms for Program Termination Checking. PLDI 2018, 135-150

背景：程序的终止性一直是计算机科学领域研究的热点。一般的程序终止性问题也可规约为图灵机的停机问题。由于图灵机的停机问题不可判定，所以程序的终止性问题也没有通用完备的算法来求解。于是很多科学家从而关注于提出部分正确却不完备的算法来判断一个输入程序是否终止，即通过程序秩函数(ranking function)的存在性来证明程序是否可以终止，如果秩函数存在，则表明返回程序终止，否则程序终止性未知。2014年德国学者Matthias Heizmann等人提出使用Buchi自动机对程序进行建模，并通过采样的方法对Buchi自动机里面的路径进行采样来逐条通过秩函数的方式证明路径的终止性。证明终止的路径会经过扩展为Buchi自动机之后从原自动机里面删除，当路径全部删除时即证明了程序可终止。此方法是当前最好的程序终止性证明算法，实现此方法的工具Ultimate也是2017年SV-COMP比赛终止性类别的冠军。

科学难题：此方法虽然将寻找程序秩函数的过程简化，即我们只需要寻找单条循环路径的秩函数即可。但是整个程序终止性的复杂度却转移到了路径的删除那一部分，因为路径删除里面会现将路径扩展为Buchi自动机然后使用Buchi自动机取补算法删除扩展的路径，其复杂度一般是PSPACE-complete，这个过程是整个分析过程的效率瓶颈。

重要突破：我们首先提出分阶段路径扩展方案，即现将证明终止的路径尽量扩展为更特殊的Buchi自动机，依次为简单单接收状态Buchi自动机，确定性Buchi自动机，半确定Bucih自动机，最后是Buchi自动机。他们取补的复杂度依次为输入自动机状态数的常数复杂度，线性复杂度，指数复杂度以及最后是一般的PSPACE-complete。这个多阶段扩展有效提升了高复杂度的取补运算的效率。其次，经过分析发现多阶段扩展过程经常产生半确定性Buchi自动机，因此我们提出了一个更高效的半确定Buchi自动机的取补算法，从而进一步提高了取补过程的效率。通过上述的结果，我们有效提高了当前的工具Ultimate的程序终止性的分析能力。​该成果发表在计算机程序理论顶级会议PLDI 2018上。