On Verifying Timed Hyperproperties
我们研究的可满足性和模型检测问题的时间超属性指定的HyperMTL，HyperLTL的时间扩展。根据是否允许在不同的跟踪中交错事件，可以为定时超属性定义两种可能的语义：异步和同步。虽然可满足性问题可以决定类似于HyperLTL的语义的选择，我们表明，模型检查问题，除非规格是替代自由，是不可判定的，即使在非常有限的时间限制是允许的。在积极的一面，我们表明，模型检验HyperMTL与量词交替是可能的，在一定条件下的同步语义，或当有一个固定的时间域的长度上的界限。
2018-12-25 cs.LO
Real-Time Model-Checking: Parameters everywhere
本文研究离散时间自动机上逻辑TCTL的模型检验和参数综合问题，其中参数在模型（时间自动机）和属性（时态公式）中都允许.我们的结果如下。在消极的一面，我们表明，模型检验问题的TCTL扩展参数是不可判定的离散时间自动机只有一个参数时钟。不可判定性结果需要逻辑上的等价性。在积极的一面，我们表明，模型检验和参数合成问题成为可判定的一个片段的逻辑是不允许的平等。我们的方法是基于自动机理论的原则和扩展我们的方法来表示时间自动机使用Presburger算法的运行持续时间。
2007-02-27 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
Parametric Timed Model Checking for Guaranteeing Timed Opacity
信息泄露可能会对系统安全造成严重后果。在有害信息泄漏中，定时信息泄漏是攻击者根据系统执行时间推断内部信息的能力。我们解决以下问题：给定一个定时系统，合成的执行时间，其中一个不能推断系统是否执行了一些秘密的行为。我们解决这个问题的时间自动机（TA）的设置。我们首先提供了一个一般的解决方案，然后扩展到参数TA的问题，通过合成内部定时，使TA的安全。我们研究可判定性，设计算法，并表明我们的方法也可以适用于程序分析。
2019-10-29 cs.CR cs.LO
Symbolic Simulation-Checking of Dense-Time Systems
直观地说，一个（实现）自动机被一个（规范）自动机模拟，如果实现自动机的每个外部可观察的转换也可以由规范自动机完成。在这项工作中，我们提出了一个符号算法的时间自动机的模拟检查。我们首先提出了一个模拟检查程序，操作状态空间，表示与凸多面体，时间自动机。然后，我们提出的技术来表示这些中间结果凸多面体的区域，并使该过程的算法。然后，我们讨论如何在实现自动机中处理芝诺状态。最后，我们完成了算法的实现，并在实验中报告了我们的算法的性能。
2006-10-13 cs.LO cs.SE
UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata
本文介绍了实时验证工具uppaal的主要扩展uppaalsmc。UPPAALSMC允许在自然随机语义下对定价时间自动机的网络的性能特性进行有效分析。特别是，uppaalsmc依赖于统计模型检验方法的一系列扩展，该方法被推广用于处理实时系统和估计不可判定的问题。UPPAALSMC与友好的用户界面结合在一起，该用户界面允许用户以有效的方式指定复杂的问题，以及以概率分布的形式获得反馈，并比较概率以分析系统的性能方面。调查的重点是该工具的演变-包括建模和规范形式主义以及应用技术-连同该工具的应用案例研究。
2012-07-04 cs.FL cs.LO
Improved Bounded Model Checking of Timed Automata
时间自动机（TA）是一个非常流行的建模形式主义的时间敏感的属性。一个常见的任务是验证TA的网络是否满足给定的属性，通常用线性时态逻辑（LTL）或时间计算树逻辑（TCTL）的子集表示。在本文中，我们建立在TACK有界模型检查TA，它支持基于信号的语义TA和更丰富的度量区间时态逻辑（MITL）。TACK将TA网络和属性编码为LTL的变体，即时钟约束LTL（CLTLoc）。产生的CLTLoc公式然后可以通过诸如Zot的工具求解，该工具将CLTLoc属性转换为可满足性模理论（SMT）求解器的输入逻辑。我们提出了一种新的方法，保留TACK的MITL属性的编码，同时直接到SMT求解器语言编码的TA网络，利用BitVector逻辑和逻辑的实算术。我们还介绍了几个优化，使我们能够显着优于CLTLoc编码在许多实际情况下。
2021-04-26 cs.LO
Guaranteeing Timed Opacity using Parametric Timed Model Checking
信息泄露可能会对系统安全造成严重后果。在有害信息泄漏中，每当攻击者成功推断机密内部信息时，就会发生定时信息泄漏。在这项工作中，我们认为攻击者可以（仅）访问系统执行时间。我们解决以下时间不透明性问题：给定一个定时系统，一个私人位置和一个最终位置，合成从初始位置到最终位置的执行时间，其中一个不能推断系统是否通过私人位置。我们还考虑了全时不透明问题，询问系统是否对所有执行时间都是不透明的。我们发现，这些问题是可判定的时间自动机（TA），但成为不可判定的，当一个添加参数，产生参数时间自动机（PTA）。我们确定了一个子类与一些可判定性的结果。然后，我们设计了一种算法，用于合成PTA参数估值，保证所得到的TA是不透明的。我们最后表明，我们的方法也可以适用于程序分析。
2022-06-11 cs.CR cs.FL cs.LO
Timed Automata Robustness Analysis via Model Checking
本文针对时间自动机在设计阶段因时间常数不确定及实现扰动导致规范违反的问题，提出了通过模型检查进行鲁棒性分析的概念与技术，以辅助修复模型并确保可达性与安全规范。
2022-07-28 cs.FL cs.LO
Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties
概率时间自动机（Probably Timed Automata，PTAs）是一种扩展了离散概率分布的时间自动机（Timed Automata，TA），它作为一种数学模型，广泛应用于随机和时间行为。在这项工作中，我们考虑的问题，模型检查的线性\emph{dense-time}性质在{PTA}。特别是，我们研究了线性密集时间属性，可以编码的TA与无限的验收criterion.First，我们表明，模型检查PTA对确定性TA规格的问题可以通过产品建设解决。基于乘积结构，证明了确定性TA规格问题的计算复杂性是EXPTIME-完全的。然后我们证明了当放宽到一般的（非确定性的）TA时，模型检测问题变得不可判定，我们的结果大大扩展了TA的稠密时间特性和非确定性。
2018-06-13 cs.FL cs.LO
Automatic Verification of Timed Concurrent Constraint Programs
时间并发约束（Timed Concurrent Constraint，tccp）是并发约束编程（Concurrent Constraint Programming，cc）范式的扩展，它允许我们指定时间至关重要的并发系统，例如反应式系统。可以有无限多个状态的系统可以在tccp中指定。模型检验是一种能够自动验证具有大量状态的有限状态系统的技术。在过去的几年里，一些研究已经调查了如何扩展模型检验技术的系统具有无限数量的状态。在本文中，我们提出了一种方法，利用tccp的计算模型。基于约束的计算允许我们定义一种方法，将模型检验算法应用于（一类）无限状态系统。我们扩展的经典算法的模型检验LTL的一个特定的逻辑定义的验证tccp和tccp结构，我们在这项工作中定义的建模程序的行为。我们定义了一个限制的时间，以得到一个有限的模型，然后我们开发了一些说明性的例子。据我们所知，这是第一个为tccp定义模型检验方法的方法。
2005-05-11 cs.LO
On MITL and alternating timed automata over infinite words
单时钟交替时间自动机（OCATA）已被引入作为（单时钟）时间自动机的自然扩展来表达MTL的语义。在本文中，我们认为OCATA的模型检查和可满足性的问题MITL（MTL的语法片段），解释了无限的话。我们的方法是基于扩展到无限词的区间语义（最近在[BEG13]中介绍了有限词的情况）。我们提出了基于区域和基于区域的算法，基于这种语义，MITL模型检查和可满足性。我们报告的原型工具实现这些算法的性能。
2014-06-17 cs.LO math.LO
Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete
IIT Bombay（印度理工学院孟买分校）；MPI-SWS（马克斯·普朗克软件系统研究所）
本文证明多变量单侧区间TPTL的可满足性检验为PSPACE完全，且其表达力严格强于MITL，但检验复杂度更低，通过归约到新的非点式交替定时自动机子类实现。
2023-09-01 cs.CL cs.FL cs.LO
Reducing Clocks in Timed Automata while Preserving Bisimulation
随着时钟数目的增加，模型检验时间自动机变得越来越复杂。因此，人们希望用尽可能少的时钟来构造一个自动机。检查是否存在一个具有较少时钟的时间自动机，使得原始自动机接受的时间语言被保留的问题是不可判定的。在本文中，我们给出了一个结构，它对任何给定的时间自动机产生一个时间双相似自动机与最少数量的时钟。此外，我们表明，这样一个自动机的最小可能数量的时钟可以构建的时间是双指数的原始自动机的时钟的数量。
2015-05-20 cs.FL cs.LO
On MITL and alternating timed automata
单时钟交替时间自动机OCATA最近被引入作为（单时钟）时间自动机的自然扩展来表达MTL的语义（Ouaknine，Worrell 2005）。我们考虑OCATA的应用问题的模型检查MITL公式（MTL的语法片段）对时间自动机。我们引入了一个新的语义OCATA，直观地说，时钟估值的间隔，而不是单一的真实值。由于这种新的语义，我们表明，我们可以绑定的时钟副本的数量是必要的，让OCATA识别模型的MITL公式。配备了这种技术，我们提出了一个新的算法来翻译的MITL公式到一个时间自动机，我们勾勒出几个想法来定义新的模型检验算法的MITL。
2013-04-09 cs.FL cs.LO
Parameterized Model-checking of Discrete-Timed Networks and Symmetric-Broadcast Systems
本文研究了带离散时钟的参数化离散时间系统的模型检测复杂度，通过引入对称广播通信原语，证明了无控制器系统的安全性规范是PSPACE完全的、活性规范在EXPTIME内可判定，并揭示了带控制器系统的活性规范不可判定。
2025-06-23 cs.LO
Liveness of Parameterized Timed Networks
研究了具有多时钟的参数化离散时间网络形式的无限状态系统的模型检验问题。我们表明，这个问题是可判定的B-或S-自动机的规格。这样的规范是非常有表现力的（他们严格submerga-regular规范），并且很容易表达复杂的活性和安全属性。我们的结果是通过使用对称广播来模拟时间的流逝，并通过解决使用k-wise交会和对称广播通信的非定时过程的参数化系统的模型检验问题而获得的。我们的可判定性证明利用自动机理论，合理的线性规划和几何推理来解决向量加法系统中的某些可达性问题，我们相信这些证明技术将有助于解决相关问题。
2016-09-14 cs.LO
A Verified Approach for Checking Real-Time Specification Patterns
我们提出了一个验证方法的形式化验证的时间属性使用模型检查技术。我们专注于使用实时的【形】规范模式，它可以被看作是一个子集的定时时序逻辑，包括反应系统的分析过程中常见的属性表示的属性。我们的模型检测方法是基于使用观察员，以转换到验证更简单的LTL公式的验证定时模式。虽然使用观察员的模型检查是很常见的，我们的贡献是原始的几个方面。首先，我们定义了一个正式的框架来验证我们的观察者是正确的和非侵入性的。其次，我们为每个模式定义不同的观察者类别，并使用务实的方法，以选择最有效的候选人在实践中。这种方法是实现在一个集成的验证工具链的Fiacre语言。
2013-01-31 cs.LO
Certifying Emptiness of Timed Büchi Automata
时间自动机的模型检测器被广泛用于验证安全关键的实时系统。最先进的工具通过复杂的抽象实现可伸缩性。我们的目标是进一步提高他们的验证结果的信任，特别是检查活性属性。为此，我们开发了一种方法提取证书的空时间Büchi自动机从模型检验运行。这些证书可以由我们在Isabelle/HOL中正式验证的认证者进行双重检查。我们在一个抽象的环境中研究活性证书，并表明我们的方法是健全和完整的。为了证明它的可行性，我们提取了几个模型的证书，这些模型由Tandem和Imitator检查，并使用我们经过验证的认证器对其进行验证。
2020-07-08 cs.FL cs.LO
Generalizing Non-Punctuality for Timed Temporal Logic with Freeze Quantifiers
度量时态逻辑（MTL）和时间命题时态逻辑（TPTL）是线性时态逻辑（LTL）的重要实时扩展。在一般情况下，这些扩展的可满足性检查问题是不可判定的，当未来的U和过去的S模态使用。在一个经典的结果中，证明了MTL [U，S]的非准时片段MITL[U，S]的可满足性检验是可判定的，具有EXPSPACE完全复杂性。鉴于这种非准时性的概念在TPTL[U，S]的情况下不能恢复可判定性，我们提出了TPTL[U，S]的非准时性的一个推广，称为\emph{non adjacency}，并专注于它的1-变量片段1-TPTL[U，S].虽然非相邻的1-TPTL[U，S]似乎是一个非常小的片段，但它比MITL更严格地表达。作为我们的主要结果，我们证明了非相邻1-TPTL[U，S]的可满足性检验问题是可判定的，具有EXPSPACE完全复杂性。
2021-09-05 cs.LO
A Note on Fault Diagnosis Algorithms
在本文中，我们审查算法检查离散事件系统和时间自动机的可诊断性。我们指出，在这两种情况下的可诊断性问题减少到空性问题（定时）Büchi自动机。此外，它是已知的，检查是否离散事件系统是可诊断的，也可以减少到检查有界可诊断性。我们建立了一个类似的时间自动机的结果。我们还提供了一个综合的复杂性结果，为不同的故障诊断问题。
2010-04-16 cs.FL cs.LO
Verification of Timed Automata Using Rewrite Rules and Strategies
ELAN是一种强大的语言和环境，用于指定和原型化演绎系统，该语言基于由策略控制的重写规则。时间自动机是一类反应式系统的连续实时模型，有效的模型检测算法已经被设计出来。在本文中，我们表明，这些算法可以很容易地在ELAN系统的原型。本文认为，通过这个例子，重写依赖于规则和策略的系统是一个很好的框架，原型，研究和测试，而有效的符号模型检测算法，即算法，涉及组合的图形探索规则，演绎规则，约束求解技术和决策过程。
2009-07-17 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
Stochastic Timed Automata
随机时间自动机是定义在时间自动机上的纯随机过程，其中延迟和离散选择都是随机的。研究了该模型的几乎确定模型检验问题，即给定一个随机时间自动机A和一个性质$Φ$，我们想判定A是否以概率1满足$Φ$.在本文中，我们确定了几类自动机和属性，这可以决定。证明依赖于一个有限的抽象，称为厚图，我们解释为一个有限的马尔可夫链，我们可以决定几乎肯定的模型检查问题的建设。正确的抽象时，自动机几乎肯定公平，我们表明，是两大类系统，单时钟自动机和所谓的弱反应自动机的情况下。本文中使用的技术收集了实时验证和概率验证的工具，以及在时间自动机上进行的拓扑游戏。
2014-12-07 cs.LO
Model-checking real-time systems: revisiting the alternating automaton route
Chennai Mathematical Institute（金奈数学研究所）；CNRS, ReLaX, IRL 2000（法国国家科学研究中心、ReLaX实验室、IRL 2000）
本文提出了一种基于区域方法的1-ATA空性算法，改进了MTL到1-ATA的转换，并研究了在特定条件下模型检验实时系统的方法。
2026-01-06 cs.FL cs.LO
Witnesses and Counterexamples for Timed Bisimulation
TU Darmstadt（达姆施塔特工业大学）；University of Siegen（锡根大学）
针对时间自动机互模拟验证，提出基于虚拟时钟扩展区域图的方法，既能有效检查时间互模拟等价，又能生成有效见证或反例解释行为差异。
2026-06-16 cs.FL cs.LO
Revisiting Reachability in Timed Automata
我们重新审视了实时验证的一个基本结果，即给定的时间自动机的配置之间的二进制可达性关系是可定义的整数和实数的线性算术。在本文中，我们给出了一个新的和更简单的证明这一结果，建立在著名的可达性分析的时间自动机涉及差分界矩阵。利用这个新的证明，我们给出了一个指数空间过程的模型检验的可达性片段的逻辑参数TCTL。最后我们证明了后一个问题是NEXPTIME困难的。
2017-04-18 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
Verifying MITL formulae on Timed Automata considering a Continuous Time Semantics
时间自动机（TA）实际上是一种标准的建模形式主义，当人们感兴趣的是随着时间的推移分析它们的行为时，它可以表示系统。这种建模形式主义主要用于检查系统的行为是否满足一组感兴趣的属性。即使存在时间自动机的有效模型检查器，这些工具也不容易配置。首先，它们的设计并不容易允许添加新的时间自动机构造，例如新的同步机制或通信过程，但它们假设一组固定的时间自动机构造。其次，它们通常不支持完整的度量间隔时态逻辑（MITL），并且依赖于逻辑的精确语义，其中指定了不能容易地修改和定制的感兴趣的属性。最后，它们不容易允许在不同的上下文中使用可以加速验证的不同求解器。本文提出了一种新的技术来执行模型检验的完整的度量区间时序逻辑（MITL）属性TA。该技术依赖于翻译的TA和MITL公式到一个中间的约束LTL的时钟（CLTLoc）公式，这是通过一个可用的决策过程进行验证。该技术是灵活的，因为中间逻辑允许编码新的语义以及新的TA结构，只需添加新的CLTLoc公式。此外，我们的技术不受特定求解器的约束，因为中间CLTLoc公式可以使用不同的程序进行验证。
2019-09-10 cs.FL cs.LO cs.SE
Finding Minimum and Maximum Termination Time of Timed Automata Models with Cyclic Behaviour
本文提出了一种计算具有循环行为的时间自动机模型的最佳和最坏执行时间（BCET/WCET）的新算法。该算法可以工作在任何任意的对角线自由TA，可以处理更多的情况下比以前现有的算法BCAT/WCET计算，因为它可以处理TA中的周期，并决定他们是否导致一个无限的WCET。我们证明了所提出的算法的合理性，并研究其复杂性。据我们所知，这是第一个模型检验算法，全面解决系统的循环行为的BCET/WCET问题。Behrmann等人提供了一种算法，用于计算在定价时间自动机（PTA）中达到目标状态的最小成本/时间。该算法已在著名的模型检验工具UPPAAL中实现，用于计算自动机的最小终止时间。然而，我们表明，在某些情况下，当无限循环存在，在UPPAAL中实现的算法可能不会终止，我们提供的例子，UPPAAL未能验证。
2016-10-31 cs.FL cs.LO
Strategic (Timed) Computation Tree Logic
本文定义了带战略算子的 CTL 和 TCTL 扩展（SCTL 和 STCTL），证明其表达力优于 ATL，并分析了不同信息与回忆语义下的模型检测复杂度，最终利用 IMITATOR 工具支持 STCTL[ir] 的实际应用。
2023-10-19 cs.LO cs.MA
Backwards Reachability for Probabilistic Timed Automata: A Replication Report
向后可达性是一种有效的基于区域的概率时间自动机模型检验方法。PTCTL属性。然而，当前的实现仅限于可达性属性的最大概率。在本文中，我们报告我们的新实现的向后可达性的一部分，适度的工具集。它支持直到公式的最小和最大概率，使其成为当今最通用的实现。我们比较其行为的实验结果报告的原始论文提出的向后可达性技术。
2022-08-25 cs.LO
Revisiting MITL to Fix Decision Procedures
度量区间时态逻辑（Metric Interval Temporal Logic，MITL）是一种具有可判定可满足性和模型检验问题的实时时态逻辑。MITL的决策过程依赖于自动机理论方法，其中逻辑公式被转换为等效的时间自动机。由于时间自动机在互补下不封闭，MITL的决策过程首先将公式转换为否定的范式，然后再转换为时间自动机。我们发现，不幸的是，这些20岁的程序是不正确的，因为它们依赖于一个不正确的语义的R运算符。我们提出了正确的语义R，并给出了新的，正确的决策程序MITL。我们表明，可满足性和模型检验的MITL是EXPSPACE完全的，如前所述。我们还确定了一个片段的MITL，我们称之为MITL_{WI}是丰富的比MITL_{0,\infty}，我们表明，可满足性和模型检验是PSPACE完成。我们的许多结果已经在PVS中得到了形式化的证明。
2019-10-09 cs.LO
Timed context-free temporal logics (extended version)
本文的重点是时间逻辑的实时下推反应系统的行为的描述。本文旨在通过确保组合设置中的可判定性和易处理性，来桥接专门用于分别表达密集实时实时属性和上下文无关属性的易处理逻辑。为此，我们引入两个实时线性时序逻辑指定定量定时上下文无关的要求在逐点语义设置：事件时钟嵌套时序逻辑（ECNTL）和嵌套度量时序逻辑（NMTL）。ECNTL逻辑是CARET逻辑（标准LTL的上下文无关扩展）和事件时钟时序逻辑（与事件时钟自动机类相关的易处理实时逻辑框架）的扩展。我们证明了ECNTL的可满足性和可视下推时间自动机VPTA对ECNTL的可视模型检验是可判定的和EXPTIME完全的。另一个提出的逻辑NMTL是标准度量时态逻辑（MTL）的上下文无关的扩展。众所周知，未来MTL的可满足性在无限时间词上是不可判定的，但在有限时间词上是可判定的。另一方面，我们表明，通过增加未来的MTL与未来的上下文无关的时间运营商，可满足性问题原来是不可判定的有限时间的话。在积极的一面，我们设计了一个有意义的和可判定的片段的逻辑NMTL，这是表示等价于ECNTL和可满足性和明显的模型检查的VPTA是EXPTIME完成的。
2018-08-14 cs.LO
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
Timed Context-Free Temporal Logics
本文的重点是时间逻辑的实时下推反应系统的行为的描述。本文旨在通过确保组合设置中的可判定性和易处理性，来桥接专门用于分别表达密集实时实时属性和上下文无关属性的易处理逻辑。为此，我们引入两个实时线性时序逻辑指定定量定时上下文无关的要求在逐点语义设置：事件时钟嵌套时序逻辑（EC_NTL）和嵌套度量时序逻辑（NMTL）。逻辑EC_NTL是逻辑CaRet（标准LTL的上下文无关扩展）和事件时钟时序逻辑（与事件时钟自动机类相关的易处理实时逻辑框架）的扩展。本文证明了EC_NTL的可满足性和可视下推时间自动机（VPTA）对EC_NTL的可视模型检验是可判定的和EXPTIME-完全的。另一个提出的逻辑NMTL是标准度量时态逻辑（MTL）的上下文无关的扩展。众所周知，未来MTL的可满足性在无限时间词上是不可判定的，但在有限时间词上是可判定的。另一方面，我们表明，通过增加未来的MTL与未来的上下文无关的时间运营商，可满足性问题原来是不可判定的有限时间的话。在积极的一面，我们设计了一个有意义的和可判定的片段的逻辑NMTL，这是表示等价于EC_NTL和可满足性和明显的模型检查的VPTA是EXPTIME完成的。
2018-09-10 cs.LO
SMT-based Induction Methods for Timed Systems
在验证方法的许多应用中，对时间相关方面进行建模是很重要的。对于精确的结果，有必要将时间解释为密集域，例如使用时间自动机作为形式主义，即使系统产生的无限状态空间对验证方法具有挑战性。此外，完全符号化处理的状态空间的定时相关和非定时相关的元素似乎提供了一个有吸引力的方法，模型检验定时系统与大量的非确定性。本文提出了一种基于SMT的定时系统扩展的IC 3算法，一种新的，高效的，完整的验证方法，基于SAT的非定时系统。在扩展的IC 3算法中，对时间系统的无限状态空间的处理是基于对时间系统的区域抽象进行适当的调整。此外，$k$ -感应，另一个符号验证方法的离散时间系统，以类似的方式扩展到支持定时系统。这两种新的方法进行评估和实验比较，使用原来的离散时间IC 3算法的基于布尔化的验证方法。
2012-04-25 cs.LO
Efficient Algorithms for Time- and Cost-Bounded Probabilistic Model Checking
在概率定时系统的设计中，关于在给定时间、能量或更一般的成本预算内发生的行为的有界要求是至关重要的。传统上，这样的需求已经通过根据成本约束展开模型来减少到无界情况来进行模型检查。这加剧了状态空间爆炸问题，并显著增加了运行时间。在本文中，我们提出了三个新的算法来模型检查的时间和成本有界的马尔可夫决策过程和概率时间自动机，避免展开的属性。它们是基于一个修改的值迭代过程，枚举的状态，并消除技术。我们现在可以得到结果的任何成本限制在一个单一的状态空间不大于相应的无界或期望值属性。特别是，我们可以自然地计算累积分布函数，而无需开销。我们评估的适用性，并比较我们的新算法的性能和他们的实施从文献中的一些案例研究。
2016-05-18 cs.LO
On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions
本文在 ADG 框架中提出 TATL 的即时符号验证算法，并通过推广包含检查与新型抽象显著加速，性能优于朴素方法及 Uppaal Tiga。
2025-06-09 cs.LO
Higher-Dimensional Timed Automata for Real-Time Concurrency
本文提出高维时间自动机（HDTAs）以统一建模实时并发系统中的事件并发与时间约束，证明其语言包含不可判定但去时间化语言包含可判定，并探讨了其在可达性检查等实际应用中的潜在优势。
2025-02-05 cs.FL cs.LO
Coarse abstractions make Zeno behaviours difficult to detect
一个时间自动机的无限运行是芝诺，如果它只跨越有限的时间。这样的运行被认为是不可行的，因此重要的是检测它们，或者双重地找到非Zeno的运行。近年来，时间自动机的可达性检验方法得到了很大的改进。我们表明，这些非常有效的优化测试的芝诺运行成本高。特别是，我们展示了NP-完备性的LU外推Behrmann等人。我们详细分析了这种复杂性的来源，并给出了外推算子的一般条件，保证了Zenoness检查的多项式复杂性（低）。我们提出了一个轻微的削弱满足这些条件的LU外推。
2013-02-26 cs.LO
Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives
窗口机制是由Chatterjee等人引入的，用于在图上的两人回合制游戏中加强具有时间界限的平均支付和总支付目标。从那以后，它被证明在各种环境中都很有用，包括游戏中的奇偶性目标和马尔可夫决策过程中的平均收益和奇偶性目标。我们研究时间自动机和定时游戏中的窗口奇偶性目标：给定窗口大小的界限，如果在路径上的所有状态中，我们看到一个足够小的窗口，其中最小的优先级是偶数，则路径满足这样的目标。我们发现，检查时间自动机的所有时间发散路径满足这样的窗口奇偶校验目标可以在多项式空间中完成，并且相应的时间游戏可以在指数时间内求解。这与计时奇偶游戏的复杂性相匹配，同时增加了推理时间界限的能力。我们还考虑了多维目标，并表明复杂性类不会增加。据我们所知，这是第一次在实时设置中研究窗口机制。
2021-08-11 cs.FL cs.GT cs.LO
On the decidability and complexity of Metric Temporal Logic over finite words
度量时态逻辑（Metric Temporal Logic，MTL）是一种重要的实时系统规格说明形式。本文证明了有限时间词上MTL的可满足性问题是可判定的，具有非本原递归复杂性。我们还考虑了MTL的模型检查问题：是否所有的话接受一个给定的Alur-Dill时间自动机满足给定的MTL公式。我们证明了这个问题是可判定的有限字。在无限的话，我们表明，模型检验的安全片段的MTL-其中包括不变性和时间有界的响应特性-也是可判定的。这些结果是相当令人惊讶的，因为它们与文献中出现的各种相反的说法相矛盾。
2007-02-28 cs.CC cs.LO
An Overview of Modest Models and Tools for Real Stochastic Timed Systems
我们依赖于从智能电网到航空电子组件的网络物理系统的安全、可靠和及时运行。其中许多涉及时间依赖性行为，并受到随机性。因此，建模语言和验证工具需要支持这些定量方面。在MARS 2022的特邀演讲中，我介绍了使用Modest建模语言和Modest工具集进行定量验证，并强调了最近对模型表达能力和工具功能要求越来越高的三个案例研究：在卫星星座中使用具有分布式信息的马尔可夫决策过程的消息路由的情况;以及通过马尔可夫自动机模型检验优化对比特币的攻击的情况。本文总结了介绍。
2022-03-18 cs.LO
Time-Darts: A Data Structure for Verification of Closed Timed Automata
符号数据结构在模型检验时系统中的应用已成为一个重要的研究课题，在一些成熟的验证工具中，差分边界矩阵（DBMs）仍然是首选的数据结构。相比之下，离散化提供了一个简单的选择，所有的操作都具有线性时间复杂度的时钟数，但有效的封闭系统的一大类。不幸的是，细粒度的离散化会导致状态空间爆炸。我们引入了一种新的数据结构，称为时间箭头的符号表示的状态空间的时间自动机。与完全离散化相比，单个时间镖允许表示任意大的状态集合，但是时间镖上的操作的时间复杂度在时钟数量上保持线性。我们证明了建议的可达性算法的正确性，并进行了几个实验，以比较性能的时间飞镖和完全离散化。主要结论是，在我们所有的实验中，时间镖方法优于完全离散化，它的规模显着更好的模型与较大的常数。
2012-11-27 cs.DS cs.LO
Formal Visual Modeling of Real-Time Systems in e-Motions: Two Case Studies
e-Motions是一个基于时间的可视化模型转换框架，具有实时的【形】Maude语义，支持通常的Maude形式化分析方法，包括模拟，可达性分析和LTL模型检验。e-Motions的特点是一套新颖而强大的结构，用于表达定时行为。在本文中，我们说明了使用这些结构-从而隐含地调查其适用性，以直观的方式定义实时的【形】系统-定义和正式分析两个原型和非常不同的实时的【形】系统：（一）一个简单的往返时间协议计算的时间，它需要一个消息从一个节点到另一个节点，并返回;（二）EDF调度算法。
2011-06-30 cs.LO cs.SE
Automating the Verification of Realtime Observers using Probes and the Modal mu-calculus
一个经典的方法模型检查的时间属性，如那些表示使用时间扩展的时间逻辑是依赖于使用观察员。在这种情况下，一个主要的问题是证明观察者的正确性。从本质上讲，这归结为证明：（1）每一个与属性相矛盾的轨迹都可以被观察者检测到;而且（2）观察者是无害的，这意味着它不能干扰被观察的系统。在本文中，我们描述了一种自动测试实时观测器的正确性的方法。这种方法是通过自动化通常被称为视觉验证的方法来获得的，在该方法中，通过检查其状态空间的图形表示来执行系统的正确性。我们的方法已经实现的工具蒂娜，时间Petri网的模型检查工具箱。
2015-09-22 cs.LO
ExpTime Tableaux for the Description Logic SHIQ Based on Global State Caching and Integer Linear Feasibility Checking
我们给出了第一个ExpTime（复杂性最优）的Tableau决策过程，用于检查描述逻辑SHIQ中的知识库的可满足性，当数字以一元编码时。我们的程序是基于全局状态缓存和整数线性可行性检查。
2013-12-31 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
User-Driven Abstraction for Model Checking
针对模型检测受限于系统描述规模的问题，提出一种在模型检测前应用抽象规则简化系统的技术，大幅缩减状态空间并辅助理解系统属性，通过Dekker互斥算法等示例验证。
2023-07-28 cs.LO cs.SE
Cut-Free ExpTime Tableaux for Checking Satisfiability of a Knowledge Base in the Description Logic SHI
我们给出了第一个无割ExpTime（最优）Tableau决策过程，用于检查描述逻辑SHI中的知识库的可满足性，它扩展了描述逻辑ALC的传递角色，逆角色和角色层次。
2012-07-16 cs.LO
Epistemic Model Checking for Knowledge-Based Program Implementation: an Application to Anonymous Broadcast
知识为基础的程序提供了一个抽象的协议，其中代理人的行动是有关他们的知识状态的描述。本文介绍了如何认识模型检验技术可能会被应用到发现和验证具体的实现基于这个抽象层次的描述。实现的细节取决于协议使用的特定上下文。基于知识的方法使得实现能够相对于这些使用条件进行优化。该方法说明使用扩展的用餐密码协议，匿名广播的安全协议。
2010-04-26 cs.DC cs.LO
Timed Multiset Rewriting and the Verification of Time-Sensitive Distributed Systems
本文提出一种带显式时间的多重集重写语言来建模时间敏感分布式系统，定义可实现性与可生存性，并证明在渐进定时系统上二者为PSPACE完全，时间有界时可实现性为NP完全，且可用Maude自动验证。
2024-07-02 cs.LO
Timed tuplix calculus and the Wesseling and van den Bergh equation
我们开发了一个代数框架来描述和分析金融行为，即在计划时间内转移一定数量的资金的行为。在很大程度上，对金融产品的分析就是对这些行为的分析。我们正式的累积利息符合保存要求的金融产品提出的Wesseling和van den Bergh的方程的框架开发和定义的概念，金融产品的行为，使用这种形式化。我们还介绍了金融产品行为的一些特性。该框架的发展受到了以前的工作的进程代数ACP。
2013-07-19 cs.LO q-fin.GN
