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
Higher-Dimensional Timed Automata for Real-Time Concurrency
本文提出高维时间自动机（HDTAs）以统一建模实时并发系统中的事件并发与时间约束，证明其语言包含不可判定但去时间化语言包含可判定，并探讨了其在可达性检查等实际应用中的潜在优势。
2025-02-05 cs.FL cs.LO
Fast detection of cycles in timed automata
我们提出了一个新的有效的算法来检测，如果一个周期的时间自动机可以无限次迭代。用于该问题的现有方法具有在时钟数量上呈指数的复杂度。我们的方法是多项式的：它本质上是对数数量的区域规范化。该方法可以用于时间自动机上Büchi性质的验证算法。我们报告的一些实验表明，显着减少搜索空间时，我们的可迭代性测试。
2014-10-15 cs.FL cs.LO
Fast algorithms for handling diagonal constraints in timed automata
解决时间自动机中可达性的一种流行方法是枚举表示为区域的可达赋值集。天真的区域枚举不会终止。多年来已经研究了各种终止机制。当自动机在守卫中具有对角约束时，提出有效的终止机制具有明显的挑战性。在本文中，我们提出了一个新的终止机制的时间自动机与对角约束的基础上，一个新的模拟区域之间的关系。与现有的方法相比，这种模拟的实现实验显示出显着的收益。
2019-04-18 cs.FL cs.LO
LTL Parameter Synthesis of Parametric Timed Automata
参数时间自动机的参数综合问题是不可判定的，即使是非常简单的可达性。在本文中，我们引入了参数估值的限制下，参数综合问题是可判定的LTL性能。所研究的有界整数参数综合问题可以使用所有可能的参数赋值的显式枚举来解决。我们提出了一种替代的符号区域为基础的方法，这个问题的结果在一个更快的计算。我们的技术扩展了基于自动机的LTL模型检验的时间自动机的方法的思想。为了证明我们的方法的有用性，我们提供了实验评估和比较我们的方法与显式枚举技术。
2016-03-04 cs.FL cs.LO
Interrupt Timed Automata with Auxiliary Clocks and Parameters
时间自动机（ITA）是一种表达性的时间模型，根据级别考虑中断。由于这一特点，这种形式主义是不可比拟的时间自动机。然而，已经获得了一些与可达性和模型检验相关的可判定性结果。我们添加辅助时钟ITA，从而扩大其表达能力，同时保持可达性的可判定性。此外，我们定义了一个参数化版本的ITA，多项式的参数出现在警卫和更新。虽然参数推理与时间模型特别相关，但它经常导致不可判定性结果。我们证明了各种可达性问题，包括“强大的”可达性，是可判定的这个模型，我们给一个固定或可变数量的时钟，水平和参数的复杂性上界。
2014-09-08 cs.FL cs.LO
Timed Automata for Modelling Caches and Pipelines
在本文中，我们专注于建模的二进制程序运行在具有缓存和管道的架构的时间方面。我们的目标是获得一个时间自动机模型计算紧边界的最坏情况下的执行时间（WCET）的程序使用模型检查技术。
2015-11-13 cs.FL cs.LO
Improving search order for reachability testing in timed automata
时间自动机可达性分析的标准算法对自动机的转换顺序很敏感。为了解决这个问题，我们提出了一个排名系统和等待策略。本文讨论了搜索顺序问题的原因，并展示了如何将排名系统和等待策略集成到标准的可达性算法中，以分别缓解和防止问题。实验表明，这两种方法的组合给出了最佳的搜索顺序在标准的基准测试，除了一个例子。这表明，它应该用来代替标准的BFS算法的时间自动机的可达性分析。
2015-06-23 cs.FL cs.LO
Timed pushdown automata revisited
本文给出了下推自动机（PDA）的时间扩张的两个结果。作为我们的第一个结果，我们证明了Abdulla等人的密集时间PDA模型的崩溃：它在表达上等价于具有无时间堆栈的密集时间PDA。出于这一结果，我们主张的框架，一阶可定义的PDA，一个专门的PDA在原子集，作为正确的设置来定义和调查的时间扩展的PDA。这样得到的一般模型是图灵完备的。作为我们的第二个结果，我们证明了NEXPTIME上界复杂性的非空性问题的表达子类。作为一个副产品，我们得到了一个严格的EXPTIME复杂性约束的一个更严格的子类PDA与永恒的堆栈，从而包含已知的密集定时PDA的复杂性约束。
2015-04-17 cs.FL cs.LO
Reducing Clocks in Timed Automata while Preserving Bisimulation
随着时钟数目的增加，模型检验时间自动机变得越来越复杂。因此，人们希望用尽可能少的时钟来构造一个自动机。检查是否存在一个具有较少时钟的时间自动机，使得原始自动机接受的时间语言被保留的问题是不可判定的。在本文中，我们给出了一个结构，它对任何给定的时间自动机产生一个时间双相似自动机与最少数量的时钟。此外，我们表明，这样一个自动机的最小可能数量的时钟可以构建的时间是双指数的原始自动机的时钟的数量。
2015-05-20 cs.FL cs.LO
Relating timed and register automata
时间自动机和寄存器自动机分别是时间字和数据字上的著名计算模型。前者具有允许测试两个事件之间的时间流逝的时钟，而后者包括可以存储数据值以供稍后比较的寄存器。虽然这两个模型在外观上表现不同，但两个模型的几个决策问题具有相同的（非）可判定性和复杂性结果。作为一个突出的例子，空性是可判定的交替自动机与一个时钟或寄存器，都具有非原始递归复杂性。这不是偶然的。这项工作证实了这两个模型之间确实存在紧密的关系。我们表明，运行的时间自动机可以模拟的寄存器自动机，反之，运行的寄存器自动机可以模拟的时间自动机。我们的研究结果允许在这两种模型之间来回转移复杂性和可判定性结果。我们证明这些减少的有用性，通过获得新的结果注册自动机。
2010-11-30 cs.FL cs.LO
History-deterministic Timed Automata
本文研究了无限时间字上的历史确定性时间自动机，证明其识别语言类别严格介于确定性与非确定性自动机之间，并证明了其普遍性、包含性和综合问题的可判定性及EXPTIME完全性。
2024-10-09 cs.FL cs.LO
Certifying Emptiness of Timed Büchi Automata
时间自动机的模型检测器被广泛用于验证安全关键的实时系统。最先进的工具通过复杂的抽象实现可伸缩性。我们的目标是进一步提高他们的验证结果的信任，特别是检查活性属性。为此，我们开发了一种方法提取证书的空时间Büchi自动机从模型检验运行。这些证书可以由我们在Isabelle/HOL中正式验证的认证者进行双重检查。我们在一个抽象的环境中研究活性证书，并表明我们的方法是健全和完整的。为了证明它的可行性，我们提取了几个模型的证书，这些模型由Tandem和Imitator检查，并使用我们经过验证的认证器对其进行验证。
2020-07-08 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
A Unifying Approach to Decide Relations for Timed Automata and their Game Characterization
在本文中，我们提出了一个统一的方法来决定各种互模拟，模拟等价和两个时间自动机状态之间的前序。我们提出了一个区域为基础的方法来决定这些关系，我们消除了显式的产品建设的区域图或区域图在经典的方法。我们的方法也是通用的，可以用来决定几个时间关系。我们还提出了一个游戏表征这些时间的关系，并表明，游戏层次结构反映了层次结构的时间关系。人们可以得到一个无限的游戏层次，因此游戏表征进一步表明，尚未研究的定义新的时间关系的可能性。游戏的特征也帮助我们提出一个公式，它编码两个状态之间的分离，不是定时bisimilarily。这样的区别公式也可以产生许多关系以外的时间双相似性。
2013-07-29 cs.FL cs.LO
Reachability relations of timed pushdown automata
时间下推自动机（TPDA）是一种将递归与时间约束逻辑相结合的表达形式。我们证明了TPDA的可达性关系可以用线性算术表示，这是一种丰富的逻辑，推广了Presburger算术和有理算术。的主要技术成分是一个新的量词消去结果的时钟约束（用于简化TPDA转换的语法），使用时钟差关系来表达的分数时钟值的可达性关系，和应用帕里克定理重建的积分时钟值。
2020-12-30 cs.FL cs.LO
Testing Membership for Timed Automata
给定一个定时自动机，它承认厚组件和定时字$x$，我们提出了一个测试器，决定如果$x$是在语言的自动机或如果$x$是$ε$ -远离语言，使用大量的样本从加权时间分布$μ$与输入$x$。我们引入了一个时间词之间的距离，{ \em定时编辑距离}，它概括了经典的编辑距离。定时单词$x$是$ε$ -如果它与定时语言的相对距离大于$ε$，则远离该语言。
2023-03-28 cs.CC cs.FL cs.LO
Reachability for Updatable Timed Automata made faster and more effective
可更新时间自动机（UTA）是经典时间自动机的扩展，允许对时钟变量进行特殊更新，如x：= x - 1，x：= y + 2等，关于过渡。UTA的可达性通常是不可判定的。研究了具有可判定可达性的各种子类。一个通用的方法，UTA的可达性包括两个阶段：第一，静态分析的自动机进行计算的时钟约束在每个状态的集合;在第二阶段，可达的配置集，称为区域，枚举。在这项工作中，我们改进了静态分析算法。与现有算法相比，我们的方法计算更小的约束集，并保证终止更多的UTA，使可达性更快，更有效。作为主要的应用，我们得到了可判定性的另一种证明和更有效的算法，时间自动机与有界减法，一类广泛用于建模调度问题的UTA。我们已经实现了我们的过程中的工具，并进行了实验，验证我们的方法的好处。
2020-09-28 cs.FL cs.LO
Active learning of timed automata with unobservable resets
Univ Rennes（雷恩大学）；Inria（法国国家信息与自动化研究所）；CNRS（法国国家科学研究中心）
时间语言的主动学习涉及从观察到的时间词推断时间自动机。Agent可以查询目标语言中单词的隶属关系，或者提出候选模型并验证其与目标的等价性。这个框架的主要困难是时钟重置的推断，中央定时自动机的动态，但不能直接观察。有趣的第一步已经被限制在事件记录自动机的子类中，其中时钟重置与观察有关。为了进一步学习一般的时间自动机，我们将这种方法推广到一个新的类，称为重置自由事件记录自动机，其中一些过渡可能会重置没有时钟。这提供了与通用时间自动机相同的挑战，同时为了可读性而保持事件记录自动机的简单框架。我们的贡献的核心是无效性的概念，以及处理它的算法和数据结构，允许动态检测和修剪与观察相矛盾的重置假设，这是通用时间自动机的任何有效主动学习过程的关键。
2020-07-08 cs.FL cs.LG cs.LO
Logics Meet 2-Way 1-Clock Alternating Timed Automata
本文研究了单时钟交替时间自动机（1-ATA）的扩展，即双向单时钟交替时间自动机（2-Way 1-ATA）。我们证明了具有重置自由循环的2-Way 1-ATA的子类（2-Way 1-ATA-rfl）在表达上等价于用保护度量量词（GQMSO）扩展的MSO[<]。2路1-ATA-rfl（以及因此GQMSO）的空性检查问题通常是不可判定的。我们提出了一个“非准时性”的限制，称为非邻接，2路1-ATA-rfl，也为GQMSO，其中的空（分别满足性）检查成为可判定的。非相邻2路1-ATA是第一类具有交替和2路性的时间自动机，其空性检查是可判定的（并且也具有初等复杂性）。我们还表明，2路1-ATA-rfl，即使与非相邻的限制，可以表达属性是不可识别的使用1-ATA。
2022-02-26 cs.FL cs.LO
A Myhill-Nerode Characterization and Active Learning for One-Clock Timed Automata
IMDEA Software Institute（IMDEA软件研究所）；Chennai Mathematical Institute（金奈数学研究所）；CNRS IRL 2000, ReLaX（法国国家科学研究中心国际研究联系单元2000，ReLaX）
本文提出了一类单时钟确定性时序自动机的语言Myhill-Nerode特征，通过分析时钟重置信息，发展出L*算法以学习标准自动机。
2026-04-14 cs.FL cs.LO
Timed Automata Benchmark Description
本报告包含时间自动机（模型）和属性（规范）的描述，这些描述用作“实时系统动态模型检验的数据结构选择中的基准示例”和“证明的力量：时间自动机模型检验的新算法”。“这些来源的四个模型是：CSMA，FISCHER，LEADER和GRC。此外，我们在本报告中还包括两个额外的模型：FDDI和PATHOS。这六个模型经常被用来在时间自动机模型检验论文中对时间自动机模型检验器的速度进行基准测试。
2020-05-27 cs.FL
Reachability in Two-Clock Timed Automata is PSPACE-complete
Haase等人最近的一个结果表明，两时钟时间自动机中的可达性等价于有界单计数器自动机中的可达性。我们证明了有界单计数器自动机的可达性是PSPACE完全的。
2013-02-20 cs.FL
What's decidable about parametric timed automata?
参数时间自动机（PTA）是推理、模拟和形式化验证关键实时系统的有力工具。经过25年的研究，现在已经很好地理解，任何非平凡的问题研究是不可判定的一般PTA。我们在这里提供了一个调查的决策和计算问题的PTA。一方面，边界时间，边界参数的数量或域的参数不（一般）导致任何决策。另一方面，限制时钟的数量、时钟的使用（与参数比较或不与参数比较）以及参数的使用（例如，仅用作上限或下限）导致一些问题的可判定性。我们还强调开放性问题。我们还讨论了接近参数时间自动机（如参数混合自动机或参数中断时间自动机）的形式主义，我们研究了专用于PTA及其扩展的工具。
2019-07-03 cs.FL cs.LO
Unknown Biases and Timing Constraints in Timed Automata
本文研究允许分支概率与时钟约束均参数化的概率时间自动机，用不可数 pMDP 给出语义，并将可达性分析及符号后向、数字时钟语义推广到该参数化情形。
2024-03-04 cs.FL cs.LO
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
IMITATOR II: A Tool for Solving the Good Parameters Problem in Timed Automata
我们在这里介绍了Imitator II，一个新版本的Imitator，一个实现参数时间自动机的“逆方法”的工具：给定参数的参考值，它合成一个约束，使得对于任何满足此约束的值，系统在迹方面的行为与参考值相同，即，位置和动作的交替序列。模仿者II还实现了“行为制图算法”，使我们能够解决以下好参数问题：在给定的有界参数域内找到一组系统行为良好的估值。我们提出了新的功能和优化的工具，并给出结果的应用程序的异步电路和通信协议的各种例子。
2010-11-01 cs.FL cs.LO
Zenoness for Timed Pushdown Automata
时间下推自动机是用有限个实值时钟扩展的下推自动机。此外，堆栈中的每个符号都配备了表示其年龄的值。转变的启用可取决于时钟的值和最顶部码元的年龄。因此，稠密时间下推自动机是下推自动机和时间自动机的子类。我们之前已经证明了这个模型的可达性问题是可判定的。本文研究了zenoness问题，证明了它是EXPTIME-完全的。
2014-02-27 cs.FL
Efficient Convex Zone Merging in Parametric Timed Automata
参数时间自动机是一个强大的形式化推理的并发实时系统与未知或不确定的时间常数。减少它们的状态空间是减少固有的大量分析时间的重要方法。我们在这里提出了不同的合并减少技术的基础上凸联盟的约束（参数区），允许减少的状态数，同时保持验证和合成结果的正确性。我们进行了广泛的实验，并确定在实践中最好的算法，带来了显着减少的基准库的计算时间。
2022-12-09 cs.FL cs.LO
Reachability in two-parametric timed automata with one parameter is EXPSPACE-complete
参数时间自动机（PTA）是时间自动机的扩展，其中时钟可以与参数进行比较。可达性问题要求存在一个非负整数的参数分配，使得可达性在底层的时间自动机中保持。PTA的可达性问题长期以来被认为是不可判定的，已经超过了三个参数时钟。几年前，Bundala和Ouaknine证明了对于两个参数时钟和一个参数的PTA，可达性问题是可判定的，并且还证明了复杂度类PSPACE^NEXP的下界。我们的主要结果是，具有一个参数的两参数时间自动机的可达性问题是EXPSPACE-完全的。我们的贡献是双重的。对于EXPSPACE下界，我们利用复杂性理论的深层结果，即EXPSPACE的可串行化表征（基于巴林顿定理）和中国剩余表示中的数字的对数空间翻译为二进制表示。对于EXPSPACE上界，我们给出了一个仔细的指数时间减少PTA两个参数的时钟和一个参数的参数单计数器自动机（POCA）的一个参数的基础上轻微的调整，由于Bundala和Ouaknine建设的一个子类。我们提供了一系列的技术来分区一个虚构的运行的POCA到几个精心选择的子运行，使我们能够证明，它是足够的，只考虑指数量级的参数值。这使我们能够显示一个双指数上界的值的唯一参数的PTA在两个参数时钟和一个参数。我们希望我们的技术的扩展导致最终建立的可达性参数时间自动机与两个参数时钟（和任意多个参数）的长期开放的问题的可判定性。
2020-11-13 cs.FL cs.LO
Towards an Efficient Tree Automata based technique for Timed Systems
本文的重点是分析的实时系统与递归，通过良好的理论技术，这是可实现的发展。使用时钟变量对时间进行建模，并使用堆栈进行递归。我们的技术包括建模的定时系统的行为图，并解释这些图的树项显示其树的宽度上的绑定。然后，我们建立一个树自动机，接受正是那些树条款，描述可实现的运行的定时系统。因此，时间系统的空性归结为接受这些树项的有限树自动机的空性。这种方法有助于我们获得最佳的复杂性，不仅在理论上（如在早期的工作中所做的），而且在走向我们的技术的有效实现。为了做到这一点，我们在理论上做了一些改进，并利用这些来构建第一个原型工具，可以分析定时系统的递归。
2017-07-08 cs.FL cs.LO
Bounded Determinization of Timed Automata with Silent Transitions
确定性时间自动机的表达能力严格低于非确定性时间自动机，后者的表达能力又低于具有无声转换的时间自动机。因此，时间自动机一般是不可确定的。这是不幸的，因为确定性自动机在基于模型的测试，可观察性和可实现性中发挥着重要作用。然而，通过限制自动机中轨迹的长度，有效的确定成为可能。我们提出了一个新的程序有界确定的时间自动机。该程序将自动机展开为有界树，删除所有无声转换，并通过警卫的析取确定。所提出的算法被优化到有界的设置，因此更有效，可以处理更大的一类时间自动机比一般的算法。该方法在一个原型工具中实现，并在几个例子中进行评估。据我们所知，这是第一次实现这种类型的程序的时间自动机。
2015-08-14 cs.FL
Timed automata as a formalism for expressing security: A survey on theory and practice
时间自动机是验证受时间约束的并发系统的一种常用形式。他们扩展有限状态自动机与时钟，限制系统的行为的位置，并采取过渡。虽然时间自动机最初是为了安全而设计的（在广义上的正确性w.r.t.一种正式的财产），在一些工程中逐渐使用它们来保证安全财产。在这项工作中，我们回顾了过去二十年来研究时间自动机安全特性的工作。我们特别回顾了理论工作，特别关注不透明性，以及更实际的工作，特别关注攻击树及其扩展。我们得出的主要结论，开放的观点，以及工具的支持。
2022-06-07 cs.CR cs.FL cs.LO
Effective Definability of the Reachability Relation in Timed Automata
本文给出了Comon和Jurski关于时间自动机的二元可达关系在线性算术中是可定义的结果的一个新的证明。
2019-03-23 cs.FL
Emptiness and Universality Problems in Timed Automata with Positive Frequency
时间自动机接受的无限时间词的语言传统上是使用Buchi类条件定义的。这些接受条件集中在沿着运行无限频繁访问的位置集合上，但完全忽略定量定时方面。在本文中，我们提出了一个自然的定量语义的时间自动机的基础上，所谓的频率，它的措施，在接受的位置所花费的时间的比例。我们研究了正频率接受的时间语言的各种性质，特别是空性和普遍性问题。
2013-09-11 cs.FL
Mean-Payoff Games on Timed Automata
时间自动机上的平均支付博弈是在两个玩家（玩家Min和玩家Max）之间的定价时间自动机配置的无限加权图上进行的，通过沿着图的状态移动令牌来形成无限运行。最小玩家的目标是最小化跑步的极限平均重量，而最大玩家的目标则相反。Brenguier，Cassez和Raskin最近研究了这些游戏的一种变体，并表明对于具有五个或更多时钟的时间自动机来说，平均收益游戏是不可判定的。我们完善了这一结果，证明了不可判定性的均值支付游戏与三个时钟。在积极的一面，我们展示了一个时钟的时间自动机与二进制价格率的平均支付游戏的可判定性。本文的一个关键贡献是应用动态规划为基础的证明技术，适用于在不可数的状态和动作空间的平均奖励优化的背景下。
2016-07-28 cs.FL cs.GT cs.LO
Better abstractions for timed automata
我们考虑时间自动机的可达性问题。这个问题的一个标准解决方案涉及计算一个搜索树，其节点是区域的抽象。这些抽象保留了自动机状态空间上的底层模拟关系。出于有效性和效率的原因，它们由自动机的保护中发生的最大下限和上限（LU-边界）参数化。我们考虑Behrmann等人定义的aLU抽象。由于这种抽象可能会产生非凸集，因此尚未在实现中使用。我们证明了aLU抽象是最大的抽象方面的LU边界是健全的和完整的可达性。我们还提供了一个有效的技术，使用aLU抽象来解决可达性问题。
2016-07-28 cs.FL cs.LO
Revisiting local time semantics for networks of timed automata
我们研究了一种基于区域的方法来解决时间自动机的可达性问题。挑战在于当考虑并行工作的时间自动机网络时，如何缓解搜索空间的大小爆炸。在定时设置中，这种爆炸特别明显，因为即使进程的局部动作的不同交织也可能导致不同的区域。Salah等人在2006年已经证明，所有这些不同区域的联合也是一个区域。这种观察被用于一种算法中，该算法不时地检测这些区域并将其聚合成单个区域。我们表明，这样的聚合区可以更有效地计算使用本地时间语义和Bengtsson等人在1998年提出的本地区域的相关概念。接下来，我们指出了现有方法中的缺陷，以确保终止的局部区域图计算。我们用一种新的算法来解决这个问题，该算法构建局部区域图，并在（标准）区域上使用抽象技术来终止。我们评估我们的算法标准的例子。在各种示例中，我们观察到搜索空间的数量级减小。在其他示例中，该算法像标准区域算法一样执行。
2019-07-04 cs.FL cs.LO
MONAA: A Tool for Timed Pattern Matching with Automata-Based Acceleration
我们提出了monaa，一个监控工具在指定的时间自动机或定时正则表达式的实时属性。它实现了定时模式匹配算法，该算法结合了1）适合在线监控的功能，以及2）基于自动机的跳过加速。我们的实验证明了monaa的性能优势，特别是在在线使用。
2018-10-22 cs.FL
On the Distance between Timed Automata
包含时间自动机$A$接受的语言的问题（例如，实现）以$B$接受的语言（例如，规范）在非确定性时间自动机类中通常是不可判定的。为了解决这个令人不安的问题，我们展示了如何有效地构建确定性的时间自动机$A_d$和$B_d$的离散化（数字化）的非确定性的时间自动机$A$和$B$和不同的原始自动机在最多$\frac{1}{6}$的时间单位上的每个事件的发生。离散时间自动机中的语言包含是可判定的，当我们考虑$\overline{\mathfrak{L}(B)}$而不是$\mathfrak{L}(B)$时，它也是可判定的，$\overline{\mathfrak{L}(B)}$是${\mathfrak{L}(B)}$在欧几里德拓扑中的闭包：如果$\mathfrak{L}(A_d) \nsubseteq \mathfrak{L}(B_d)$，则$\mathfrak{L}(A) \nsubseteq \mathfrak{L}(B)$，如果$\mathfrak{L}(A_d) \subseteq \mathfrak{L}(B_d)$，则$\mathfrak{L}(A) \subseteq \overline{\mathfrak{L}(B)}$。此外，如果$\mathfrak{L}(A_d) \nsubseteq \mathfrak{L}(B_d)$，我们想知道$\mathfrak{L}(A_d)$离被…
2019-09-23 cs.FL
Adding Time to Pushdown Automata
在本教程中，我们将通过示例说明如何结合两个经典模型，即下推自动机（PDA）和时间自动机，以获得时间下推自动机（TPDA）。此外，我们描述了如何可达性问题TPDA可以减少到PDA的可达性问题。
2012-12-17 cs.FL cs.LO
Determinisability of one-clock timed automata
时间自动机的确定性成员问题是关于被非确定性时间自动机识别的时间语言是否能被确定性时间自动机识别。我们表明，当输入自动机是一个单时钟的非确定性时间自动机没有转换和确定性时间自动机的时钟数是固定的，这个问题是可判定的。我们表明，在所有其他情况下的问题是不可判定的，即，当1）输入非确定性定时自动机具有两个或更多个时钟，或2）它使用双跳变，或3）输出确定性自动机的时钟数量不固定时。
2020-07-18 cs.FL
Decidability of Timed Communicating Automata
研究了时间通信网络的可达性问题。每个进程都是一个时间自动机，通过在无界FIFO通道上交换消息与其他进程进行通信。消息携带时钟，该时钟在发送和接收时以适当的定时约束进行检查。每个自动机只能访问它的本地时钟和发送/接收消息的消息时钟集。时间是密集的，所有的时钟都以相同的速度进化。我们的主要贡献是一个完整的特征的可判定和不可判定的通信拓扑结构概括和统一以前的工作。从技术的角度来看，我们使用量词消去和减少计数器自动机与寄存器。
2018-04-20 cs.DC cs.FL cs.LO
Computing maximally-permissive strategies in acyclic timed automata
时间自动机是实时系统建模和推理的一种方便的数学模型。虽然它们提供了一种强大的方式来表示此类系统的时序方面，但时间自动机假设任意精度和零延迟动作;特别是，一个状态可能在时间自动机中被声明为可达，但在它所建模的物理系统中不可能到达。在本文中，我们认为宽容的策略，以克服这个问题：这样的策略提出的延迟间隔，而不是单一的延迟，并旨在达到一个目标状态，无论延迟实际发生。我们开发了一个算法计算的最佳许可（和相关的最大许可的战略）在无循环时间自动机和游戏。
2020-07-08 cs.FL
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
UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata
本文介绍了实时验证工具uppaal的主要扩展uppaalsmc。UPPAALSMC允许在自然随机语义下对定价时间自动机的网络的性能特性进行有效分析。特别是，uppaalsmc依赖于统计模型检验方法的一系列扩展，该方法被推广用于处理实时系统和估计不可判定的问题。UPPAALSMC与友好的用户界面结合在一起，该用户界面允许用户以有效的方式指定复杂的问题，以及以概率分布的形式获得反馈，并比较概率以分析系统的性能方面。调查的重点是该工具的演变-包括建模和规范形式主义以及应用技术-连同该工具的应用案例研究。
2012-07-04 cs.FL cs.LO
Modal Specifications for Probabilistic Timed Systems
模态自动机是一个经典的形式化模型，基于组件的系统，配备了丰富的规范理论支持抽象，细化和组合推理。近年来，模态自动机的定量变量被引入到嵌入式和移动系统的基于组件的设计的说明和推理中。这些分别概括了定时和概率系统的模态规范理论。在本文中，我们定义了一个模态规约语言的组合概率时间系统，称为抽象概率时间自动机，推广现有的形式主义。我们引入适当的语法和语义细化的概念，并讨论我们的规约语言的一致性，也相对于时间发散。我们确定了我们的模型，我们定义的抽象，结合和并行组合的基本操作的子类，并显示几个组合的结果。
2013-06-12 cs.FL cs.LO
Polynomial Interrupt Timed Automata
时间自动机（ITA）是秒表自动机的一个子类，它的可达性和时间模型检验的一些变体即使在参数存在的情况下也是可判定的。它们非常适合于建模和分析实时操作系统。在这里，我们用多项式保护和更新来扩展ITA，从而得到多项式ITA（PolITA）类。我们证明了可达性和模型检验的一个定时版本的CTL的一阶理论的圆柱形分解方法的适应性的可判定性。与以前的方法相比，我们的程序以统一的方式处理参数和时钟。此外，我们表明，Polita是不可比拟的秒表自动机。最后，在保持可判定性的同时引入了额外的功能。
2015-04-17 cs.FL
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
Communicating Timed Processes with Perfect Timed Channels
我们引入了通信时间自动机（CTA）的模型，扩展了经典的有限状态进程通过FIFO完美通道和时间自动机进行通信的模型，在这个意义上，有限状态进程被时间自动机所取代，完美通道内的消息配备有代表其年龄的时钟。除了标准操作（重置时钟，检查时钟的保护），每个自动机可以（1）将消息附加到具有初始年龄的通道的尾部，或者（2）如果其年龄满足一组给定的约束，则在通道的头部接收消息。在本文中，我们表明，可达性问题是不可判定的，即使在两个时间自动机连接一个单向定时通道的情况下，如果允许全球时钟（这两个自动机可以检查和操纵）。我们证明了这种不可判定性仍然成立，即使CTA由三个定时自动机和两个单向定时通道（没有任何全局时钟）。然而，可达性问题变得可判定（在$\mathsf{EXPTIME}$）的情况下，两个自动机链接一个单向定时通道，没有全局时钟。最后，我们考虑有界上下文的情况下，在每个上下文中，只有一个定时自动机被允许从一个通道接收消息，同时能够发送消息到所有其他定时通道。在这种情况下，我们证明了可达性问题是可判定的。
2018-03-18 cs.FL
Zone extrapolations in parametric timed automata
时间自动机（TA）是一种有效的形式化建模和验证系统的硬时间约束，并发。虽然TA假设具有无限精度的精确定时常数，但参数TA（PTA）利用这一限制并以不可判定性为代价增加其表现力。TA效率的一个实际解释是区域外推，其中超过给定常数的时钟估值被认为是等效的。这个概念不能轻易地扩展到PTA，因为参数可以是无界的。本文在M-外推的基础上，提出了几种PTA外推的定义，并研究了它们的正确性。我们的实验表明，整体减少的计算时间，最重要的是，允许终止一些以前无法解决的基准。
2022-03-24 cs.FL cs.LO
On Nonlinear Prices in Timed Automata
IIT Bombay（印度理工学院孟买分校）；CU Boulder（科罗拉多大学博尔德分校）
本文研究了更一般的 priced timed automata，证明在最一般情况下最优可达性问题是不可判定的，并利用 Z3 工具进行初步研究。
2016-12-15 cs.FL cs.LO cs.SY
On the expressive power of invariants in parametric timed automata
结合硬时序约束和并发性的系统的验证是具有挑战性的。当一些定时常数丢失或未知时，这个挑战变得更加困难。参数定时形式主义，如参数定时自动机（PTA），解决了这样的定时常数（被视为参数）的合成，其中一个属性成立。这样的形式主义是高度表达，但也不可判定，并提出了一些可判定的子类。在这里，我们提出了一个语法限制的PTA组成的删除警卫（限制过渡），只保持不变（限制位置）。虽然这种限制保留了PTA的表达能力（因此也保留了它们的不可判定性），但对约束类型的附加限制不仅允许证明可判定性，而且还允许执行满足可达性的参数估值的精确合成。这种形式主义，乍一看似乎微不足道，因为它受益于可达性问题的可判定性，具有比时间自动机（TA）更好的复杂性，但却受到TA相反享受的整个TCTL逻辑的不可判定性的影响。我们相信我们的形式主义允许一个有趣的权衡之间的可判定性和实际的表现力，因此是有前途的。我们在一个小的案例研究中展示了它的适用性。
2019-08-19 cs.FL cs.LO
Integer Reset Timed Automata: Clock Reduction and Determinizability
本文提出了一个过程，给定一个整数复位时间自动机（IRTA）${\cal A}$，产生一个语言等价的确定性单时钟IRTA ${\cal B}$，其大小至多是${\cal A}$大小的双指数.我们证明了这个位置的数量上的界是紧的。进一步地，如果整数重置被用于秒表自动机中，则获得在所有布尔运算下封闭且可达性可判定的秒表自动机子类。
2010-01-08 cs.FL
