Compositional Verification for Timed Systems Based on Automatic Invariant Generation
我们提出了一种组合验证的方法，以解决状态空间爆炸问题固有的模型检查定时系统的大量组件。主要的挑战是获得相关的全球时间约束的组件单独的时间。为此，我们利用辅助时钟自动生成新的不变量，捕获组件之间的同步引起的约束。该方法已在RTD-STIM工具中实现，并在多个基准测试中成功实验。
2015-09-16 cs.LO
Concurrent Constraint Conditional-Branching Timed Interactive Scores
多媒体场景具有与计算机程序相关联的多媒体内容和交互式事件。交互式分数（IS）是一种形式主义来表示这种情况下的时间对象，时间关系（TR）和交互事件。IS描述TR，但IS不能与条件分支一起表示TR。我们提出了一个模型的条件分支定时IS的非确定性时间并发约束（ntcc）演算。我们在Ntccrt（ntcc的实时解释器）中运行了我们的模型原型，响应时间对于实时交互来说是可以接受的。与Max/MSP或Petri网相比，ntcc的一个优点是条件和全局约束是声明式表示的。
2017-05-03 cs.LO cs.MM cs.PL
Verification of Timed Automata Using Rewrite Rules and Strategies
ELAN是一种强大的语言和环境，用于指定和原型化演绎系统，该语言基于由策略控制的重写规则。时间自动机是一类反应式系统的连续实时模型，有效的模型检测算法已经被设计出来。在本文中，我们表明，这些算法可以很容易地在ELAN系统的原型。本文认为，通过这个例子，重写依赖于规则和策略的系统是一个很好的框架，原型，研究和测试，而有效的符号模型检测算法，即算法，涉及组合的图形探索规则，演绎规则，约束求解技术和决策过程。
2009-07-17 cs.LO
A benchmark library for parametric timed model checking
涉及硬时序约束和并发的实时系统的验证是至关重要的。参数定时模型检验允许在存在未知定时常数或不确定性（例如，周期的不精确性）的情况下进行形式化验证。随着近年来一些技术和工具的发展，以提高效率的参数化定时模型检验，有一个适当的基准测试和比较这些工具的需求越来越大。我们在这里提出了一个基准库参数定时模型检验的基准积累了多年。我们的基准包括学术基准，工业案例研究和使用现有技术无法解决的例子。
2018-12-20 cs.LO
Abstract Diagnosis for Timed Concurrent Constraint programs
时间并发约束语言（Timed Concurrent Constraint Language，简称tccp）是一种基于简单但功能强大的并发约束范式Saraswat的并发逻辑语言。在这种范例中，存储作为值的概念被存储作为约束的概念所取代，这引入了与存储作为值的概念的一些差异。其他并发方法。在本文中，我们提供了一个通用的框架调试tccp程序。为此，我们首先提出了一个新的紧凑的，自底向上的语义的语言，非常适合于调试和验证的目的，在反应式系统的上下文中。我们还提供了一个抽象的语义，使我们能够有效地实现基于抽象解释的调试算法。给定一个tccp程序和一个行为规范，我们的调试方法自动检测程序是否满足规范。这与其他半自动调试方法不同，避免了提前提供症状的需要。我们通过介绍两个说明性的例子来展示我们的方法的有效性。我们选择一个特定的抽象域，并展示我们如何可以检测到一个程序是错误的。
2011-09-07 cs.LO cs.PL
Towards the Automated Verification of Cyber-Physical Security Protocols: Bounding the Number of Timed Intruders
时间入侵者模型被提出来验证网络物理安全协议（CPSP），修改了传统的Dolev-Yao入侵者以遵守环境的物理限制。由于要学习消息，定时入侵者需要等待消息到达，因此发起攻击可能取决于定时入侵者的位置。很可能出现这样的情况，即在存在大量入侵者的情况下，没有攻击，但在存在少量处于适当位置的入侵者的情况下，存在攻击。因此，CPSP自动化验证的一个主要挑战是确定使用多少定时入侵者以及将它们放置在何处。本文通过证明使用与参与者数量相同的定时入侵者数量就足够了来回答这个问题。我们还报告了一些初步的实验结果，发现在CPSP攻击。
2016-05-27 cs.CR cs.LO
Decentralized Stream Runtime Verification for Timed Asynchronous Networks
我们研究的问题，监测分布式系统中的计算机通信使用消息传递和共享一个几乎同步的时钟。这是一个现实的情况下，网络的监测速度是足够慢（在人的尺度），以允许有效的时钟同步，其中时钟偏差是小相比，监测周期。在广域网、互联网或包括大型部署中监控人类系统时就是这种情况。更具体地说，我们研究了如何监测分散的系统，其中监视器表示为流运行时验证规范，定时异步网络下。我们的监视器使用网络进行通信，其中消息可以花费任意长的时间，但不能被复制或丢失。这种通信设置在许多网络物理系统中很常见，如智能建筑和环境生活。以前的分散监控方法仅限于同步网络，由于网络故障，在实践中不容易实现。即使网络故障是不寻常的，他们可能需要几个监测周期来修复。在这项工作中，我们提出了一个解决方案的定时异步监控问题，并表明，这个问题概括了同步的情况下。我们研究的规范和条件的网络行为，允许监控发生有限的资源，独立的跟踪长度。最后，我们报告的实施和验证的有效性和效率方面的理论结果的实证评估的结果。
2023-02-03 cs.LO
Stochastic Timed Automata
随机时间自动机是定义在时间自动机上的纯随机过程，其中延迟和离散选择都是随机的。研究了该模型的几乎确定模型检验问题，即给定一个随机时间自动机A和一个性质$Φ$，我们想判定A是否以概率1满足$Φ$.在本文中，我们确定了几类自动机和属性，这可以决定。证明依赖于一个有限的抽象，称为厚图，我们解释为一个有限的马尔可夫链，我们可以决定几乎肯定的模型检查问题的建设。正确的抽象时，自动机几乎肯定公平，我们表明，是两大类系统，单时钟自动机和所谓的弱反应自动机的情况下。本文中使用的技术收集了实时验证和概率验证的工具，以及在时间自动机上进行的拓扑游戏。
2014-12-07 cs.LO
Concurrent Constraint Machine Improvisation: Models and Implementation
机器即兴创作通过明确的规则编码或应用机器学习方法来创作音乐。我们处理后一种情况。能够实时的即兴创作系统必须同时执行两个过程：一个是将机器学习方法应用于音乐序列以捕获突出的音乐特征，另一个是产生与学习材料风格一致的音乐序列。作为示例，基于非确定性时间并发约束（ntcc）演算的用于音乐即兴的并发约束因子Oracle模型（ccfomi）使用因子Oracle来存储所学习的序列。
2015-10-09 cs.LO
Parameterized Verification of Disjunctive Timed Networks
本文提出了一种基于新颖区域图算法的析取时间网络（DTNs）参数化验证新技术，通过解决最小时间可达性问题构建摘要时间自动机，避免了指数级截断系统的构建，并在特定时钟不变式条件下扩展了适用性。
2024-01-02 cs.FL cs.LO
Timed Multiset Rewriting and the Verification of Time-Sensitive Distributed Systems
本文提出一种带显式时间的多重集重写语言来建模时间敏感分布式系统，定义可实现性与可生存性，并证明在渐进定时系统上二者为PSPACE完全，时间有界时可实现性为NP完全，且可用Maude自动验证。
2024-07-02 cs.LO
Time-Darts: A Data Structure for Verification of Closed Timed Automata
符号数据结构在模型检验时系统中的应用已成为一个重要的研究课题，在一些成熟的验证工具中，差分边界矩阵（DBMs）仍然是首选的数据结构。相比之下，离散化提供了一个简单的选择，所有的操作都具有线性时间复杂度的时钟数，但有效的封闭系统的一大类。不幸的是，细粒度的离散化会导致状态空间爆炸。我们引入了一种新的数据结构，称为时间箭头的符号表示的状态空间的时间自动机。与完全离散化相比，单个时间镖允许表示任意大的状态集合，但是时间镖上的操作的时间复杂度在时钟数量上保持线性。我们证明了建议的可达性算法的正确性，并进行了几个实验，以比较性能的时间飞镖和完全离散化。主要结论是，在我们所有的实验中，时间镖方法优于完全离散化，它的规模显着更好的模型与较大的常数。
2012-11-27 cs.DS cs.LO
Verification and Control of Turn-Based Probabilistic Real-Time Games
定量验证技术已经被开发用于各种概率模型的形式化分析，例如马尔可夫链、马尔可夫决策过程及其变体。它们可用于对系统行为的定量方面产生保证，例如安全性、可靠性和性能，或帮助合成控制器以确保满足这些保证。我们提出了基于回合的概率定时多人游戏模型，它结合了概率选择，实时的【形】时钟和多个玩家之间的不确定性行为。基于概率时间自动机的简单模型的数字时钟方法，我们展示了如何计算定量验证的关键指标，即达到目标的概率和预期累积价格。我们说明了这一点，从计算机安全和任务调度的案例研究。
2019-07-17 cs.LO
An Overview of Modest Models and Tools for Real Stochastic Timed Systems
我们依赖于从智能电网到航空电子组件的网络物理系统的安全、可靠和及时运行。其中许多涉及时间依赖性行为，并受到随机性。因此，建模语言和验证工具需要支持这些定量方面。在MARS 2022的特邀演讲中，我介绍了使用Modest建模语言和Modest工具集进行定量验证，并强调了最近对模型表达能力和工具功能要求越来越高的三个案例研究：在卫星星座中使用具有分布式信息的马尔可夫决策过程的消息路由的情况;以及通过马尔可夫自动机模型检验优化对比特币的攻击的情况。本文总结了介绍。
2022-03-18 cs.LO
Re-verification of a Lip Synchronization Protocol using Robust Reachability
时间自动机是描述和分析实时系统的重要模型。鲁棒性是在时钟出现小漂移或测试防护装置不精确的情况下模型的正确性。实现了一种分析时间自动机鲁棒性的符号算法。在本文中，我们重新分析了一个工业案例唇同步协议使用新的鲁棒可达性算法。这个唇同步协议是一个有趣的情况下，因为定时方面是至关重要的协议的正确性。该模型的几个版本被认为是：一个理想的视频流，锚定抖动，和非锚定抖动。
2010-03-01 cs.LO
A Verified Approach for Checking Real-Time Specification Patterns
我们提出了一个验证方法的形式化验证的时间属性使用模型检查技术。我们专注于使用实时的【形】规范模式，它可以被看作是一个子集的定时时序逻辑，包括反应系统的分析过程中常见的属性表示的属性。我们的模型检测方法是基于使用观察员，以转换到验证更简单的LTL公式的验证定时模式。虽然使用观察员的模型检查是很常见的，我们的贡献是原始的几个方面。首先，我们定义了一个正式的框架来验证我们的观察者是正确的和非侵入性的。其次，我们为每个模式定义不同的观察者类别，并使用务实的方法，以选择最有效的候选人在实践中。这种方法是实现在一个集成的验证工具链的Fiacre语言。
2013-01-31 cs.LO
Automatic Translation of tock-CSP into Timed Automata
进程代数tock-CSP为离散时间行为建模提供了文本符号，并支持各种验证工具。类似地，时间自动机（TA）的自动验证由实时验证工具箱UPPAAL支持。TA和tock-CSP在建模和验证方法上都不同。例如，活性要求很难用tock-CSP的结构来指定，但它们很容易在UPPAAL中验证。在这项工作中，我们将tock-CSP转化为TA，以利用UPPAAL。我们已经开发了一个翻译技术和工具，我们的工作使用的规则翻译tock-CSP到一个网络的小TA，解决了复杂的捕捉tock-CSP的组合。为了验证，我们使用一种基于有限近似跟踪集的实验方法。我们计划使用数学证明来建立规则的正确性，这些规则将覆盖无限的轨迹集。
2021-04-29 cs.FL cs.LO
Towards a Digital Highway Code using Formal Modelling and Verification of Timed Automata
设计安全、可靠和值得信赖的自动驾驶汽车（AV）的挑战之一是确保AV遵守交通规则。为此，自动驾驶汽车需要能够理解和推理交通规则。在以前的工作中，我们引入了空间交通逻辑USL-TR，允许明确的，机器可读的，形式化的交通规则。这只是迈向可验证地遵守交通规则的自主交通代理的第一步。在本研究预览中，我们重点关注两个进一步的步骤：a）直接从交通规则中检索行为图，b）将行为图转换为使用USL-TR公式的时间自动机。有了这个，我们就有了一个正式的交通规则代表，并可以朝着建立数字公路代码的方向迈进。我们简要地设想进一步的步骤，其中包括添加环境和代理模型的时间自动机，最终实现和验证这些交通规则模型使用选择的形式化验证工具。
2022-09-28 cs.FL cs.LO cs.SE
Runtime Verification For Timed Event Streams With Partial Information
验证（RV）研究如何在观察下分析系统的执行轨迹。流跟踪验证（Stream Tracking Verification，SRV）应用流转换从观察到的跟踪中获取信息。当将RV和SRV技术应用于现实世界的系统时，在间隙中缺失信息的不完整跟踪构成了一个共同的挑战，因为RV方法通常需要完整的跟踪而没有缺失的部分。本文提出了一种基于抽象的对不完整轨迹执行SRV的解决方案。我们使用TeSSLa作为非同步定时事件流的规约语言，并定义抽象事件流，表示在输入跟踪的间隙期间可能发生的所有可能的跟踪的集合。我们展示了如何将TeSSLa规范翻译成其抽象的对应物，该对应物可以通过输入流的变换来传播间隙，从而生成声音输出，即使输入流包含具有不精确值的间隙和事件。该解决方案已被实现为一组宏的原始TeSSLa和实证评估表明该方法的可行性。
2019-07-10 cs.FL cs.LO cs.PL
Timed Automata Semantics for Analyzing Creol
我们给出了一个实时语义的并发，面向对象的建模语言克里奥尔，克里奥尔进程映射到网络的时间自动机。我们可以使用我们的语义来验证Creol对象的实时的属性，特别是看看进程是否可以正确调度并满足其端到端的最后期限。实时Creol可以用于分析，例如，多核嵌入式系统的抽象模型。我们展示了如何在Uppaal进行分析。
2010-07-29 cs.DC cs.LO
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
Parameterized Model-Checking for Timed-Systems with Conjunctive Guards (Extended Version)
在这项工作中，我们扩展艾默生和Kahlon的截止定理的过程骨架与合取警卫参数化网络的时间自动机，即系统获得的\emph{apriori}未知数量的时间自动机实例化从一个有限的时间自动机模板集$U_1, \dots, U_n$。通过这种方式，我们的目标是提供一个工具，普遍验证软件系统中未知数量的软件组件（即过程）与连续时间的时间约束进行交互。事实上，分布式算法往往表现出异构性，将动态方面与实时方面结合起来。在本文中，我们还将展示如何模型检查协议，使用特殊的变量存储标识符的参与进程（即PID）的时间自动机与合取警卫。这是不平凡的，因为参数化验证问题的解决方案通常依赖于过程是对称的，即不可区分的。另一方面，许多流行的分布式算法使用PID，因此不能直接应用这些解决方案。
2014-07-30 cs.LO
Towards Probabilistic Strategic Timed CTL
Institute of Computer Science, PAS（波兰科学院计算机科学研究所）；Nicolaus Copernicus University in Toruń（托伦哥白尼大学）；Department of Computer Science, University of Oxford（牛津大学计算机科学系）；LIPN, CNRS UMR 7030, Université Sorbonne Paris Nord（索邦巴黎北大学 LIPN 实验室）
本文提出PSTCTL，一种概率战略时序CTL变体，用于在随机多智能体系统中进行验证。
2026-02-11 cs.LO cs.MA
A Framework for Modelling, Verification and Transformation of Concurrent Imperative Programs
本研究提出一种嵌入简单类型高阶逻辑的并发命令式程序建模、验证与转换框架，可支持对交错计算命令式程序模型性质的可靠结构化推理，并通过Peterson互斥算法案例验证了其适用性。
2024-07-14 cs.LO
Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
我们研究了验证有限连续时间马尔可夫链（CTMC）C对线性实时规范作为一个确定性的时间自动机（DTA）A有限或穆勒接受条件。我们要解决的中心问题是：C的路径集合被A接受的概率是多少，即，C满足A的可能性结果表明，在有限的验收标准，这等于在有限的分段确定性马尔可夫过程（PDP）的可达概率，而Muller验收标准，它符合终端强连通组件在这样的PDP的可达概率。定性验证显示相当于PDP的图形分析。在我们的PDP的可达性概率，然后其特征在于作为第二类Volterra积分方程系统的最小解，并示出近似的偏微分方程系统的解决方案。对于单时钟DTA，该积分方程系统可以被变换成线性方程系统，其中系数是常微分方程的解。由于系数实际上是CTMC中的瞬态概率，因此该结果意味着CTMC分析的标准算法足以验证单时钟DTA规范。
2011-03-27 cs.LO
On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions
本文在 ADG 框架中提出 TATL 的即时符号验证算法，并通过推广包含检查与新型抽象显著加速，性能优于朴素方法及 Uppaal Tiga。
2025-06-09 cs.LO
Automating the Verification of Realtime Observers using Probes and the Modal mu-calculus
一个经典的方法模型检查的时间属性，如那些表示使用时间扩展的时间逻辑是依赖于使用观察员。在这种情况下，一个主要的问题是证明观察者的正确性。从本质上讲，这归结为证明：（1）每一个与属性相矛盾的轨迹都可以被观察者检测到;而且（2）观察者是无害的，这意味着它不能干扰被观察的系统。在本文中，我们描述了一种自动测试实时观测器的正确性的方法。这种方法是通过自动化通常被称为视觉验证的方法来获得的，在该方法中，通过检查其状态空间的图形表示来执行系统的正确性。我们的方法已经实现的工具蒂娜，时间Petri网的模型检查工具箱。
2015-09-22 cs.LO
Multi-player Equilibria Verification for Concurrent Stochastic Games
并发随机博弈（Concurrent Stochastic Games，CSG）是一种理想的概率系统建模方法，其特点是多个参与者或组件具有不同的目标，同时做出合理的决策。示例包括通信或安全协议和多机器人导航。存在用于CSG的验证方法，但仅限于代理或玩家被分组为两个联盟的场景，其中同一联盟中的那些共享相同的目标。在本文中，我们提出了多联盟的验证技术的CSG。我们使用子博弈完美的社会福利（或社会成本）的最优纳什均衡，这是战略，没有任何联盟单方面改变其战略在任何游戏状态，并在总的组合目标最大化（或最小化）。我们提出了一个扩展的时序逻辑rPATL（概率交替时间时序逻辑与奖励），指定任何数量的不同联盟的基于均衡的属性，和相应的模型检验算法的一个变体停止游戏。我们实现我们的技术在PRISM游戏工具，并将其应用到几个案例研究，包括秘密共享协议和公益游戏。
2020-07-24 cs.LO
Lightweight Time Modeling in Timed Creol
Creol是一种面向对象的建模语言，其中固有的并发对象交换异步方法调用。Creol的操作语义是以基于角色的风格编写的，并在重写逻辑中公式化。操作语义在Maude系统中产生了一个语言解释器，它可以用来分析模型。最近，Creol已被应用到无线电通信系统的建模，如传感器系统。在无线电通信中，信息会过期，如果同时发送，它们可能会在空中相撞。为了捕捉这些和其他属性的分布式系统，我们扩展了克里奥尔的操作语义的时间概念。我们利用框架的语言解释器使用一个轻量级的时间概念，与通用规约语言所需的。本文给出了Creol语言的一个时间扩展，包括语义和实现策略，并通过一个扩展实例讨论了它的性质。该方法可以推广到其他并发对象或演员为基础的系统。
2010-09-22 cs.LO cs.PL cs.SE
Automatic Verification of Concurrent Stochastic Systems
随机游戏的自动验证技术允许对系统进行正式推理，这些系统具有不确定或概率设置中理性代理之间的竞争或协作行为。现有的工具和技术集中于回合制游戏，其中游戏的每个状态由单个玩家控制，以及零和属性，其中两个玩家或联盟具有直接相反的目标。在本文中，我们提出了并发随机游戏（CSG）的自动验证技术，它提供了一个更自然的并发决策和交互模型。我们还考虑（社会福利）纳什均衡，正式确定的情况下，两个球员或联盟有不同的目标可以合作，以优化他们的联合表现。我们提出了一个扩展的时间逻辑rPATL在这种情况下指定的定量属性，并提出相应的算法验证和策略合成的变体停止游戏。对于有限时域的性质，计算是精确的，而对于无限时域，它是近似使用值迭代。对于零和性质，它需要通过线性规划来求解矩阵博弈，对于基于均衡的性质，我们通过SMT编码的标记多面体方法来找到双矩阵博弈的社会福利或社会成本纳什均衡。我们在PRISM游戏中实现了这种方法，这需要扩展工具的建模语言用于CSG，并将其应用于包括机器人技术，计算机安全和计算机网络在内的领域的案例研究，明确展示了CSG和基于平衡的属性的好处。
2020-08-29 cs.LO
Structured Interactive Music Scores
交互式评分是一种形式主义的设计和表现的交互式方案，提供了时间关系（TR）的对象之间的情况。在时间流Petri网中，对象间的TR可以建模，但难以表示全局约束。这可以在非确定性时间并发约束（ntcc）演算中显式完成。我们想形式化一个异构系统，在一个子系统中使用ntcc控制对象的并发执行，在另一个子系统中控制音频和视频处理。我们还计划开发一个自动验证ntcc。
2018-09-01 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
MightyPPL: Verification of MITL with Past and Pnueli Modalities
针对现有MITL验证方法支持逻辑片段有限或验证不完全的问题，本文提出MightyPPL工具，可将表达力更强的MITPPL公式转为兼容多验证后端的时间自动机，结合多项优化提升性能，并通过多案例评估了工具链表现。
2025-10-01 cs.FL cs.LO
Model Checking Data Flows in Concurrent Network Updates (Full Version)
我们提出了一个模型检验的方法来验证数据流的正确性，在网络配置的并发更新。该验证问题对于软件定义网络（SDN）非常重要，其中错误可能导致分组丢失、黑洞和安全违规。我们的方法是基于规范的时间属性的个人数据流，如要求流是免费的周期。我们检查这些属性是否同时满足所有活动的数据流，而网络配置更新。为了表示并发网络控制器的行为和由此产生的配置的演变，我们引入了一个扩展的Petri网的过境关系，其特征在于由Petri网的每个转变所引起的数据流。对于安全的Petri网与过境，我们减少了时间流属性的验证电路模型检验问题，可以解决有效的验证技术，如IC3，插值，有界模型检验。我们报告令人鼓舞的实验与原型实现的基础上的硬件模型检查ABC。
2019-11-14 cs.LO
On The Reachability Problem for Recursive Hybrid Automata with One and Two Players
受有限状态机有界模型检验框架成功的启发，Ouaknine和Worrell提出了实时验证的时间有界理论，认为对有限时间的限制恢复了与实时验证相关的几个关键决策问题的可判定性。为了支持这一理论，最近的列表不可判定的问题证明在时间有界的限制下可判定的是相当令人印象深刻的：语言包含的时间自动机，空问题交替时间自动机，空问题矩形混合自动机。我们研究的目的是恢复一般递归时间自动机的可判定性-也许递归混合自动机-在时间有界的限制下，以提供一个有吸引力的验证框架，强大的建模环境，如Stateflow/Simulink。不幸的是，然而，我们回答这个问题的否定表明，时间有界的可达性问题保持不可判定的递归时间自动机与五个或更多的时钟。虽然坏消息继续，即使当一个考虑行为良好的子类的递归混合自动机，我们恢复可判定性考虑递归混合自动机与有界上下文使用通过引用机制，或通过限制变量的数量为2，率在$\{0,1\}$。
2014-08-15 cs.FL cs.LO
Shared Memory Concurrent System Verification using Kronecker Algebra
多线程软件的验证仍然是一个挑战。这主要是因为线程交织的数量在线程数量中呈指数级增长。用矩阵演算研究线交织是这一研究领域的一种新方法。我们的程序的稀疏矩阵表示使用Kronecker代数的惰性实现进行操作。一个目标是生成一个称为并发程序图（CPG）的数据结构，它描述了所有可能的交织，并在保持完整性的同时结合了同步。我们证明了CPG在一般情况下可以表示为稀疏邻接矩阵。因此，矩阵中的条目数与其行数成线性关系。因此，有效的算法可以应用于CPG。此外，由于同步，实际上只需要结果矩阵的很小一部分，而其余部分在自动机方面是不可达到的。由于矩阵运算的延迟实现，无法到达的部分永远不会计算。这大大加快了处理速度，表明这种方法非常有前途。可以在CPG上执行包括数据流分析在内的各种应用。此外，矩阵的结构可以用来证明任意数量的线程的底层程序的属性。例如，死锁自由证明了一大类程序。
2011-09-26 cs.LO
Certifying Emptiness of Timed Büchi Automata
时间自动机的模型检测器被广泛用于验证安全关键的实时系统。最先进的工具通过复杂的抽象实现可伸缩性。我们的目标是进一步提高他们的验证结果的信任，特别是检查活性属性。为此，我们开发了一种方法提取证书的空时间Büchi自动机从模型检验运行。这些证书可以由我们在Isabelle/HOL中正式验证的认证者进行双重检查。我们在一个抽象的环境中研究活性证书，并表明我们的方法是健全和完整的。为了证明它的可行性，我们提取了几个模型的证书，这些模型由Tandem和Imitator检查，并使用我们经过验证的认证器对其进行验证。
2020-07-08 cs.FL cs.LO
Modeling Hybrid Systems in Hy-tccp
并发、反应和混合系统需要高质量的建模语言来描述和分析。时间并发约束语言（tccp）是作为一种简单但功能强大的反应式系统模型而引入的。在本文中，我们提出了混合tccp（hy-tccp），连续时间tccp的扩展，其中包括新的结构建模的连续动态的混合系统。
2014-12-15 cs.LO cs.PL
NTCCRT: A concurrent constraint framework for real-time interaction (extended version)
编写多媒体交互系统并不容易。它们的并发进程通常以不确定的顺序访问共享资源，这通常会导致不可预测的行为。使用纯数据（Pd）和Max/MSP可以编程并发，但是，很难基于多个标准同步进程。诸如非确定性时间并发约束（ntcc）之类的过程演算通过将多个标准表示为约束来克服该问题。我们建议使用我们的框架Ntccrt来管理Pd和Max中的并发。Ntccrt是一种实时的【形】ntcc的解译器。在Pd中使用Ntccrt外部（二进制插件），我们运行了机器即兴和信号处理的模型。
2015-10-09 cs.LO cs.MM
Compositional Reasoning for Shared-variable Concurrent Programs
并发系统的可扩展和自动化形式化验证一直是一个迫切的需求。在本文中，我们提出了一个验证框架，以支持自动组合推理的并发程序共享变量。我们的框架模型并发程序作为简洁的自动机，并支持多个重要属性的验证。简洁自动机的安全性验证和仿真是并行组合的，简洁自动机的安全性在精化过程中保持不变。我们以自动化的方式从无限状态并发程序中生成简洁的自动机。此外，我们提出了第一个自动化的方法来检查可靠保证无限状态并发程序之间的模拟。我们已经将我们的算法原型化，并将我们的工具应用于多个改进的验证。
2018-03-26 cs.FL cs.LO cs.SE
Barriers in Concurrent Separation Logic: Now With Tool Support!
我们开发并证明了一个合理的并发分离逻辑的Pthreads风格的障碍。尽管Pthreads屏障在系统中被广泛使用，并且分离逻辑被广泛用于验证，但是还没有任何努力将两者结合起来。与锁和临界区不同，Pthreads屏障允许在多个线程之间同时进行资源重新分配，并且本质上是有状态的，导致逻辑设计及其可靠性证明的显着复杂性。我们展示了我们的逻辑可以应用到一个特定的示例程序中的模块化的方式。我们的校样在Coq进行机器检查。我们展示了一个程序验证工具集，自动应用逻辑规则，并履行相关的证明义务。
2012-04-19 cs.LO
Compositional Verification in Concurrent Separation Logic with Permissions Regions
本文提出带权限区域的 CSL-Perm 组合式验证系统，通过可推断框架规则残余堆的蕴涵过程实现线程与函数调用推理，并经 CoSl 工具验证其优势。
2025-10-06 cs.LO cs.PL
Towards modular verification of pathways: fairness and assumptions
模块化验证是一种用于解决并发交互系统等复杂系统的性能验证中经常遇到的状态爆炸问题的技术。模块化方法是基于这样的观察，即感兴趣的属性通常只涉及系统的一小部分。因此，可以构建简化的模型，其近似于整个系统的行为，从而允许更有效的验证。生物化学途径可以被看作是复杂的并发交互系统。因此，验证它们的属性通常在计算上非常昂贵，并且可以利用模块化方法。在本文中，我们报告的生化途径的模块化验证框架的发展的初步结果。我们认为生物化学途径是竞争分子资源的并行反应系统。模块化验证技术可以基于仅包含涉及感兴趣的分子资源的反应的简化模型。对于一个适当的描述系统的行为，我们认为，它是必不可少的考虑一个合适的公平性的概念，这是一个完善的概念，并发理论，但在该领域的新途径建模。我们提出了一个建模方法，包括公平性，我们确定的假设下，验证属性可以在一个模块化的方式。我们证明了这种方法的正确性，并证明它的模型上的EGF受体诱导的MAP激酶级联Schoeberl等。
2012-11-17 cs.LO
Towards an Effective Decision Procedure for LTL formulas with Constraints
本文介绍了一个正在进行的工作，是一个更广泛的项目，其最终范围是定义一种方法来验证LTL公式w.r.t.的一部分。一个用时间并发约束语言tccp编写的程序，tccp是一种基于Saraswat并发约束范式的逻辑并发约束语言。tccp过程的一些固有概念是非确定性，处理状态中的部分信息和信息的单调演化。为了检查一个过程的LTL属性，我们的方法是基于抽象诊断技术。该技术的最后一步需要以有效的方式检查LTL公式（带约束）的有效性。在本文中，我们提出了一个决策方法的有效性时序逻辑公式（约束）建立我们的抽象诊断技术。
2013-08-19 cs.LO
Automated Verification of Reactive and Concurrent Programs by Calculation
反应式程序将传统的顺序编程结构与原语相结合，以允许与其他并发代理进行通信。它们在现代应用中无处不在，从组件系统和Web服务到网络物理系统和自主机器人。在本文中，我们提出了一个代数验证策略的并发反应式程序，与一个大的或无限的状态空间。我们定义了新的运营商来描述相互作用和状态更新，以及相关的方程理论。有了这个，我们可以计算一个反应式程序的指称语义，从而促进自动证明。值得注意的是，我们的推理支持迭代程序与反应不变量，Kleene代数的基础上，并行组成。我们通过验证反应缓冲区来说明我们的策略。我们的法律和战略是机械化的伊莎贝尔/UTP，我们的霍尔和他的统一编程理论（UTP）框架的实施，提供健全的保证和实际的验证支持。
2021-04-12 cs.LO cs.PL
Efficient Verification of Concurrent Programs Over TSO Memory Model
我们解决的问题，多线程程序运行在总存储顺序（TSO）内存模型的有效验证。它已被证明，即使有限的数据域程序，控制状态可达下TSO的复杂性是非原始递归。在本文中，我们首先提出了一种有界缓冲区验证方法，其中缓冲区的大小上的界限放置，验证是递增地进行，通过增加的缓冲区的大小与验证过程的每次迭代，直到达到所述的界限。对于有限数据域上的程序，我们还证明了存在一个缓冲区的界限K，如果该程序是安全的，那么它也是安全的无界缓冲区。我们已经实现了这种技术在一个工具ProofTraPar。我们的结果对memorax [2]，一个国家的最先进的声音和完整的验证TSO记忆模型，一直令人鼓舞。
2016-06-17 cs.LO cs.PL
A Formal Model For Real-Time Parallel Computation
对并行计算环境（特别是高性能集群计算系统）施加实时的【形】约束，对系统时序特性的形式化验证提出了各种挑战。在本文中，我们简要地激发了这样一个系统的需要，我们介绍了一个自动机为基础的方法来执行这样的形式化验证。我们定义了一个一致的并行定时系统的概念：一个混合动力系统组成的一组时间自动机（具体来说，定时Buchi自动机以及标准有限自动机的定时变体），旨在模拟一个表现良好的实时的【形】并行系统的定时特性。最后，我们给出了一个简短的案例研究来证明本文中的概念：一个并行矩阵乘法内核，它在可证明的时间上界内运行。我们给出了所使用的算法，相应的一致的并行定时系统，和实证结果表明，该系统在指定的时间约束下运行。
2013-01-01 cs.DC cs.LO
On Reducing Linearizability to State Reachability
原子对象（如并发堆栈和队列）的有效实现特别容易受到编程错误的影响，并且需要自动验证。不幸的是，他们的正确性标准-相对于给定的ADT规格的线性化-很难验证。即使在通常的时间安全属性（如控制状态可达性）是可判定的实现类上，线性化也是不可判定的。在这项工作中，我们证明了验证线性化某些固定ADT规格是可减少控制状态的可达性，尽管更难任意ADT。我们实现了几个最流行的原子对象的这种减少。这种减少产生的第一个可判定性结果的验证，而不限制并发线程的数量。此外，它使现有的安全验证工具的线性化验证的应用。
2015-05-25 cs.LO
Verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking
网络中领导者的选举是一项具有挑战性的任务，特别是当进程是异步的时，即，执行具有时变周期的算法。Thales开发了一种工业选举算法，具有任意数量的过程，可能会失败。在这项工作中，我们证明了这种工业算法的一个变体的正确性。我们使用的方法相结合的抽象，SafeProver求解器，和参数定时模型检查。这使我们能够证明算法的正确性为大量的p进程（p=5000）。
2018-12-21 cs.LO
A Rewriting Logic Approach to Stochastic and Spatial Constraint System Specification and Verification
本文讨论的问题，指定，模拟和验证反应系统重写逻辑。它提出了一个可执行的语义概率，时间和空间并发约束编程-这里称为随机和空间并发约束系统（SSCC）-在重写逻辑语义框架。该方法是基于一个增强和广义模型的并发约束规划（CCP）的计算层次空间可以分配给属于代理。可执行语义忠实地表示和操作捕捉高度并发的性质，不确定的行为，空间和认知特征的反应系统与信息流。在SSCC中，定时属性（由随机持续时间表示）可以与进程相关联，并且还支持排他性和独立的概率选择。利用Maude系统中的SMT求解技术，实现了SSCC的底层约束系统，包括整数和实数上的无量词公式。这导致了一个完全可执行的实时符号规范，可用于定量分析的统计模型检验的形式。SSCC的主要特点和能力说明了整个文件的例子。这一贡献是一个更大的研究工作的一部分，旨在提供正式的分析技术和工具，数学上建立在CCP的方法，研究界。
2022-11-03 cs.LO
Dense-Timed Petri Nets: Checking Zenoness, Token liveness and Boundedness
我们考虑密集时间Petri网（TPN），Petri网的扩展，其中每个令牌配备有实值时钟，并且语义是懒惰的（即，启用的转换不需要触发;时间可以流逝并禁用转换）。我们考虑了主题方案网络的下列核查问题。(i)Zenoness：是否存在来自给定标记的Zeno计算，即，只需要有限时间的无限计算。我们展示了TPN的zenoness的可判定性，从而解决了[Escrig et al.]的一个开放问题。此外，相关的问题，如果存在任意快速计算从一个给定的标记也是可判定的。另一方面，普遍的zenoness，即，如果所有来自给定标记的无限计算都是zeno，则问题是不可判定的。(ii)Token liveness：标记中的token是否存活，即，是否存在来自标记的最终消耗令牌的计算。我们通过将问题简化为可覆盖性问题来显示问题的可判定性，这对于TPN是可判定的。(iii)有界性：可达标记的大小是否有界。我们考虑两个版本的问题，即语义有界性，只有活令牌被考虑在标记，和语法有界性，也死令牌被认为是。我们展示了语义有界性的不可判定性，同时我们证明了句法有界性是可判定的，通过扩展的Karp-Miller算法。
2007-01-23 cs.LO
UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata
本文介绍了实时验证工具uppaal的主要扩展uppaalsmc。UPPAALSMC允许在自然随机语义下对定价时间自动机的网络的性能特性进行有效分析。特别是，uppaalsmc依赖于统计模型检验方法的一系列扩展，该方法被推广用于处理实时系统和估计不可判定的问题。UPPAALSMC与友好的用户界面结合在一起，该用户界面允许用户以有效的方式指定复杂的问题，以及以概率分布的形式获得反馈，并比较概率以分析系统的性能方面。调查的重点是该工具的演变-包括建模和规范形式主义以及应用技术-连同该工具的应用案例研究。
2012-07-04 cs.FL cs.LO
Timed Games with Bounded Window Parity Objectives
Chatterjee等人为图上的两人回合制游戏中的平均收益和总收益目标引入了窗口机制，该机制细化了具有时间界限的长期目标。这种机制已被证明在各种设置中是有用的，最近在定时系统中也是如此。在定时设置中，研究了所谓的固定定时窗口奇偶校验目标。固定定时窗口奇偶性目标是相对于某个时间界限定义的，并且要求我们始终见证时间帧，即，一个窗口，其大小小于最小优先级为偶数的固定范围。在这项工作中，我们专注于有界定时窗口奇偶校验目标。如果存在满足固定目标的某个界，则满足这样的目标。有界目标的满意度是鲁棒的建模选择，如常数出现在约束，不像固定的目标，常数的选择可能会影响一个给定的范围的满意度。我们证明了时间自动机中有界时间窗口目标的验证可以在多项式空间中进行，并且即使对于多目标扩展，具有这些目标的时间游戏也可以在指数时间内解决。这与固定情况的复杂性类相匹配。我们还提供了一个窗口奇偶性目标的不同变体的比较。
2022-05-09 cs.FL cs.GT cs.LO
A Note on Runtime Verification of Concurrent Systems
本文提出基于Mazurkiewicz迹的三值LTrL运行时验证方法，通过迹一致Büchi自动机构造监控器，使同一迹的所有线性化得到一致的验证结论。
2025-07-07 cs.FL cs.LO cs.SE
