Applications of the Differential Calculus in the Study of the Timed Automata: the Inertial Delay Buffer
Serban E. Vlad
利用R->{0，1}函数的导数，我们将描述最简单的时间自动机--惯性延迟缓冲器的关系写成两种形式：非确定性的和确定性的.
We write the relations that characterize the simpliest timed automaton, the inertial delay buffer, in two versions: the non-deterministic and the deterministic one, by making use of the derivatives of the R->{0,1} functions.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Probabilistic Timed Automata with Clock-Dependent Probabilities
概率时间自动机是经典的时间自动机扩展的离散概率分布的边缘。我们引入了依赖于时钟的概率时间自动机，概率时间自动机的一个变体，其中转移概率可以线性依赖于时钟值。依赖于时钟的概率时间自动机允许建模的时间推移和系统事件的可能性之间的连续关系。我们表明，决定是否到达某个位置的最大概率是在一个阈值以上的问题是不可判定的依赖于时钟的概率时间自动机。另一方面，我们表明，在时钟依赖的概率时间自动机到达某个位置的最大和最小概率可以近似使用基于区域图的方法。
Timed Automata with Polynomial Delay and their Expressiveness
我们考虑以前的模型的时间，概率和随机时间自动机，我们介绍我们的模型的时间自动机与多项式延迟，我们表征这些模型相对于彼此的表现力。
Symbolic Optimal Reachability in Weighted Timed Automata
加权时间自动机在2000年初被定义用于建模实时系统中的资源消耗或分配问题。在加权时间自动机中，最优可达性是可判定的，并提出了一种符号前向算法来解决这一问题。该算法使用所谓的定价区域，即具有成本函数的标准区域的扩展。为了确保终止，该算法要求时钟有界。对于未定价的时间自动机，已经做了很多工作来开发适合于时间自动机的前向探索的合理抽象，确保在不限制时钟的情况下终止模型检查算法。在本文中，我们利用最近的发展抽象的时间自动机，并提出了一个算法，允许符号分析的所有加权时间自动机，而不需要有界的时钟。
Model Checking Probabilistic Timed Automata with One or Two Clocks
概率时间自动机是具有离散概率分布的时间自动机的扩展。我们考虑模型检测算法的概率时间自动机，其中有一个或两个时钟的子类。首先，我们证明了PCTL概率模型检验问题（如确定一组目标状态是否可以以至少0.99的概率到达，而不管非确定性如何解决）对于单时钟概率时间自动机是PTIME完全的，对于具有两个时钟的概率时间自动机是EXPTIME完全的。其次，我们证明了，对于单时钟概率时间自动机，概率时间时序逻辑PCTL的模型检测问题是EXPTIME完全的。然而，模型检查问题的子类PCTL不允许准时的定时界，这需要在一个确切的时间点发生的事件，并与概率界以外的0或1，是PTIME完全的一个时钟概率定时自动机。
Trace Expressiveness of Timed and Probabilistic Automata
自动机的表现力是一个重要的功能，在理解可用的形式主义应选择建模一个特定的问题。概率自动机和随机自动机适用于表现出概率行为的系统建模，并且相对于非概率转移系统和马尔可夫链，已经研究了它们的表达能力。在本文中，我们考虑以前的形式主义的时间，概率和随机时间自动机，我们提出了我们的新模型的时间自动机与多项式延迟，我们引入了一个衡量的表现力的自动机，我们称之为跟踪表现力，我们的特点，这些模型的表现力相对于彼此在这个新的措施。
Weak Alternating Timed Automata
交替时间自动机上无限的话被认为是。主要结果是接受条件的表征，这些自动机的空性问题是可判定的。这一结果意味着新的可判定性结果的片段的时间时序逻辑。它还表明，与MITL不同，即使不允许准时的限制，表征仍然相同。
Alternating Timed Automata
提出了交替时间自动机的概念。证明了这种只有一个时钟的自动机在有限字上存在可判定的空性问题。这给出了一类新的定时语言，它在布尔运算下是封闭的，并且具有有效的表示。我们证明了具有一个时钟的交替时间自动机的空性问题的复杂性是非本原递归的。证明也给出了相同的下界的普遍性问题的非确定性时间自动机与一个时钟。我们研究了具有ε-跃迁的模型的扩张，证明了空性是不可判定的。在无限的话，我们显示undecidability的普遍性问题。
Verification for Timed Automata extended with Unbounded Discrete Data Structures
研究了扩展为无界离散数据结构的时间自动机验证问题的可判定性。更详细地说，我们扩展时间自动机与下推堆栈。通过这种方式，我们获得了一个强大的模型，例如可以用来模拟实时程序与过程调用。这是长期以来已知的，该模型的可达性问题是可判定的。本文的目标是确定语言包含问题和相关问题是可判定的时间下推自动机的子类。
Pushdown Timed Automata: a Binary Reachability Characterization and Safety Verification
我们认为下推时间自动机（PTA）的时间自动机（密集的时钟）增加了下推堆栈。PTA的配置包括控制状态、密集时钟值和堆栈字。通过使用模式技术，我们给出了二进制可达性的可判定特征（即，PTA的所有配置对的集合，使得一个可以到达另一个）。由于一个时间自动机可以被视为一个PTA没有下推栈，我们可以证明，二进制可达性的时间自动机是定义在实数和整数的加法理论。结果可用于验证稠密变量和无界离散变量上均包含线性关系的一类性质。这些性质以前不能用经典的区域技术来验证，也不能用时间自动机的时间时序逻辑和下推系统的CTL $^*$来表示。这些结果也被推广到时间自动机的其他推广。
Zone-based verification of timed automata: extrapolations, simulations and what next?
时间自动机是由Rajeev Schmidt和David Dill在90年代初提出的。在过去的几十年里，时间自动机已经成为事实上的模型，用于验证实时系统。时间自动机的算法是基于使用区域作为符号表示的状态空间的遍历。由于状态空间是无限的，终止依赖于产生可达状态的有限表示的有限抽象。获得有限抽象的第一个解决方案是基于区域的外推，并已在行业实力工具Uppaal中实现。在过去的十年中，出现了一种基于区域之间模拟的不同方法，并已在完全开源的工具中实现。这种基于模拟的方法已经为时间自动机的可达性和活性带来了新的有效算法，并且还扩展到更丰富的模型，如加权时间自动机和具有对角约束和更新的时间自动机。在这篇文章中，我们调查的外推和模拟技术，并讨论了未来的一些开放的挑战。
Probabilistic Timed Automata with One Clock and Initialised Clock-Dependent Probabilities
本文针对具有单时钟、仿射时钟依赖及初始化条件的时钟相关概率时间自动机，提出多项式时间算法解决其定量与定性可达性问题，通过转换为区间马尔可夫决策过程实现。
Revisiting Reachability in Timed Automata
我们重新审视了实时验证的一个基本结果，即给定的时间自动机的配置之间的二进制可达性关系是可定义的整数和实数的线性算术。在本文中，我们给出了一个新的和更简单的证明这一结果，建立在著名的可达性分析的时间自动机涉及差分界矩阵。利用这个新的证明，我们给出了一个指数空间过程的模型检验的可达性片段的逻辑参数TCTL。最后我们证明了后一个问题是NEXPTIME困难的。
On timed automata with input-determined guards
我们考虑一个一般概念的时间自动机与输入确定的警卫，并表明他们承认一个强大的逻辑框架沿着[D 'Souza03]的路线，在一元二阶逻辑表征和表达完整的时间时序逻辑。然后，我们推广这些自动机使用的概念介绍了Henzinger，拉斯金和Schobbens递归算子，并表明，他们承认一个类似的逻辑框架。这些结果在“逐点”语义中成立。最后，我们使用这个框架来表明，实时逻辑MITL的MITL等是表达完整的MSO对应于一个适当的输入确定的运营商。
Stochastic Timed Automata
随机时间自动机是定义在时间自动机上的纯随机过程，其中延迟和离散选择都是随机的。研究了该模型的几乎确定模型检验问题，即给定一个随机时间自动机A和一个性质$Φ$，我们想判定A是否以概率1满足$Φ$.在本文中，我们确定了几类自动机和属性，这可以决定。证明依赖于一个有限的抽象，称为厚图，我们解释为一个有限的马尔可夫链，我们可以决定几乎肯定的模型检查问题的建设。正确的抽象时，自动机几乎肯定公平，我们表明，是两大类系统，单时钟自动机和所谓的弱反应自动机的情况下。本文中使用的技术收集了实时验证和概率验证的工具，以及在时间自动机上进行的拓扑游戏。
Reachability in timed automata with diagonal constraints
我们考虑了具有对角约束（如x-y < 5）的时间自动机的可达性问题。时间自动机的最佳算法是通过枚举其配置的可达集来进行的，这些配置以称为“区域”的数据结构的形式存储。区域之间的仿真关系对于确保终止和效率至关重要。该算法采用了模拟测试“是Z模拟Z”？“，这表明区域Z不到达比区域Z '更多的状态，因此不需要从Z进一步枚举。没有有效的模拟已知的时间自动机包含对角约束作为警卫。本文提出了一种对角约束时间自动机的模拟关系LU-d。在消极的一面，我们证明了决定Z-不是-LU-d-simulated-by-Z'是NP-完全的。在积极的一面，我们确定了证人的非模拟，并提出了一种算法来决定这样的证人使用SMT求解器的存在。证人的形状表明，模拟测试在实践中可能是有效的。
Minimal witnesses for probabilistic timed automata
见证子系统在概率系统的分析中被证明是一个有用的概念，例如作为关于为什么给定属性成立的诊断信息或作为细化算法的输入。介绍了概率时间自动机（PTA）中可达性问题的见证子系统。使用一个新的操作差界矩阵，它示出了如何法卡斯证书的有限状态互模拟子系统的PTA可以被翻译成见证子系统。我们提出了算法的最小见证子系统的三个概念下的最小性，从不同的角度捕捉的时间行为的计算，并讨论了它们的复杂性。
Lazy abstractions for timed automata
我们考虑时间自动机的可达性问题。这个问题的一个标准解决方案涉及计算一个搜索树，其节点是区域的抽象。出于效率原因，它们由自动机的保护中发生的最大下限和上限（LU-边界）参数化。我们提出了一个算法，是更新的搜索树的探索过程中的LU边界。为了保持它们尽可能小，只有当它们能够实现在未抽象系统中不可能的过渡时，才对边界进行细化。因此，我们的算法可以看作是一种懒惰的CEGAR算法的时间自动机。我们表明，在几个标准的基准测试，该算法是能够保持非常小的LU边界，从而大大减少了搜索空间。
Backwards Reachability for Probabilistic Timed Automata: A Replication Report
向后可达性是一种有效的基于区域的概率时间自动机模型检验方法。PTCTL属性。然而，当前的实现仅限于可达性属性的最大概率。在本文中，我们报告我们的新实现的向后可达性的一部分，适度的工具集。它支持直到公式的最小和最大概率，使其成为当今最通用的实现。我们比较其行为的实验结果报告的原始论文提出的向后可达性技术。
Revisiting Timed Logics with Automata Modalities
众所周知，（定时的）$ω$ --诸如“p在每个偶数位置保持”和“p在接下来的10个时间单位内至少出现三次”的规则属性不能在度量间隔时间逻辑（$\mathsf{MITL}$）和事件时钟逻辑（$\mathsf{ECL}$）中表达。一个标准的补救措施，这一缺陷是扩展这些与模态定义的自动机。在本文中，我们表明，逻辑$\mathsf{EMITL}_{0,\infty}$（添加非确定性的有限自动机模式到片段的$\mathsf{MITL}$只有下限和上限的约束）和$\mathsf{EECL}$（添加自动机模式到$\mathsf{ECL}$）已经表现为$\mathsf{EMITL}$（完整的$\mathsf{MITL}$与自动机模式）。特别地，$\mathsf{EMITL}_{0,\infty}$和$\mathsf{EECL}$的可满足性和模型检查问题是PSPACE完全的，而$\mathsf{EMITL}$的相同问题是EXPSPACE完全的。我们还提供了一个简单的翻译，从$\mathsf{EMITL}_{0,\infty}$对角自由时间自动机，这使得实际的可满足性和模型检验的基础上，现成的工具。
Bounded Model Checking of an MITL Fragment for Timed Automata
时间自动机（TA）是一种常见的建模时间系统的形式。有界模型检验（BMC）是一种使用SAT或SMT求解器搜索违反属性的运行的验证方法。MITL是线性时间逻辑LTL的实时扩展。最初，MITL被定义为非重叠时间间隔的轨迹，而不是“超密集”时间轨迹，允许时间间隔重叠在单个点上，这些点被当今常见的时间自动机语义所采用。在本文中，我们扩展的MITL片段的语义超密集的时间轨迹，并设计了一个有界的模型检验编码的片段。我们证明了正确性和完整性的意义上说，使用一个足够大的范围内的反例，任何给定的非控股property.We可以找到实现建议的有界模型检验方法和实验研究的效率和可扩展性的实现。
Sound Conflict Analysis for Timed Contract Automata
针对连续时间下道义规范分析技术的缺失，提出一种可靠但不完备的算法用于检测时间契约自动机中的冲突，证明了其正确性并通过案例研究进行了验证。
A Benchmarks Library for Extended Parametric Timed Automata
参数时间自动机是一个强大的形式化推理的并发实时系统与未知或不确定的时间常数。为了测试新算法的效率，需要一组公平的基准测试。我们提出了一个扩展的IMITATOR基准库，多年来积累了一些案例研究，从学术和工业背景。我们在这里扩展了几十个新的基准库;这些基准突出了几个新的功能：活性属性，（参数）时间自动机（包括秒表或多速率时钟）的扩展，以及不可解的玩具基准。这些后者的补充有助于强调国家的最先进的参数合成技术的限制，希望在未来开发新的专用算法。
MTL-Model Checking of One-Clock Parametric Timed Automata is Undecidable
参数时间自动机扩展了时间自动机（Alfrer和Dill，1991），因为它们允许指定时钟值的参数边界。自1993年由Alfred，Henzinger和Vardi提出以来，已知具有一个时钟的参数时间自动机的空性问题是可判定的，而如果自动机使用三个或更多个参数时钟，则是不可判定的。该问题是开放的参数时间自动机与两个参数时钟。度量时态逻辑（Metric Temporal Logic，简称MTL）是一种广泛应用于实时系统的规约语言。时间自动机的MTL-模型检验是可判定的，无论时间自动机中使用多少时钟。本文证明了参数时间自动机的MTL-模型检验是不可判定的，即使该自动机只使用一个时钟和一个参数并且是确定的。
A Decidable Probability Logic for Timed Probabilistic Systems
在本文中，我们扩展的谓词逻辑介绍[Beauquier等人。2002]，以处理半马尔可夫过程。我们证明，相对于定性概率性质，模型检验是可判定的这种逻辑应用于半马尔可夫过程。此外，我们将我们的逻辑概率时间自动机考虑经典和紧急语义，并考虑时钟上的谓词。我们证明，半马尔可夫过程的结果也举行概率时间自动机的两个语义考虑。此外，我们证明了马尔可夫过程的结果[Beauquier et al. 2002]是可扩展的概率时间自动机，其中紧急语义被认为是。
Analyzing Timed Systems Using Tree Automata
本文提出用有限树自动机替代字自动机分析定时系统，通过将定时行为建模为有界树宽图并利用树自动机检查MSO性质，应用于定时下推系统等，实现状态可达性等时间抽象性质的分析。
Reachability of Communicating Timed Processes
我们研究的可达性问题的通信时间进程，在离散和密集的时间。我们的模型包括自动机与本地的时间限制通信无界FIFO通道。每个自动机只能访问其本地时钟集;所有时钟都以相同的速率进化。我们的主要贡献是一个完整的表征的可判定和不可判定的通信拓扑结构，离散和密集的时间。我们也得到了复杂性的结果，通过显示，通信时间的进程至少是硬的Petri网，在离散时间，我们也表现出等价的Petri网。我们的研究结果遵循相互拓扑保持时间自动机和（非定时）计数器自动机之间的减少。
Efficient Emptiness Check for Timed Büchi Automata (Extended version)
时间自动机的Büchi非空性问题是指判定一个给定的自动机是否有满足Büchi接受条件的无限非Zeno运行。这个问题的标准解决方案是添加一个辅助时钟来处理非Zenoness。在本文中，它表明，这种简单的变换有时可能导致指数爆破。提出了一种避免这种爆破的结构。它还表明，在许多情况下，非Zenoness可以确定没有额外的建设。提出了一种只在需要时使用非Zenoness构造的非空问题的动态算法。与原型实现的算法进行了实验报告。
Verification of Timed Automata Using Rewrite Rules and Strategies
ELAN是一种强大的语言和环境，用于指定和原型化演绎系统，该语言基于由策略控制的重写规则。时间自动机是一类反应式系统的连续实时模型，有效的模型检测算法已经被设计出来。在本文中，我们表明，这些算法可以很容易地在ELAN系统的原型。本文认为，通过这个例子，重写依赖于规则和策略的系统是一个很好的框架，原型，研究和测试，而有效的符号模型检测算法，即算法，涉及组合的图形探索规则，演绎规则，约束求解技术和决策过程。
Minimal-Time Synthesis for Parametric Timed Automata
参数时间自动机（PTA）通过允许时钟约束中的参数来扩展时间自动机。这样的形式主义是有用的，例如推理时，在一个定时系统中的未知延迟。使用现有技术，用户可以合成允许系统到达指定目标位置的参数约束，而不管内部时钟已经过去了多少时间。我们专注于综合参数，不仅达到目标位置，但我们也解决了以下问题：什么是最短的时间到达目标位置？对于哪些参数值，我们可以实现这一点？我们分析了这个问题，并提出了一个算法来解决它。我们还讨论了最小化一个特定的参数值，仍然达到目标，并提供解决方案。我们实证研究这些算法的性能在一个基准集的PTA和最小时间可达性合成是更有效的计算比标准的合成算法的可达性。
Costs and Rewards in Priced Timed Automata
我们认为帕累托分析的可达状态的多价格时间自动机（MPTA）：时间自动机配备了多个观察员，跟踪成本（最小化）和奖励（最大化）沿计算。每个观察者具有恒定的非负导数，其可以取决于MPTA的位置。我们研究了帕累托支配问题，它问是否有可能通过运行中的累积成本和奖励帕累托支配一个给定的目标向量到达目标位置。我们表明，这个问题是不可判定的一般，但可判定的MPTA与最多三个观察员。对于MPTA的观察者是所有的成本或所有的回报，我们证明了帕累托支配问题是PSPACE完全的。我们还考虑了一个ε近似的帕累托支配问题，是可判定的，而不限制数量和类型的观察员。我们开发MPTA和丢番图方程之间的联系。帕累托支配问题的不可判定性是由希尔伯特第十问题的还原所显示的，而三个观察者的可判定性是由一个涉及二次形式的算术片段的翻译所显示的。
Dense Integer-Complete Synthesis for Bounded Parametric Timed Automata
本文提出了一种参数外推方法，用于在有界参数域内合成参数估值集，确保可达性和无避免性，同时保持与参考估值的无时行为。
Parameterized Model-Checking for Timed-Systems with Conjunctive Guards (Extended Version)
在这项工作中，我们扩展艾默生和Kahlon的截止定理的过程骨架与合取警卫参数化网络的时间自动机，即系统获得的\emph{apriori}未知数量的时间自动机实例化从一个有限的时间自动机模板集$U_1, \dots, U_n$。通过这种方式，我们的目标是提供一个工具，普遍验证软件系统中未知数量的软件组件（即过程）与连续时间的时间约束进行交互。事实上，分布式算法往往表现出异构性，将动态方面与实时方面结合起来。在本文中，我们还将展示如何模型检查协议，使用特殊的变量存储标识符的参与进程（即PID）的时间自动机与合取警卫。这是不平凡的，因为参数化验证问题的解决方案通常依赖于过程是对称的，即不可区分的。另一方面，许多流行的分布式算法使用PID，因此不能直接应用这些解决方案。
Improved Undecidability Results for Reachability Games on Recursive Timed Automata
我们研究递归时间自动机（RTA）上的可达性游戏，推广Alur-Dill时间自动机的递归过程调用机制类似于递归状态机。对于具有两个或多个时钟的自动机，RTA上的可达性博弈中的胜者判定问题是不可判定的，而对于只有一个时钟的自动机，该问题是可判定的。Ouaknine和Worrell最近提出了一个实时验证的时间有界理论，声称对有界时间的限制恢复了与实时验证相关的几个关键决策问题的可判定性。我们重新审视了具有时间限制的递归时间自动机上的博弈，希望能恢复可判定性。然而，我们发现，这个问题仍然是不可判定的递归时间自动机与三个或更多的时钟。使用类似的证明技术，我们的特点是一个可判定性边境的推广RTA递归秒表自动机。
Active Learning of One-Clock Timed Automata using Constraint Solving
在Angluin的$L^*$算法框架下的主动自动机学习已被应用于学习多种自动机模型。在时间模型（如时间自动机）的应用中，主要的挑战是确定转换中时钟值的保护以及哪些转换重置时钟。本文介绍了一种新的算法，用于确定性单时钟时间自动机和时间Mealy机的主动学习。该算法使用的观察表不提交特定的重置选择，而是依赖于约束求解来确定满足准备条件的重置选择。我们评估我们的算法随机生成的例子以及实际案例研究，表明它适用于较大的模型，并与现有的工作学习其他形式的定时模型的竞争。
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编码在许多实际情况下。
Binary reachability of timed pushdown automata via quantifier elimination and cyclic order atoms
我们研究了一个扩展了模块和分数时钟约束的时间下推自动机的表达模型。我们表明，二进制可达性关系是有效的混合线性算术与合理的整数排序表示。这包含了类似的可表达性结果，以前已知的有限和下推定时自动机与不定时堆栈。作为关键的技术工具，我们使用量词消去的混合线性算术的一个片段和循环顺序原子，并减少注册下推自动机循环顺序原子。
Event-Clock Automata: From Theory to Practice
事件时钟自动机（Event Clock Automata，ECA）是一种时间语言模型，由Alfred，Fix和Henzinger提出，作为时间自动机的替代品，具有更好的理论属性（例如，ECA是可确定的，而时间自动机不是）。在本文中，我们重新审视和扩展的ECA理论。我们首先证明，没有有限时间的抽象语言等价存在的ECA，从而反驳索赔在原来的工作ECA。这特别意味着区域不形成时间抽象互模拟。然而，我们表明，区域仍然可以用来建立一个有限自动机识别的非定时语言的ECA。然后，我们通过引入事件区和事件DBMs（EDBMs），扩展了经典的区域和DBMs概念，让它们处理事件时钟而不是普通时钟（如在时间自动机中）。我们讨论的算法来处理事件区表示为EDBM，以及（半）算法的基础上EDBM决定的ECA语言空。
Fast zone-based algorithms for reachability in pushdown timed automata
由于时间自动机的多功能性，大量的工作已经发展到考虑时间自动机的扩展。一个已经引起很多兴趣的扩展是具有可能无界堆栈的时间自动机，也称为下推时间自动机（PDTA）模型。虽然不同的算法已经给出了这个模型的不同变体的可达性，这些结果中的大多数是纯理论的，并没有产生有效的实现。其中一个主要原因是这些算法（以及现有的实现）都没有使用所谓的基于区域的抽象，而是依赖于区域抽象或其他方法，这些方法很难实现。在本文中，我们表明，一个天真的扩展的区域为基础的可达性算法的控制状态可达性问题的时间自动机是不健全的堆栈的存在。为了更好地理解这一点，我们给出了一个基于归纳规则的时间自动机的区域可达性算法。这个替代视图允许我们分析和调整规则，使其也适用于下推时间自动机。我们得到了第一个基于区域的算法PDTA是终止，健全和完整的。我们实现了我们的算法在工具中的Tendash和进行实验，以显示其有效性，从而为更实用的方法来验证下推定时系统的方式。
On MITL and alternating timed automata
单时钟交替时间自动机OCATA最近被引入作为（单时钟）时间自动机的自然扩展来表达MTL的语义（Ouaknine，Worrell 2005）。我们考虑OCATA的应用问题的模型检查MITL公式（MTL的语法片段）对时间自动机。我们引入了一个新的语义OCATA，直观地说，时钟估值的间隔，而不是单一的真实值。由于这种新的语义，我们表明，我们可以绑定的时钟副本的数量是必要的，让OCATA识别模型的MITL公式。配备了这种技术，我们提出了一个新的算法来翻译的MITL公式到一个时间自动机，我们勾勒出几个想法来定义新的模型检验算法的MITL。
Higher-Dimensional Timed Automata for Real-Time Concurrency
本文提出高维时间自动机（HDTAs）以统一建模实时并发系统中的事件并发与时间约束，证明其语言包含不可判定但去时间化语言包含可判定，并探讨了其在可达性检查等实际应用中的潜在优势。
Game Characterizations of Timed Relations for Timed Automata Processes
在这项工作中，我们设计的游戏语义的时间等价物和前序的时间进程。对应于各种时间关系的时间游戏形成层次结构。这些游戏类似于斯特林的互模拟游戏。如果在游戏${\cal G}_1$中存在防守者的获胜策略意味着在另一游戏${\cal G}_2$中存在防守者的获胜策略，则对应于${\cal G}_1$的关系比对应于${\cal G}_2$的关系更强。游戏的层次结构也抛出光到几个时间关系，在本文中没有考虑。
Higher-Dimensional Timed Automata
本文提出高维时序自动机，证明其可达性为PSPACE完全，并展示如何利用张量积解决状态空间爆炸问题，扩展至高维混合自动机。
Fast detection of cycles in timed automata
我们提出了一个新的有效的算法来检测，如果一个周期的时间自动机可以无限次迭代。用于该问题的现有方法具有在时钟数量上呈指数的复杂度。我们的方法是多项式的：它本质上是对数数量的区域规范化。该方法可以用于时间自动机上Büchi性质的验证算法。我们报告的一些实验表明，显着减少搜索空间时，我们的可迭代性测试。
Fast algorithms for handling diagonal constraints in timed automata
解决时间自动机中可达性的一种流行方法是枚举表示为区域的可达赋值集。天真的区域枚举不会终止。多年来已经研究了各种终止机制。当自动机在守卫中具有对角约束时，提出有效的终止机制具有明显的挑战性。在本文中，我们提出了一个新的终止机制的时间自动机与对角约束的基础上，一个新的模拟区域之间的关系。与现有的方法相比，这种模拟的实现实验显示出显着的收益。
LTL Parameter Synthesis of Parametric Timed Automata
参数时间自动机的参数综合问题是不可判定的，即使是非常简单的可达性。在本文中，我们引入了参数估值的限制下，参数综合问题是可判定的LTL性能。所研究的有界整数参数综合问题可以使用所有可能的参数赋值的显式枚举来解决。我们提出了一种替代的符号区域为基础的方法，这个问题的结果在一个更快的计算。我们的技术扩展了基于自动机的LTL模型检验的时间自动机的方法的思想。为了证明我们的方法的有用性，我们提供了实验评估和比较我们的方法与显式枚举技术。
Interrupt Timed Automata with Auxiliary Clocks and Parameters
时间自动机（ITA）是一种表达性的时间模型，根据级别考虑中断。由于这一特点，这种形式主义是不可比拟的时间自动机。然而，已经获得了一些与可达性和模型检验相关的可判定性结果。我们添加辅助时钟ITA，从而扩大其表达能力，同时保持可达性的可判定性。此外，我们定义了一个参数化版本的ITA，多项式的参数出现在警卫和更新。虽然参数推理与时间模型特别相关，但它经常导致不可判定性结果。我们证明了各种可达性问题，包括“强大的”可达性，是可判定的这个模型，我们给一个固定或可变数量的时钟，水平和参数的复杂性上界。
Testing Membership for Timed Automata
给定一个定时自动机，它承认厚组件和定时字$x$，我们提出了一个测试器，决定如果$x$是在语言的自动机或如果$x$是$ε$ -远离语言，使用大量的样本从加权时间分布$μ$与输入$x$。我们引入了一个时间词之间的距离，{ \em定时编辑距离}，它概括了经典的编辑距离。定时单词$x$是$ε$ -如果它与定时语言的相对距离大于$ε$，则远离该语言。
On MITL and alternating timed automata over infinite words
单时钟交替时间自动机（OCATA）已被引入作为（单时钟）时间自动机的自然扩展来表达MTL的语义。在本文中，我们认为OCATA的模型检查和可满足性的问题MITL（MTL的语法片段），解释了无限的话。我们的方法是基于扩展到无限词的区间语义（最近在[BEG13]中介绍了有限词的情况）。我们提出了基于区域和基于区域的算法，基于这种语义，MITL模型检查和可满足性。我们报告的原型工具实现这些算法的性能。
Active learning of timed automata with unobservable resets
时间语言的主动学习涉及从观察到的时间词推断时间自动机。Agent可以查询目标语言中单词的隶属关系，或者提出候选模型并验证其与目标的等价性。这个框架的主要困难是时钟重置的推断，中央定时自动机的动态，但不能直接观察。有趣的第一步已经被限制在事件记录自动机的子类中，其中时钟重置与观察有关。为了进一步学习一般的时间自动机，我们将这种方法推广到一个新的类，称为重置自由事件记录自动机，其中一些过渡可能会重置没有时钟。这提供了与通用时间自动机相同的挑战，同时为了可读性而保持事件记录自动机的简单框架。我们的贡献的核心是无效性的概念，以及处理它的算法和数据结构，允许动态检测和修剪与观察相矛盾的重置假设，这是通用时间自动机的任何有效主动学习过程的关键。
Undecidable Problems About Timed Automata
本文解决了S. Tripakis在[ Folk Theorems on the Determinization and Minimization of Timed Automata，in the Proceedings of the International Workshop FORMATS'2003，LNCS，Volume 2791，p.182 -188，2004 ]和E. Asarin in [ Challenges in Timed Languages，From Applied Theory to Basic Theory，Bulletin of the EATCS，Volume 83，p. 106-120，2004 ].特别是，我们不能决定是否一个给定的时间自动机是可确定的，或是否补充的时间正则语言是定时定期。我们证明了时间自动机的时钟数的最小化问题是不可判定的。两个定时正则语言的混洗是否定时正则也是不可判定的。我们证明，在接受无限时间词的时间Büchi自动机的情况下，其中一些问题是Pi^1_1-hard的，因此是高度不可判定的（位于算术层次之外）。
Timed Automata for Modelling Caches and Pipelines
在本文中，我们专注于建模的二进制程序运行在具有缓存和管道的架构的时间方面。我们的目标是获得一个时间自动机模型计算紧边界的最坏情况下的执行时间（WCET）的程序使用模型检查技术。
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作为最终修复的模型。实验表明，该方法能够成功地部分修复用户的初始设计。
Improving search order for reachability testing in timed automata
时间自动机可达性分析的标准算法对自动机的转换顺序很敏感。为了解决这个问题，我们提出了一个排名系统和等待策略。本文讨论了搜索顺序问题的原因，并展示了如何将排名系统和等待策略集成到标准的可达性算法中，以分别缓解和防止问题。实验表明，这两种方法的组合给出了最佳的搜索顺序在标准的基准测试，除了一个例子。这表明，它应该用来代替标准的BFS算法的时间自动机的可达性分析。
Timed pushdown automata revisited
本文给出了下推自动机（PDA）的时间扩张的两个结果。作为我们的第一个结果，我们证明了Abdulla等人的密集时间PDA模型的崩溃：它在表达上等价于具有无时间堆栈的密集时间PDA。出于这一结果，我们主张的框架，一阶可定义的PDA，一个专门的PDA在原子集，作为正确的设置来定义和调查的时间扩展的PDA。这样得到的一般模型是图灵完备的。作为我们的第二个结果，我们证明了NEXPTIME上界复杂性的非空性问题的表达子类。作为一个副产品，我们得到了一个严格的EXPTIME复杂性约束的一个更严格的子类PDA与永恒的堆栈，从而包含已知的密集定时PDA的复杂性约束。
Reducing Clocks in Timed Automata while Preserving Bisimulation
随着时钟数目的增加，模型检验时间自动机变得越来越复杂。因此，人们希望用尽可能少的时钟来构造一个自动机。检查是否存在一个具有较少时钟的时间自动机，使得原始自动机接受的时间语言被保留的问题是不可判定的。在本文中，我们给出了一个结构，它对任何给定的时间自动机产生一个时间双相似自动机与最少数量的时钟。此外，我们表明，这样一个自动机的最小可能数量的时钟可以构建的时间是双指数的原始自动机的时钟的数量。
Relating timed and register automata
时间自动机和寄存器自动机分别是时间字和数据字上的著名计算模型。前者具有允许测试两个事件之间的时间流逝的时钟，而后者包括可以存储数据值以供稍后比较的寄存器。虽然这两个模型在外观上表现不同，但两个模型的几个决策问题具有相同的（非）可判定性和复杂性结果。作为一个突出的例子，空性是可判定的交替自动机与一个时钟或寄存器，都具有非原始递归复杂性。这不是偶然的。这项工作证实了这两个模型之间确实存在紧密的关系。我们表明，运行的时间自动机可以模拟的寄存器自动机，反之，运行的寄存器自动机可以模拟的时间自动机。我们的研究结果允许在这两种模型之间来回转移复杂性和可判定性结果。我们证明这些减少的有用性，通过获得新的结果注册自动机。
Average-Time Games on Timed Automata
在有限时间自动机的无限图上进行平均时间博弈。两个玩家，Min和Max，通过轮流执行定时转换来构建自动机的无限运行。最小博弈者希望最小化每次转移的平均时间，而最大博弈者希望最大化每次转移的平均时间。一个直接的结果是平均时间博弈的决定性的一个初等证明。这补充了我们对可达时间博弈的研究结果，并部分解决了Bouyer等人提出的问题，在定价时间自动机上设计求解平均价格博弈的算法。本文还建立了求解平均时间对策的精确计算复杂性：对于至少有两个时钟的时间自动机，该问题是EXPTIME完全的。
Language Preservation Problems in Parametric Timed Automata
本文研究参数化时间自动机中非定时语言与迹保持问题的可判定性，证明一般情形不可判定，但单时钟及单参数确定性L/U-PTA可判定，并考虑鲁棒版本。
Real-Time Model-Checking: Parameters everywhere
本文研究离散时间自动机上逻辑TCTL的模型检验和参数综合问题，其中参数在模型（时间自动机）和属性（时态公式）中都允许.我们的结果如下。在消极的一面，我们表明，模型检验问题的TCTL扩展参数是不可判定的离散时间自动机只有一个参数时钟。不可判定性结果需要逻辑上的等价性。在积极的一面，我们表明，模型检验和参数合成问题成为可判定的一个片段的逻辑是不允许的平等。我们的方法是基于自动机理论的原则和扩展我们的方法来表示时间自动机使用Presburger算法的运行持续时间。
Timed Automata Semantics for Analyzing Creol
我们给出了一个实时语义的并发，面向对象的建模语言克里奥尔，克里奥尔进程映射到网络的时间自动机。我们可以使用我们的语义来验证Creol对象的实时的属性，特别是看看进程是否可以正确调度并满足其端到端的最后期限。实时Creol可以用于分析，例如，多核嵌入式系统的抽象模型。我们展示了如何在Uppaal进行分析。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。