Real-Time Model Checking Support for AADL
我们描述了一个模型检查工具链的AADL模型的行为验证，考虑到语言的实时语义，这是兼容的AADL行为附件。我们给出了一个高层次的视图的工具和转换中涉及的验证过程，并专注于我们的框架检查用户定义的属性提供的支持。我们还描述了在一个重要的航空电子演示器上获得的实验结果，该演示器模拟了负责飞机和地面站之间数据通信的网络协议。
2015-03-02 cs.LO cs.SE
A benchmark library for parametric timed model checking
涉及硬时序约束和并发的实时系统的验证是至关重要的。参数定时模型检验允许在存在未知定时常数或不确定性（例如，周期的不精确性）的情况下进行形式化验证。随着近年来一些技术和工具的发展，以提高效率的参数化定时模型检验，有一个适当的基准测试和比较这些工具的需求越来越大。我们在这里提出了一个基准库参数定时模型检验的基准积累了多年。我们的基准包括学术基准，工业案例研究和使用现有技术无法解决的例子。
2018-12-20 cs.LO
Making Abstraction Refinement Efficient in Model Checking
摘要抽象是模型检验中处理状态空间爆炸问题的重要策略之一。在抽象模型中，虽然状态空间大大缩小，但是在这样的模型中找到的反例可能不是真正的反例。对于经常涉及NP-难状态分离问题的抽象模型，需要进一步细化。本文提出了一种新的方法，通过增加额外的变量的抽象模型的细化。该方法不仅避免了NP-hard状态分离问题，而且得到了一个更小的精化抽象模型。
2010-07-21 cs.LO
Detecting Spurious Counterexamples Efficiently in Abstract Model Checking
摘要抽象是模型检验中处理状态空间爆炸问题的重要策略之一。在抽象模型中，状态空间大大缩小，然而，在这样的模型中找到的反例可能不是具体模型中的真正反例。因此，需要进一步完善抽象模型。如何检验反例是否为伪反例是抽象-精化循环中的一个关键问题。本文给出了伪路的一个形式化定义。在此基础上，提出了检测虚假反例的有效算法。
2011-09-26 cs.LO
Dynamic Verification of SystemC with Statistical Model Checking
许多嵌入式和实时系统具有固有的概率行为（传感器数据，不可靠的硬件等）。在这种情况下，至关重要的是评估系统属性，如“特定硬件故障的概率”。这样的属性可以通过使用概率模型检验来评估。然而，由于状态空间爆炸，这种技术在代表现实嵌入式和实时系统的模型上失败了。为了克服这个问题，我们提出了一个基于统计模型检验的验证框架。我们的框架是能够评估的概率和时间属性在SystemC，一个标准的系统级建模语言建模的大型系统。它作为Plasma-lab统计模型检查器的扩展完全实现。我们说明了我们的方法上的多升系统的案例研究。
2015-09-21 cs.LO cs.SE
Bounded Model Checking of an MITL Fragment for Timed Automata
时间自动机（TA）是一种常见的建模时间系统的形式。有界模型检验（BMC）是一种使用SAT或SMT求解器搜索违反属性的运行的验证方法。MITL是线性时间逻辑LTL的实时扩展。最初，MITL被定义为非重叠时间间隔的轨迹，而不是“超密集”时间轨迹，允许时间间隔重叠在单个点上，这些点被当今常见的时间自动机语义所采用。在本文中，我们扩展的MITL片段的语义超密集的时间轨迹，并设计了一个有界的模型检验编码的片段。我们证明了正确性和完整性的意义上说，使用一个足够大的范围内的反例，任何给定的非控股property.We可以找到实现建议的有界模型检验方法和实验研究的效率和可扩展性的实现。
2013-04-26 cs.LO
Path Checking for MTL and TPTL over Data Words
本文研究了数据词上MTL与TPTL的路径检查问题，依据寄存器数量和约束编码方式给出完整复杂度分析，证明MTL为P完全、TPTL为PSPACE完全，并得出单计数器机器模型检查的精确复杂度。
2017-09-01 cs.LO
Generic Model Checking for Modal Fixpoint Logics in COOL-MC
本文提出参数化模型检测工具 COOL-MC，支持多种 μ-演算实例，并通过归约奇偶博弈或惰性局部算法进行检测和基准评估。
2023-11-03 cs.LO
Accelerated Model Checking of Parametric Markov Chains
参数马尔可夫链很自然地出现在各种应用中：它们可以用于概率系统的保守分析（无论如何选择参数，系统都按照规范工作）;它们可以用于找到参数的最佳设置;它们可以用于可视化系统参数的影响;并且它们可以用于使得对于参数改变的情况容易地调整分析。不幸的是，这些进步是有代价的：参数模型检验通常很慢。为了使参数马尔可夫模型的分析规模化，我们需要三个要素：巧妙的算法，正确的数据结构和良好的工程。聪明的算法通常是主要的（或唯一的）卖点;我们面临着本文关注的问题--有效的模型检验的后一种成分。因此，我们最容易成名的是我们在与最先进的技术进行比较时经常意识到的速度。
2018-11-02 cs.LO
Model-checking Quantitative Alternating-time Temporal Logic on One-counter Game Models
我们考虑定量扩展的交替时间时序逻辑ATL/ATL称为定量交替时间时序逻辑（QATL/QATL），其中计数器的值可以比较使用等式，不等式和模约束的常数。我们解释这些逻辑在一个计数器的游戏模型，这是无限的持续时间的游戏有限的控制图，每个过渡可以增加或减少一个无界计数器的值。也就是说，这些游戏的状态空间通常是无限的。我们考虑的模型检验问题的逻辑QATL和QATL的一个计数器的游戏模型与VASS语义，我们开发的算法，并提供匹配的下界。我们的算法是基于减少的模型检验问题的模型检验游戏。这种方法使我们很容易处理扩展的逻辑语言以及无限的状态空间。该框架一方面概括了定性问题，如有限状态系统的ATL/ATL模型检验、单计数器过程上的分支时间时序逻辑CTL和CTL的模型检验以及LTL规范的可实现性问题。另一方面，QATL/QATL的模型检验问题推广了定量问题，如能源博弈（在QATL的情况下）和能源平价博弈（在QATL的情况下）的固定初始信用问题。我们的结果是积极的，因为我们表明，泛化是不是太昂贵的复杂性。作为一个副产品，我们获得了新的结果的复杂性模型检验CTL在一个计数器的过程中，并表明，决定赢家在一个计数器的游戏与LTL的目标是2 ExpSpace完成。
2014-09-19 cs.LO
Model checking and model synthesisfrom partial models: a logic-based perspective
我考虑以下一般情况：一个抽象的模型M的一些“真正的”系统只是部分介绍，或部分已知的，我们必须确保实际的系统满足给定的规范，形式化的一些逻辑语言。这种情况至少有两个本质上不同的解释，导致两个本质上不同的形式逻辑和算法问题：“部分模型的模型合成”，其中M到完整模型的一些“可接受”扩展必须满足规范，和“部分模型的模型检验”，其中M到完整模型的所有“可接受”扩展必须满足规范。这些问题自然地扩展了经典的可满足性、有效性和模型检验的逻辑决策问题。在这里，我简要地讨论这两个问题的背景下，经典，模态和时间逻辑。我做了一些观察，状态一些开放的问题，并概述了一个一般的表格式的程序，解决了几个著名的模态和时序逻辑，包括有限的部分模型的无约束模型合成的问题。K、LTL、CTL、ATL。
2020-12-22 cs.LO
A shallow dive into the depths of non-termination checking for C programs
针对现有非终止性检查工具在现实程序上效果不佳的问题，提出一种基于有界模型检查的健全高效技术，通过循环内断言与迭代展开深度检查循环状态，实验表明优于现有工具。
2024-09-04 cs.LO cs.SE
Stochastic Model Checking for Multimedia
现代分布式系统包括一类非功能性需求很重要的应用程序。特别是，这些应用程序包括多媒体设施，实时约束是至关重要的，他们的正确运作。为了指定这样的系统，它是必要的，以描述事件发生的概率分布和随机自动机已成为一个有用的技术，通过它可以指定和验证这样的系统。然而，随机描述是非常一般的，特别是它们允许使用一般的概率分布函数，因此它们的验证可能是复杂的。在过去的几年里，模型检测已经成为一个有用的验证工具，大型系统。在本文中，我们描述了两个随机自动机的模型检测算法。这些算法考虑如何写在一个简单的概率实时逻辑的属性可以检查一个给定的随机自动机。
2000-02-04 cs.LO cs.MM
Model Checking Probabilistic Real-Time Properties for Service-Oriented Systems with Service Level Agreements
服务质量属性的保证是面向服务的软件工程的一个重要方面。所谓的服务级别协议（SLA）的表示法，例如Web服务级别协议（WSLA）语言，提供了正式的语法来指定服务提供商和客户之间的（具有法律约束力的）合同方面的此类保证。另一方面，用于验证概率实时的【形】行为的形式化方法已经达到了一定的表达能力和效率水平，可以将其应用于现实世界的场景中。本文建议采用最近引入的区间概率时间自动机（IPTA）模型来对面向服务系统的QoS属性进行形式化验证。具体来说，我们表明，IPTA与概率时间自动机（PTA）相比，能够直接捕获SLA中指定的保证。IPTA分析中的一个特殊挑战是，它们的朴素语义通常会产生无限的状态集和无限分支的转换。然而，使用符号表示，IPTA可以进行分析，而有效。我们已经开发了第一个实现的IPTA模型检查器扩展的PRISM工具，并表明，模型检验IPTA是只稍微贵于模型检验可比PTA。
2011-11-14 cs.LO cs.PF cs.SE
Symbolic Simulation-Checking of Dense-Time Systems
直观地说，一个（实现）自动机被一个（规范）自动机模拟，如果实现自动机的每个外部可观察的转换也可以由规范自动机完成。在这项工作中，我们提出了一个符号算法的时间自动机的模拟检查。我们首先提出了一个模拟检查程序，操作状态空间，表示与凸多面体，时间自动机。然后，我们提出的技术来表示这些中间结果凸多面体的区域，并使该过程的算法。然后，我们讨论如何在实现自动机中处理芝诺状态。最后，我们完成了算法的实现，并在实验中报告了我们的算法的性能。
2006-10-13 cs.LO cs.SE
Model Checking Quantum Continuous-Time Markov Chains
本文首次对量子连续时间马尔可夫链进行模型检测，提出基于Schanuel猜想的实根隔离算法并结合自底向上区间运算检测信号时序逻辑公式，实现了与公式规模线性相关的查询复杂度。
2021-05-02 cs.LO math.NT quant-ph
UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata
本文介绍了实时验证工具uppaal的主要扩展uppaalsmc。UPPAALSMC允许在自然随机语义下对定价时间自动机的网络的性能特性进行有效分析。特别是，uppaalsmc依赖于统计模型检验方法的一系列扩展，该方法被推广用于处理实时系统和估计不可判定的问题。UPPAALSMC与友好的用户界面结合在一起，该用户界面允许用户以有效的方式指定复杂的问题，以及以概率分布的形式获得反馈，并比较概率以分析系统的性能方面。调查的重点是该工具的演变-包括建模和规范形式主义以及应用技术-连同该工具的应用案例研究。
2012-07-04 cs.FL cs.LO
FO Model Checking of Interval Graphs
我们研究了区间图上FO模型检验问题的计算复杂性，即，实数直线上区间的交图。主要的积极结果是，FO模型检验和后继不变的FO模型检验可以解决时间O（n log n）的n-顶点区间图的表示只包含从一个指定的有限集的长度的区间。我们补充这一结果表明，同样是不正确的，如果长度限制到任何集，是密集的一个开放的子集，例如，在集合$(1, 1 + \varepsilon)$中。
2015-12-11 cs.DM cs.LO
An Efficient Explicit-time Description Method for Timed Model Checking
时间模型检验作为一种形式化验证实时系统的方法，正受到模型检验界和实时界的广泛关注。显式时间描述方法使用标准非定时模型检查器中的一般模型构造来验证实时系统。Lamport提出了一种显式时间描述方法，使用时钟滴答过程（Tick）来模拟时间的流逝，并使用一组全局变量来建模时间需求。提出了两种方法，基于同步的显式时间描述方法和基于信号量的显式时间描述方法，这两种方法在建模实时系统时都比Lamport方法具有更好的模块性。与基于时间自动机的模型检查器（如UPPAAL）相比，显式时间描述方法可以访问和存储当前时刻，以便许多实时系统（特别是具有抢先调度的系统）将来进行必要的计算。然而，上述三种方法中的Tick过程在每个Tick中增加一个单位的时间;因此，状态空间随着时间参数的增加而相对快速地增长，当系统的时间周期相对较长时会出现问题。在本文中，我们提出了一个更有效的方法，使滴答过程跨越多个时间单位在一个滴答。在高性能计算环境下的初步实验结果表明，该方法显著地减少了状态空间，提高了时间和内存效率。
2009-12-13 cs.DC cs.LO cs.SE
Parametric Linear Dynamic Logic (full version)
我们介绍参数线性动态逻辑（PLDL），它扩展了线性动态逻辑（LDL）的时间运营商配备参数，约束其范围。LDL本身是作为线性时序逻辑（LTL）的扩展而提出的，它能够表达所有的ω-正则规范，同时仍然保持LTL的许多理想属性，如直观的语法和语义，并转换为指数大小的非确定性Büchi自动机。但是LDL缺乏表达时间约束的能力。通过添加参数化的运营商LDL，我们得到一个逻辑，能够表达所有的ω-正则性质，并包含参数化LTL和PROMPT-LTL LTL的参数化扩展。我们的主要技术贡献是翻译PLDL公式到不确定的Büchi自动机的指数大小通过交替自动机。这就产生了多项式空间算法的模型检验和假设保证模型检验和可实现算法的双指数运行时间。所有这三个问题也被证明是完整的这些复杂性类。此外，我们给出了严格的上限和下限的最佳参数值的模型检验和可实现性。利用这些界，我们提出了一个多项式空间过程的模型检验优化和一个算法的三次指数运行时间的可实现性优化。我们的研究结果表明，PLDL模型检验和可实现性并不比它们各自的（参数）LTL对应。
2015-12-07 cs.FL cs.LO
MTL-Model Checking of One-Clock Parametric Timed Automata is Undecidable
参数时间自动机扩展了时间自动机（Alfrer和Dill，1991），因为它们允许指定时钟值的参数边界。自1993年由Alfred，Henzinger和Vardi提出以来，已知具有一个时钟的参数时间自动机的空性问题是可判定的，而如果自动机使用三个或更多个参数时钟，则是不可判定的。该问题是开放的参数时间自动机与两个参数时钟。度量时态逻辑（Metric Temporal Logic，简称MTL）是一种广泛应用于实时系统的规约语言。时间自动机的MTL-模型检验是可判定的，无论时间自动机中使用多少时钟。本文证明了参数时间自动机的MTL-模型检验是不可判定的，即使该自动机只使用一个时钟和一个参数并且是确定的。
2014-04-01 cs.FL cs.LO
Model-checking real-time systems: revisiting the alternating automaton route
本文提出了一种基于区域方法的1-ATA空性算法，改进了MTL到1-ATA的转换，并研究了在特定条件下模型检验实时系统的方法。
2026-01-06 cs.FL cs.LO
Foundations for Entailment Checking in Quantitative Separation Logic (extended version)
定量分离逻辑（QSL）是分离逻辑（SL）的扩展，用于概率指针程序的验证。在QSL中，公式计算为实数而不是真值，例如，在给定的符号堆中，内存安全终止的概率。与\SL一样，使用QSL进行推理时的一个关键问题是\emph{entailment}：公式f是否包含另一个公式g？我们给出了从QSL中的蕴涵检查到SL中的蕴涵检查的一般性约简。这允许利用大量的SL研究来自动验证概率指针程序。我们分析了我们的方法的复杂性，并证明其适用性。特别是，我们得到的第一个可判定性结果，验证这些程序通过应用我们的减少到一个量化的扩展著名的符号堆片段的分离逻辑。
2022-01-27 cs.LO cs.PL
Model Checking Regular Language Constraints
即使是最快的SMT求解器在处理来自真实程序的正则表达式时也会遇到性能问题。由于这些性能问题通常来自问题表示（例如，非确定性有限自动机得到确定和正则表达式得到展开），我们重新审视布尔有限自动机，它允许直接和自然的表示任何正则语言的布尔组合。将IC3模型检验算法应用于布尔有限自动机，不仅可以有效地回答空性和普适性问题，而且通过扩展，可以判定多变量串成员问题的可满足性。我们证明了所产生的系统的有效性，一些流行的基准和正则表达式。
2017-08-30 cs.FL cs.LO cs.SC
Model Checking for Closed-Loop Robot Reactive Planning
University of Glasgow（格拉斯哥大学）
本文利用模型检验为差速驱动轮式机器人实时生成多步避障规划，通过新颖的LiDAR数据离散化和前向深度优先搜索实现，优于单步反应式代理，展现出在自动驾驶中安全透明轨迹规划的潜力。
2023-11-16 cs.AI cs.LO cs.RO
Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement
LMU Munich（慕尼黑大学）
本文提出了一种基于并行轨迹抽象细化的多线程软件模型检查方法，通过利用多核CPU提升验证效率，优于传统顺序方法和DSS技术。
2026-01-15 cs.LO cs.PL cs.SE
