数值流程序中加速方法的可达性分析：处理数值输入不确定性

本文主要探讨了在数值输入数据流程序中应用抽象加速方法进行可达性分析的问题。在理论计算机科学背景下，作者聚焦于同步程序，这些程序同时涉及布尔变量和数值变量，如LUSTRE程序，这类逻辑-数值程序在安全特性验证和基于模型的测试中有广泛应用。 可达性分析在计数器模型中通常用于精确计算循环效应，但将其应用于数据流程序时，面临两个主要挑战。首先，为了分析仅包含数值变量的控制结构，需要对布尔状态进行枚举，从而简化问题。其次，由于数值输入变量的存在，引入了不确定性，这使得传统的抽象解释技术，如只提供过近似的有限状态集合，可能无法满足精确性需求。 作者针对这个问题，借鉴了Gonnord等人的抽象加速概念，扩展了这一方法。他们提出了一种处理数值输入变量非确定性的方式，通过加速技术，旨在在某些特定情况下计算出精确的可达状态集，尽管这种方法不保证总能终止。这种方法的核心是通过迭代求解X=X0post(X)的形式方程，其中X代表状态集合，X0是初始状态，post是程序相关的后置条件运算符。 然而，对于逻辑-数值程序的可达性问题，尤其是当涉及到抽象解释和加速技术的结合时，存在不可判定性。现有的两种主要方法——抽象解释和加速技术——各有优缺点。抽象解释虽然能够提供近似结果，但不保证结果的精确性；而加速技术在某些情况下能够得到精确答案，但可能存在不终止的情况。 本文的工作背景是在INRIA Rhône-Alpes的大型科研项目“科学”支持下进行的，两位作者分别提供了他们的联系信息，表明该研究是开放访问的，并被发表在《电子笔记在理论计算机科学》上，获得了CC BY-NC-ND许可。文章通过示例（如图1中的一般循环转换与加速转换对比）深入阐述了抽象加速方法在具体程序分析中的应用策略和技术细节，对于理解和改进数值输入数据流程序的可达性分析具有重要意义。