Better abstractions for timed automata
我们考虑时间自动机的可达性问题。这个问题的一个标准解决方案涉及计算一个搜索树，其节点是区域的抽象。这些抽象保留了自动机状态空间上的底层模拟关系。出于有效性和效率的原因，它们由自动机的保护中发生的最大下限和上限（LU-边界）参数化。我们考虑Behrmann等人定义的aLU抽象。由于这种抽象可能会产生非凸集，因此尚未在实现中使用。我们证明了aLU抽象是最大的抽象方面的LU边界是健全的和完整的可达性。我们还提供了一个有效的技术，使用aLU抽象来解决可达性问题。
2016-07-28 cs.FL cs.LO
Effective Stochastic Automata Model Checking by Interval Abstraction (extended version)
Universidad Nacional de Córdoba（科尔多瓦国立大学）；CONICET（国家科学研究委员会）；University of Twente（特温特大学）
提出一种结合可细化区间抽象与“大时间步”语义的随机自动机模型检测方法，为最大/最小可达概率提供上下界，实验表明对非平凡示例有效。
2026-07-02 cs.LO
Repairing Timed Automata Clock Guards through Abstraction and Testing
时间自动机（TA）是一种广泛使用的形式化描述具有时间需求的系统。然而，准确地指定系统可能是困难的，因为用户可能不知道触发状态转换的确切时钟约束。在这项工作中，我们假设用户已经指定了一个TA，并且他希望根据可以查询接受的oracle验证它。假设用户只写了错误的保护转换（即，TA的结构是正确的），用于正确TA的搜索空间可以由参数时间自动机（PTA）表示，即，一个TA，其中一些常数是参数化的。该论文提出了一种过程，i）提取PTA pta中的初始（故障）TA taint; ii）生成一些测试数据（即，定时跟踪）; iii）用oracle评估迹线的正确评估; iv）使用IMITATOR工具来合成对pta的参数的一些约束phi; v）从phi实例化TA tarep作为最终修复的模型。实验表明，该方法能够成功地部分修复用户的初始设计。
2019-06-27 cs.LO
Zone-based verification of timed automata: extrapolations, simulations and what next?
时间自动机是由Rajeev Schmidt和David Dill在90年代初提出的。在过去的几十年里，时间自动机已经成为事实上的模型，用于验证实时系统。时间自动机的算法是基于使用区域作为符号表示的状态空间的遍历。由于状态空间是无限的，终止依赖于产生可达状态的有限表示的有限抽象。获得有限抽象的第一个解决方案是基于区域的外推，并已在行业实力工具Uppaal中实现。在过去的十年中，出现了一种基于区域之间模拟的不同方法，并已在完全开源的工具中实现。这种基于模拟的方法已经为时间自动机的可达性和活性带来了新的有效算法，并且还扩展到更丰富的模型，如加权时间自动机和具有对角约束和更新的时间自动机。在这篇文章中，我们调查的外推和模拟技术，并讨论了未来的一些开放的挑战。
2022-07-15 cs.LO
Cost Preserving Bisimulations for Probabilistic Automata
概率自动机构成了并发概率系统的通用和优雅的模型。他们配备了一个组合理论支持抽象，使弱概率互模拟作为参考概念，总结抽象的效果。本文考虑了增加成本的概率自动机。它扩展了概率自动机中弱转换的概念，使得沿着弱转换产生的成本被捕获。这就产生了成本保持和成本约束的变化弱概率双相似性，我们建立组合属性相对于并行组合。此外，多项式时间的决策算法，提出了，可以有效地用于计算马尔可夫决策过程中的组合方式的回报约束抽象。
2015-02-16 cs.FL cs.LO
Automated Predicate Abstraction for Real-Time Models
我们提出了一种技术，旨在自动计算谓词抽象密集的实时模型表示为网络的时间自动机。我们使用的CIPM算法在我们以前的工作，计算新的不变量的时间自动机控制位置和修剪模型，计算谓词抽象的模型。我们这样做，考虑到控制位置和他们的新计算的不变量的信息。
2009-11-17 cs.FL cs.LO
Interpolant Tree Automata and their Application in Horn Clause Verification
本文研究了凸多面体域上的抽象解释与插值树自动机相结合的Horn子句验证的抽象-精化方案。这些技术以前已经单独应用，但在本文中以一种新的方式相结合。内插树自动机的作用是在精化过程中提供一个伪反例的概括，捕获一组可能无限的伪反例迹。在我们的方法中，这些痕迹，然后消除使用的Horn子句的变换。我们比较这种方法与其他两种方法，其中之一使用插值树自动机的算法跟踪抽象和细化，而另一个使用抽象的解释没有概括步骤的凸多面体的域。一些霍恩子句验证问题的实验结果的评价表明，插值树自动机与抽象解释的组合给出了一些增加的验证工具的力量，而有时会产生的性能开销。
2016-07-10 cs.LO
Design of a Distributed Reachability Algorithm for Analysis of Linear Hybrid Automata
提出了一种新的线性混合自动机可达性分析分布式算法d-IRA的设计。最近的工作迭代松弛抽象（IRA）的杠杆分配的计算问题之间的多个计算节点，在一个非冗余的方式进行仔细的不可行性分析对应的伪反例的线性规划。d-IRA算法是抵抗多个计算节点的失败。实验结果为该技术的成功应用提供了有力的证据。
2007-10-19 cs.LO
Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction
本文研究了实时的【形】系统的安全性验证与综合问题。我们介绍实时的【形】程序，这些程序由可以执行离散和实值变量赋值的指令组成。它们足够通用，可以捕获有趣的时间系统类，如时间自动机，秒表自动机，时间（d）Petri网和混合自动机。我们提出了一种使用轨迹抽象细化的半算法来解决实时的【形】程序的可达性验证问题和参数综合问题。所有提出的算法已经实施，我们已经进行了一系列的实验，比较我们的新方法的性能，以国家的最先进的工具，在经典的可达性，鲁棒性分析和参数合成定时系统。我们表明，我们的新方法提供了解决方案，这些问题是无法解决的，目前最先进的工具。
2020-07-21 cs.FL cs.LO cs.SY
Automata Theory Meets Barrier Certificates: Temporal Logic Verification of Nonlinear Systems
我们认为时间逻辑验证（可能是非线性的）动态系统在连续的状态空间。我们的方法结合了基于自动机的验证和所谓的屏障证书的使用。基于自动机的验证允许将验证任务分解为连续状态空间上的有限的简单约束集合。反过来，这些约束的满足可以（可能是保守的）通过适当构造的屏障证书来证明。因此，我们的方法，再加上基于优化的搜索屏障证书，允许计算验证的动态系统对时间逻辑属性，同时避免显式抽象的动力学通常在文献中做。
2014-03-14 cs.FL cs.LO
Modal Specifications for Probabilistic Timed Systems
模态自动机是一个经典的形式化模型，基于组件的系统，配备了丰富的规范理论支持抽象，细化和组合推理。近年来，模态自动机的定量变量被引入到嵌入式和移动系统的基于组件的设计的说明和推理中。这些分别概括了定时和概率系统的模态规范理论。在本文中，我们定义了一个模态规约语言的组合概率时间系统，称为抽象概率时间自动机，推广现有的形式主义。我们引入适当的语法和语义细化的概念，并讨论我们的规约语言的一致性，也相对于时间发散。我们确定了我们的模型，我们定义的抽象，结合和并行组合的基本操作的子类，并显示几个组合的结果。
2013-06-12 cs.FL cs.LO
Abstraction Refinement for Trace Inclusion of Infinite State Systems
\emph{data automaton}是一个有限自动机，配备了在无限数据域范围内的变量（计数器或寄存器）。数据自动机的轨迹是在自动机的执行期间由计数器取得的字母符号和值的交替序列。本文所解决的问题是包含在这样的自动机识别的痕迹（数据语言）之间的集合。由于该问题在一般情况下是不可判定的，我们给出了一个基于抽象加细的半算法，该算法被证明是可靠的和完备的，但不能保证其终止性。我们已经实现了我们的技术在一个~原型工具，并在几个非平凡的例子显示出可喜的成果。
2015-10-21 cs.FL cs.LO
Active Learning of Abstract System Models from Traces using Model Checking [Extended]
我们提出了一种新的主动模型学习方法来生成抽象的系统实现，有限状态自动机（FSA），从执行轨迹。给定一个实现和一组可观察的系统变量，生成的自动机承认给定变量上的所有系统行为，并以保持实现的不变量的形式提供有用的见解。为了实现这一点，所提出的方法使用一个可插拔的模型学习组件，可以从一组给定的跟踪生成FSA。然后从正在构建的FSA中提取编码完整性假设的条件，并使用软件模型检验通过检查其真值来评估其完整性程度。这会生成新的轨迹，以表达任何缺失的行为。新的跟踪数据用于迭代地细化抽象，直到所有系统行为都被学习的抽象所接受。为了评估这种方法，我们逆向工程一组公开的Simulink Stateflow模型，从他们的C实现。
2021-12-11 cs.FL cs.LO
Automatic Synthesis of Switching Controllers for Linear Hybrid Automata
Università di Napoli “Federico II”（那不勒斯费德里科二世大学）
针对线性混合自动机，提出基于多面体抽象状态空间的符号不动点程序，自动生成满足安全目标的切换控制器，并证明每次迭代的终止性。
2011-08-04 cs.FL cs.LO cs.SY
Logical Characterization of Coherent Uninterpreted Programs
一个未解释的程序（UP）是一个程序，其语义定义在理论上的未解释的功能。这是等价性检查、编译器优化和程序验证中常用的抽象。虽然简单，但该模型足够强大，可以对计数器自动机进行编码，因此不可判定。最近，一类UP程序，称为相干，已被提出并证明是可判定的。我们提供了一个替代的，合乎逻辑的表征，这一结果。具体来说，我们证明了每一个相干程序是一个有限状态系统的双相似。此外，一个连贯程序的归纳不变量可以用一个公式表示，该公式的项的深度至多为1。我们还表明，原来的证明，通过自动机，只适用于一元未解释的功能的程序。虽然这项工作是纯理论的，它提出了一种新颖的抽象，是完整的连贯的程序，但可以合理地用于任意的未解释（和部分解释）的程序。
2021-07-26 cs.FL cs.LO
Neural Abstractions
University of Oxford（牛津大学）；University of Birmingham（伯明翰大学）
我们提出了一种新的方法，使用神经网络来表示其动态的抽象的非线性动力学模型的安全验证。神经网络以前曾被广泛用作逼近器;在这项工作中，我们更进一步，首次将它们用作抽象。对于一个给定的动力学模型，我们的方法合成一个神经网络，通过确保一个任意紧，正式认证的近似误差的范围overapproximates其动态。为此，我们采用了一个反例引导归纳合成过程。我们表明，这产生了一个神经ODE与非确定性的干扰，构成了一个正式的抽象的具体模型进行分析。这保证了一个基本属性：如果抽象模型是安全的，即，没有达到不期望状态的任何初始化轨迹，则具体模型也是安全的。通过使用带有ReLU激活函数的神经常微分方程作为抽象，我们将非线性动力学模型的安全验证问题转化为带有仿射动力学的混合自动机的安全验证问题，并使用SpaceEx进行验证。我们证明了我们的方法在现有的基准非线性模型上对成熟的工具Flow* 进行了验证。我们还证明，它是有效的模型，不表现出局部Lipschitz连续性，这是遥不可及的现有技术。
2023-01-27 cs.LG cs.LO cs.SY
A Cegar-centric Bounded Reachability Analysis for Compositional Affine Hybrid Systems
针对组合混合系统可达性分析中乘积自动机位置爆炸的问题，提出以CEGAR为核心的有界可达性分析算法，结合不同组合语义与缓存优化，在SAT-Reach工具中实现并验证了可扩展性优势。
2025-09-03 cs.LO
On the Trade-off Between Efficiency and Precision of Neural Abstraction
University of Oxford（牛津大学）；University of Birmingham（伯明翰大学）
本文研究神经抽象在效率与精度间的权衡，提出分段常数与 sigmoid 非线性非多项式模板，并通过形式化归纳综合和可达性验证评估其性能。
2023-10-02 cs.LG cs.LO cs.SY
