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求解器的存在。证人的形状表明，模拟测试在实践中可能是有效的。
2018-06-28 cs.LO
Reachability Problem for Weak Multi-Pushdown Automata
本文研究了多下推自动机的一个受限子类的可达性分析。我们假设自动机的控制状态是偏序的，并且自动机的所有转换都是相对于顺序向下的。我们证明了可达性问题的可判定性和向后可达集的可计算性。作为主要的贡献，我们确定相关的子类的可达性问题成为NP完全。这与无通信向量加法系统（无状态多下推自动机的特殊情况）的相同问题的复杂性相匹配。
2013-09-20 cs.FL cs.LO
Improving search order for reachability testing in timed automata
时间自动机可达性分析的标准算法对自动机的转换顺序很敏感。为了解决这个问题，我们提出了一个排名系统和等待策略。本文讨论了搜索顺序问题的原因，并展示了如何将排名系统和等待策略集成到标准的可达性算法中，以分别缓解和防止问题。实验表明，这两种方法的组合给出了最佳的搜索顺序在标准的基准测试，除了一个例子。这表明，它应该用来代替标准的BFS算法的时间自动机的可达性分析。
2015-06-23 cs.FL cs.LO
Reachability of Communicating Timed Processes
我们研究的可达性问题的通信时间进程，在离散和密集的时间。我们的模型包括自动机与本地的时间限制通信无界FIFO通道。每个自动机只能访问其本地时钟集;所有时钟都以相同的速率进化。我们的主要贡献是一个完整的表征的可判定和不可判定的通信拓扑结构，离散和密集的时间。我们也得到了复杂性的结果，通过显示，通信时间的进程至少是硬的Petri网，在离散时间，我们也表现出等价的Petri网。我们的研究结果遵循相互拓扑保持时间自动机和（非定时）计数器自动机之间的减少。
2012-10-17 cs.LO
Binary reachability of timed pushdown automata via quantifier elimination and cyclic order atoms
我们研究了一个扩展了模块和分数时钟约束的时间下推自动机的表达模型。我们表明，二进制可达性关系是有效的混合线性算术与合理的整数排序表示。这包含了类似的可表达性结果，以前已知的有限和下推定时自动机与不定时堆栈。作为关键的技术工具，我们使用量词消去的混合线性算术的一个片段和循环顺序原子，并减少注册下推自动机循环顺序原子。
2018-04-28 cs.FL cs.LO
Improved Undecidability Results for Reachability Games on Recursive Timed Automata
我们研究递归时间自动机（RTA）上的可达性游戏，推广Alur-Dill时间自动机的递归过程调用机制类似于递归状态机。对于具有两个或多个时钟的自动机，RTA上的可达性博弈中的胜者判定问题是不可判定的，而对于只有一个时钟的自动机，该问题是可判定的。Ouaknine和Worrell最近提出了一个实时验证的时间有界理论，声称对有界时间的限制恢复了与实时验证相关的几个关键决策问题的可判定性。我们重新审视了具有时间限制的递归时间自动机上的博弈，希望能恢复可判定性。然而，我们发现，这个问题仍然是不可判定的递归时间自动机与三个或更多的时钟。使用类似的证明技术，我们的特点是一个可判定性边境的推广RTA递归秒表自动机。
2014-08-26 cs.FL cs.LO
Reachability relations of timed pushdown automata
时间下推自动机（TPDA）是一种将递归与时间约束逻辑相结合的表达形式。我们证明了TPDA的可达性关系可以用线性算术表示，这是一种丰富的逻辑，推广了Presburger算术和有理算术。的主要技术成分是一个新的量词消去结果的时钟约束（用于简化TPDA转换的语法），使用时钟差关系来表达的分数时钟值的可达性关系，和应用帕里克定理重建的积分时钟值。
2020-12-30 cs.FL cs.LO
Verification of Parametric Markov Automata under Time-bounded Reachability
Eindhoven University of Technology（埃因霍温理工大学）
针对参数化马尔可夫自动机（pMA），提出通过离散化为参数化马尔可夫决策过程（pMDP）并分析，解决时间有界可达性概率的合成问题，实现参数空间的满足/违反区域划分。
2026-06-23 cs.LO
Fast zone-based algorithms for reachability in pushdown timed automata
由于时间自动机的多功能性，大量的工作已经发展到考虑时间自动机的扩展。一个已经引起很多兴趣的扩展是具有可能无界堆栈的时间自动机，也称为下推时间自动机（PDTA）模型。虽然不同的算法已经给出了这个模型的不同变体的可达性，这些结果中的大多数是纯理论的，并没有产生有效的实现。其中一个主要原因是这些算法（以及现有的实现）都没有使用所谓的基于区域的抽象，而是依赖于区域抽象或其他方法，这些方法很难实现。在本文中，我们表明，一个天真的扩展的区域为基础的可达性算法的控制状态可达性问题的时间自动机是不健全的堆栈的存在。为了更好地理解这一点，我们给出了一个基于归纳规则的时间自动机的区域可达性算法。这个替代视图允许我们分析和调整规则，使其也适用于下推时间自动机。我们得到了第一个基于区域的算法PDTA是终止，健全和完整的。我们实现了我们的算法在工具中的Tendash和进行实验，以显示其有效性，从而为更实用的方法来验证下推定时系统的方式。
2021-07-19 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
Reachability and liveness in parametric timed automata
本文研究参数化时间自动机（PTAs）的可达性与活性，通过提出整数点PTAs子类推进可判定性边界，并证明L/U-PTAs中无限运行存在性为PSpace完全，而死锁存在性不可判定。
2022-02-07 cs.LO
Reachability-time games on timed automata
在可达性-时间博弈中，玩家Min和Max选择移动，使得在时间自动机中到达最终状态的时间分别最小化或最大化。Asarin和Maler使用值迭代算法证明了强非Zeno时间自动机上可达时间博弈的可判定性。本文补充他们的工作，提供了一个战略改进算法的问题。由于所提出的策略改进算法解决了所有时间自动机上的可达时间博弈，因此也推广了他们的可判定性结果。精确的计算复杂性解决可达时间游戏也建立：问题是EXPTIME完全的时间自动机至少有两个时钟。
2009-07-20 cs.CC cs.DS cs.GT
An algorithmic approximation of the infimum reachability probability for Probabilistic Finite Automata
给定一个概率有限自动机（PFA），一组状态S和一个错误阈值e > 0，我们的算法近似于自动机到达S的下确界概率（量化所有无限词）。我们的结果对比与已知的结果，近似问题是不可判定的，如果我们考虑的上确界，而不是下确界。由于我们研究的是到达一组状态的概率，而不是以接受状态结束的概率，因此我们的工作与模型检验的关系比与形式语言的关系更大。
2010-09-20 cs.FL 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
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
Re-verification of a Lip Synchronization Protocol using Robust Reachability
时间自动机是描述和分析实时系统的重要模型。鲁棒性是在时钟出现小漂移或测试防护装置不精确的情况下模型的正确性。实现了一种分析时间自动机鲁棒性的符号算法。在本文中，我们重新分析了一个工业案例唇同步协议使用新的鲁棒可达性算法。这个唇同步协议是一个有趣的情况下，因为定时方面是至关重要的协议的正确性。该模型的几个版本被认为是：一个理想的视频流，锚定抖动，和非锚定抖动。
2010-03-01 cs.LO
Adding Time to Pushdown Automata
在本教程中，我们将通过示例说明如何结合两个经典模型，即下推自动机（PDA）和时间自动机，以获得时间下推自动机（TPDA）。此外，我们描述了如何可达性问题TPDA可以减少到PDA的可达性问题。
2012-12-17 cs.FL cs.LO
Interrupt Timed Automata with Auxiliary Clocks and Parameters
时间自动机（ITA）是一种表达性的时间模型，根据级别考虑中断。由于这一特点，这种形式主义是不可比拟的时间自动机。然而，已经获得了一些与可达性和模型检验相关的可判定性结果。我们添加辅助时钟ITA，从而扩大其表达能力，同时保持可达性的可判定性。此外，我们定义了一个参数化版本的ITA，多项式的参数出现在警卫和更新。虽然参数推理与时间模型特别相关，但它经常导致不可判定性结果。我们证明了各种可达性问题，包括“强大的”可达性，是可判定的这个模型，我们给一个固定或可变数量的时钟，水平和参数的复杂性上界。
2014-09-08 cs.FL cs.LO
Expected Reachability-Time Games
概率时间自动机是一个合适的形式主义建模系统的实时，不确定性和概率行为。我们研究两个玩家零和游戏的自动机，游戏的目标被指定为预期的时间达到一个目标。两个玩家-被称为玩家Min和玩家Max-通过同时提出定时移动来竞争，并且执行延迟较短的移动。第一个玩家试图最小化给定的目标，而第二个玩家试图最大化目标。我们观察到，这些游戏是不确定的，并研究决策问题有关的计算上限和下限值，表明问题是可判定的，并在于复杂性类NEXPTIME $\cap$合作NEXPTIME。
2016-04-15 cs.LO
The Cost of Parameterized Reachability in Mobile Ad Hoc Networks
我们调查的影响，自发运动的复杂性验证问题的自动机为基础的协议模型的网络与选择性广播通信。我们首先考虑错误状态的可达性，并证明参数化验证是可判定的多项式复杂性。然后，我们转向更丰富的查询，并显示当考虑具有否定或基数约束的属性时，复杂性如何变化。
2012-02-27 cs.LO
Numerical Simulation guided Lazy Abstraction Refinement for Nonlinear Hybrid Automata
该草案提出了一个新的反例引导抽象精化（CEGAR）框架，该框架使用非线性微分方程的数值模拟与线性混合自动机（LHA）的线性规划相结合，对非线性混合自动机进行可达性分析。还引入了$ε-$结构鲁棒性的概念，该概念允许算法使用数值模拟来验证反例。保留字：验证，模型检验，混杂系统，混杂自动机，鲁棒性，鲁棒混杂系统，数值模拟，cegar，抽象精化。
2006-11-13 cs.LO
Markov Automata with Multiple Objectives
马尔可夫自动机结合了非确定性，概率分支和指数分布延迟。这种连续时间马尔可夫决策过程的组合变体被用于可靠性工程、性能评估和随机调度。到目前为止，它们的核查侧重于单一目标，如（定时）可达性和预期成本。在实践中，这些目标往往是相互依赖的，目的是揭示权衡取舍。我们提出的算法，同时分析几个目标和近似帕累托曲线。这包括，例如，多个（定时）可达性目标或各种预期成本目标。我们还考虑其组合，如在预算内的时间目标-哪些政策保证达到目标状态的最后期限内至少有概率$p$，同时保持允许的平均成本低于阈值？我们采用现有的方法为经典的马尔可夫决策过程。主要的挑战是如何对待利用国家居留时间的政策，即使是为了不定时的目标。实验结果表明了该方法的可行性和可扩展性。
2017-05-10 cs.LO
Decision Questions for Probabilistic Automata on Small Alphabets
研究一元和二元概率有限自动机的空性与$\lambda$-可达性问题，根据歧义度和字母表大小刻画其复杂度，揭示了多项式与有限歧义下的NP困难性及EXPTIME可解性。
2023-12-20 cs.FL cs.LO
Better abstractions for timed automata
我们考虑时间自动机的可达性问题。这个问题的一个标准解决方案涉及计算一个搜索树，其节点是区域的抽象。这些抽象保留了自动机状态空间上的底层模拟关系。出于有效性和效率的原因，它们由自动机的保护中发生的最大下限和上限（LU-边界）参数化。我们考虑Behrmann等人定义的aLU抽象。由于这种抽象可能会产生非凸集，因此尚未在实现中使用。我们证明了aLU抽象是最大的抽象方面的LU边界是健全的和完整的可达性。我们还提供了一个有效的技术，使用aLU抽象来解决可达性问题。
2016-07-28 cs.FL cs.LO
Graph Reachability and Pebble Automata over Infinite Alphabets
设D表示一个无限字母表--一个由无限多个符号组成的集合。一个单词w = a_0 b_0 a_1 b_1. D上偶数长度的a_n b_n可以看作是一个有向图G_w，其顶点是出现在w中的符号，边是（a_0，b_0），（a_1，b_1），.，（a_n，b_n）。对于一个正整数m，定义一种语言R_m，使得一个词w = a_0 b_0. a_n b_n在R_m中当且仅当图G_w中存在一条从顶点a_0到顶点b_n的长度<= m的路。我们建立了无限字母表上卵石自动机的如下层次定理。对于每一个正整数k，（i）存在一个接受语言R_{2^k-1}的k-pebble自动机;（ii）不存在接受语言R_{2^{k+1} - 2}的k-pebble自动机。基于这一结果，我们建立了一些以前未知的关系，一些类的语言在无限的字母表。
2012-04-10 cs.FL cs.LO
Continuous One-Counter Automata
研究了连续单计数器自动机（COCA）的可达性问题。在这样的自动机中，转换由计数器值的上限和下限测试来保护。此外，与进行转换相关联的计数器更新可以（非确定性地）按零和一之间的非零因子按比例缩小。我们的三个主要结果如下：（1）证明了具有全局上下界检验的COCA的可达性问题是在NC 2中的;（2）在一般情况下，该问题是在多项式时间内可判定的;（3）具有参数计数器更新和界检验的COCA的可达性问题是在多项式层次内可判定的.
2021-02-03 cs.FL cs.LO
Probabilistic bounded reachability for hybrid systems with continuous nondeterministic and probabilistic parameters
本文提出了一种计算混合系统有界可达概率的算法，系统在有限数量的离散转换内到达不安全区域的概率。特别是，我们专注于混合动力系统的非线性常微分方程的解决方案（可能不确定的初始条件和参数），并给出了概率行为的初始参数分布为连续（可能无限支持）和离散随机变量的连续动态。我们的方法是定义一个适当的松弛（不可判定）的可达性问题，使它可以解决的$δ$ -完全决策程序。特别是，对于连续随机参数的系统，我们开发了一个有效的集成程序，计算一个任意小的区间，保证包含的可达性概率。在更一般的情况下，系统的不确定性和概率参数，我们的程序计算一个有保证的外壳的范围内的可达性概率。我们已经将我们的方法应用到一些非线性混合模型，并通过与Monte Carlo模拟的比较验证了结果。
2015-05-11 cs.LO
Complete Robust Hybrid Systems Reachability
Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）
本文提出鲁棒微分动态逻辑，证明其对混合系统可达性问题的绝对完备性，为精确语义的混合系统提供自动验证方法。
2026-07-24 cs.LO
Weighted automata on infinite words in the context of Attacker-Defender games
我们考虑具有可达性目标的无限状态攻防对策。该文件的结果是双重的。首先，我们证明了一个新的语言理论结果的加权自动机上无限的话，并显示其编码到攻击者-防御者游戏的框架。其次，我们使用这个新的概念来证明不可判定性检查存在的一个获胜的策略在几个低维数学游戏，包括向量可达性游戏，文字游戏和辫子游戏。
2015-04-27 cs.FL cs.GT 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
State Space Reduction for Reachability Graph of CSM Automata
经典的CTL时态逻辑是建立在具有交错模型并发的系统上的。许多尝试是为了解决状态空间爆炸问题（例如，组合模型检验）。有一些基于动作独立性的状态空间缩减方法。然而，在CSM模型，这是基于重合而不是交错，动作的独立性不能定义。因此，提出了基于相同的时间后果，而不是独立的行动的状态空间约简。新的减少不如交织系统好，因为在减少之前必须获得状态的所有后继者（在两个级别的深度）。这导致状态空间的表示所需的空间的减少，但不是在状态空间构造的时间。然而，在CSM系统的常规状态空间中可能会发生很多节省。
2017-10-25 cs.FL cs.LO cs.SE
Minimal-Time Synthesis for Parametric Timed Automata
参数时间自动机（PTA）通过允许时钟约束中的参数来扩展时间自动机。这样的形式主义是有用的，例如推理时，在一个定时系统中的未知延迟。使用现有技术，用户可以合成允许系统到达指定目标位置的参数约束，而不管内部时钟已经过去了多少时间。我们专注于综合参数，不仅达到目标位置，但我们也解决了以下问题：什么是最短的时间到达目标位置？对于哪些参数值，我们可以实现这一点？我们分析了这个问题，并提出了一个算法来解决它。我们还讨论了最小化一个特定的参数值，仍然达到目标，并提供解决方案。我们实证研究这些算法的性能在一个基准集的PTA和最小时间可达性合成是更有效的计算比标准的合成算法的可达性。
2019-02-08 cs.LO
A Cegar-centric Bounded Reachability Analysis for Compositional Affine Hybrid Systems
针对组合混合系统可达性分析中乘积自动机位置爆炸的问题，提出以CEGAR为核心的有界可达性分析算法，结合不同组合语义与缓存优化，在SAT-Reach工具中实现并验证了可扩展性优势。
2025-09-03 cs.LO
Generating Concurrency Checks Automatically
本文介绍了ATAB，这是一个自动为动作树生成成对可达性检查的工具。动作树可以用来研究现实世界中并发程序的行为。ATAB将成对可达性检查编码到交替树自动机中，以确定动作树是否具有程序中任何一对给定点同时可达的调度。由于成对可达性问题是不可判定的，因此ATAB通常在基于锁的并发的受限形式下操作。ATAB产生的交替树自动机比以前使用的更紧凑，更有效地检查。该过程是完全自动化的，这简化了对更复杂的动作树进行编码检查的过程。产生的交替树自动机比以前的构造更容易扩展到大量的锁。
2016-04-22 cs.FL cs.LO
Invariants for One-Counter Automata with Disequality Tests
研究带不等性测试的单计数器自动机可达性问题，通过引入几乎归纳的泄漏不变量对可达集核心进行过度近似，将问题复杂度上界降至多项式层级第二层。
2024-08-21 cs.FL cs.LO
Minimal witnesses for probabilistic timed automata
见证子系统在概率系统的分析中被证明是一个有用的概念，例如作为关于为什么给定属性成立的诊断信息或作为细化算法的输入。介绍了概率时间自动机（PTA）中可达性问题的见证子系统。使用一个新的操作差界矩阵，它示出了如何法卡斯证书的有限状态互模拟子系统的PTA可以被翻译成见证子系统。我们提出了算法的最小见证子系统的三个概念下的最小性，从不同的角度捕捉的时间行为的计算，并讨论了它们的复杂性。
2020-07-01 cs.LO
Complexity of Verification and Synthesis of Threshold Automata
Technical University of Munich（慕尼黑工业大学）
本文研究了阈值自动机的验证与合成问题的复杂性，证明了多个核心问题的计算复杂度，并提出了一种基于Presburger公式的新算法。
2025-11-28 cs.DC cs.LO
Lazy abstractions for timed automata
我们考虑时间自动机的可达性问题。这个问题的一个标准解决方案涉及计算一个搜索树，其节点是区域的抽象。出于效率原因，它们由自动机的保护中发生的最大下限和上限（LU-边界）参数化。我们提出了一个算法，是更新的搜索树的探索过程中的LU边界。为了保持它们尽可能小，只有当它们能够实现在未抽象系统中不可能的过渡时，才对边界进行细化。因此，我们的算法可以看作是一种懒惰的CEGAR算法的时间自动机。我们表明，在几个标准的基准测试，该算法是能够保持非常小的LU边界，从而大大减少了搜索空间。
2013-01-18 cs.LO
A Forward Reachability Algorithm for Bounded Timed-Arc Petri Nets
时间弧Petri网（TAPN）是Petri网模型的一种著名的时间扩展，并且已经针对该模型提出了几种时间自动机的网络转换。我们提出了一个直接的，基于数据库管理的算法向前可达性分析的有界TAPN扩展的运输弧，抑制弧和年龄不变。我们也给出了一个完整的证明其正确性，包括减少技术的基础上对称性和外推。最后，我们增加了一种新的状态空间减少技术的算法，引入了标记上的单调排序，并证明其可靠性，即使在存在的单调性破坏功能，如年龄不变量和抑制弧。我们实现的算法内的模型检查器TAPAAL和实验结果文件一个令人鼓舞的性能相比，验证方法，翻译TAPN模型UPPAAL时间自动机。
2012-11-27 cs.DS cs.LO
Goal-Oriented Reduction of Automata Networks
我们考虑网络的有限状态机具有本地的过渡条件的当前状态的其他自动机。在本文中，我们描述了一个针对给定的可达性性质量身定制的归约过程，其形式为“从全局状态s存在一系列转换，导致自动机g处于局部状态T”的状态。通过利用因果关系分析的个别自动机内的过渡，建议减少删除本地的过渡，同时保留所有的最小的痕迹，满足可达性。该过程的复杂性是多项式的本地状态和转换的总数，和指数的本地状态的数量在一个自动机。应用于自动机网络建模动态的生物系统，我们观察到，减少显着缩小了可达的状态空间，提高了大型网络的模型检查的易处理性。
2016-08-19 cs.DM cs.FL cs.LO
HySIA: Tool for Simulating and Monitoring Hybrid Automata Based on Interval Analysis
我们提出HySIA：一个可靠的非线性混合自动机（HA）和信号时序逻辑（STL）属性的运行时验证工具。HySIA用区间分析技术模拟HA，以便轨迹被急剧封闭在一组区间内。然后，HySIA计算模拟轨迹是否满足给定的STL属性;再次进行区间分析，以实现可靠性的计算。通过几个示例HA和STL公式演示了使用HySIA的模拟和验证。
2017-12-02 cs.LO
Model-Checking of Linear-Time Properties Based on Possibility Measure
利用可能性测度研究了可能性Kripke结构下的LTL模型检验。首先介绍了可能性Kripke结构的概念和相关的可能性测度，然后研究了有限可能性Kripke结构线性时间可达性和重复可达性的模型检验.引入了可能性Kripke结构的标准安全性和非正则性，深入研究了正则安全性和非正则性的有限自动机验证问题。证明了有限可能性Kripke结构中正则安全性和非正则性的验证可以转化为本文所介绍的乘积可能性Kripke结构中可达性和重复可达性的验证。文中给出了几个算例来说明本文所提出的方法。
2016-09-25 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
Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata
我们考虑由无限多个均匀设计的线性混合自动机组成的系统，其动态行为由它们与相邻系统的关系决定。我们提出了一类这样的系统和一类安全属性，其验证可以减少到验证（小）家庭的有界大小的相邻系统，并确定在这种情况下，验证问题是可判定的，分别。固定参数易于处理。我们说明了一个例子，从协调车辆指导的方法，并描述了一个实现，使我们能够自动执行这样的验证任务。
2016-01-07 cs.LO
On verification and constraint generation for families of similar hybrid automata
本文研究参数化及相似线性混合自动机系统的全局安全验证，利用分层推理与符号消去生成参数约束，使安全属性成为归纳不变量，并通过实现与示例验证方法。
2025-05-14 cs.LO
ProbReach: Verified Probabilistic Delta-Reachability for Stochastic Hybrid Systems
Newcastle University（纽卡斯尔大学）
ProbReach通过计算系统达到危险区域的概率，验证随机混合系统的概率可达性，采用delta可达性方法使问题可解。
2015-03-05 cs.LO cs.SY eess.SY
Fast algorithms for handling diagonal constraints in timed automata
解决时间自动机中可达性的一种流行方法是枚举表示为区域的可达赋值集。天真的区域枚举不会终止。多年来已经研究了各种终止机制。当自动机在守卫中具有对角约束时，提出有效的终止机制具有明显的挑战性。在本文中，我们提出了一个新的终止机制的时间自动机与对角约束的基础上，一个新的模拟区域之间的关系。与现有的方法相比，这种模拟的实现实验显示出显着的收益。
2019-04-18 cs.FL cs.LO
Delta-Complete Analysis for Bounded Reachability of Hybrid Systems
Carnegie Mellon University（卡内基梅隆大学）
本文提出了一种用于混合系统有界可达性问题的Delta-完全分析框架，通过求解实数上的Delta决策问题进行有界可达性检查，并考虑系统在数值扰动下的鲁棒性。
2014-04-28 cs.LO cs.SY eess.SY
Using non-convex approximations for efficient analysis of timed automata
时间自动机的可达性问题是问是否存在从初始状态到目标状态的路径。这个问题的标准解决方案涉及计算自动机的区域图，原则上可以是无限的。为了使图形有限，使用外推算子来近似区域。出于当前算法中的效率的原因，区域的外推总是区域，并且特别地，它是凸的。在本文中，我们建议解决的可达性问题，没有这样的外推算子。为了确保终止，我们提供了一个有效的算法来检查一个区域是否包含在另一个所谓的区域闭包中。虽然理论上更好，但闭合不能用于标准算法中，因为区域的闭合可能不是凸的。所提出的方法的另一个好处是，它允许在区域图的探索期间实时计算近似参数，这与在探索之前通过自动机的静态分析来计算近似参数的当前方法相反。这允许算法的进一步改进。有希望的实验结果。
2011-10-17 cs.FL cs.LO
A Complexity Dichotomy for Semilinear Target Sets in Automata with One Counter
该研究针对三类单计数器系统，通过引入Presburger公式的通用框架，证明了半线性目标集问题的复杂性二分定理，且可判定公式所属的复杂度侧。
2025-05-19 cs.CC cs.FL cs.LO
Decidability of Timed Communicating Automata
研究了时间通信网络的可达性问题。每个进程都是一个时间自动机，通过在无界FIFO通道上交换消息与其他进程进行通信。消息携带时钟，该时钟在发送和接收时以适当的定时约束进行检查。每个自动机只能访问它的本地时钟和发送/接收消息的消息时钟集。时间是密集的，所有的时钟都以相同的速度进化。我们的主要贡献是一个完整的特征的可判定和不可判定的通信拓扑结构概括和统一以前的工作。从技术的角度来看，我们使用量词消去和减少计数器自动机与寄存器。
2018-04-20 cs.DC cs.FL cs.LO
Safe & Robust Reachability Analysis of Hybrid Systems
Genova Univ.（热那亚大学）；Halmstad University（哈尔姆斯塔德大学）；Rice University（莱斯大学）
本文提出安全可达性概念，以解决混合系统可达性分析中的不安全问题，并探讨其在安全分析中的鲁棒性。
2017-09-17 cs.LO cs.SY eess.SY
O-Minimal Hybrid Reachability Games
在本文中，我们考虑一般混合系统上的可达性博弈，并区分这些博弈的两种可能的观察框架：要么系统的精确动态被玩家看到（这是完美的观察框架），要么只有起点和延迟被玩家知道（这是部分观察框架）。在第一个更经典的框架，我们表明，时间抽象互模拟是不足以解决这个问题，虽然它是足够的情况下，时间自动机。这就是为什么我们考虑另一个等价，即后缀等价的基础上编码的轨迹通过单词。我们表明，这个后缀等价一般是一个正确的游戏抽象。我们将这个结果应用到o-极小混杂系统，并在此框架下得到了可判定性和可计算性的结果。对于第二个框架，它假设部分观察系统的动态，我们提出了另一个抽象，称为超字编码，这是适合于解决该假设下的游戏。在这个框架中，我们还提供了可判定性和可计算性的结果。
2010-01-12 cs.GT cs.LO
Hybrid Automata for Formal Modeling and Verification of Cyber-Physical Systems
离散控制（“网络”）和模拟环境（“物理”）之间的紧密集成-通过有线或无线通信网络上的传感器和执行器-是网络物理系统的定义特征。因此，信息物理系统的功能正确性不仅关键地取决于模拟物理环境的动态，而且还取决于改变环境动态的离散控制所采取的决策。混合自动机的框架-介绍了由Alberr，Courcoubetis，Henzinger和Ho-提供了一个正式的建模和规范环境来分析网络物理系统的离散和连续部分之间的相互作用。混合自动机可以被认为是有限状态自动机的推广，其在每个状态下的动态由常微分方程系统控制。此外，混合自动机的离散转换是由这些实值变量的值的约束，并使这些变量的演化不连续的跳跃。考虑到混合自动机中动力学的丰富性，一般模型的基本验证问题（如可达性和可扩展性）是不可判定的，这也许并不奇怪。在这篇文章中，我们提出了一个审查的混合自动机作为建模和验证框架的网络物理系统，并调查一些关键结果有关的实际验证问题的混合自动机。
2015-03-17 cs.FL cs.LO
