Variations of Checking Stack Automata: Obtaining Unexpected Decidability Properties
我们引入了一个单向语言接受者模型（检查栈自动机的一个变体），并证明了以下可判定性性质：（1）确定性版本具有可判定的成员问题，但具有不可判定的空性问题。(2)非确定性版本有一个不可判定的成员问题和空性问题。有许多接受设备的模型，对于这些问题，确定性和非确定性版本之间没有区别，同样适用于空性问题。据我们所知，我们上面介绍的模型是第一个表现出性质（1）和（2）的单向模型。我们定义了另一个单向接受器族，其中非确定性版本具有不可判定的空问题，但确定性版本具有可判定的空问题。我们也不知道在文献中有其他模型具有这种性质。我们还研究了检查堆栈自动机的其他变体的可判定性特性（例如，允许多个堆栈、双向输入等）。令人惊讶的是，双向确定性机器与多个检查堆栈和多个反向有界计数器被证明有一个可判定的成员资格问题，一个非常一般的模型与此属性。
2019-03-07 cs.FL
A Symbolic Decision Procedure for Symbolic Alternating Finite Automata
我们引入符号交替有限自动机（S-AFA）作为一个表达，简洁，可判定的模型，用于描述任意字母表上的有限序列集。s-AFA上的布尔运算具有线性复杂度，这与非交替符号自动机的交和并的二次成本形成鲜明对比。由于这种简洁性，空性和等价性检查是PSpace困难的。我们介绍了一种算法，用于检查两个s-AFA的等价性的基础上互模拟同余。该算法允许我们利用SAT和SMT求解器的能力来有效地搜索s-AFA的状态空间。我们评估我们的决策过程中的两个验证和安全应用：1）检查可满足性的线性时序逻辑公式在有限的痕迹，2）检查等价的布尔组合的正则表达式。我们的实验表明，我们的技术往往优于现有的技术，它可以在这两个应用程序中是有益的。
2016-10-06 cs.FL
Model-checking branching-time properties of probabilistic automata and probabilistic one-counter automata
本文研究概率自动机及概率一计数器自动机对 PCTL 与 PCTL$^*$ 的模型检测，通过归约空性问题并构造行为等价的一计数器自动机，证明两类问题均不可判定。
2021-08-30 cs.FL cs.LO math.LO
Checking History-Determinism is NP-hard for Parity Automata
University of Warwick（华威大学）
通过证明非确定性奇偶自动机之间的模拟关系检查是NP难的，进而证明检查奇偶自动机的历史确定性也是NP难的，改进了Kuperberg和Skrzypczak在2015年的下界，并给出了单令牌和双令牌游戏判定问题的NP难性以及语言包含问题的拟多项式时间算法。
2024-01-23 cs.FL
Checking Timed Bisimilarity with Virtual Clocks
Technical University of Darmstadt（达姆施塔特工业大学）；University of Siegen（锡根大学）；Accso – Accelerated Solutions GmbH（Accso-加速解决方案有限公司）
本文提出了一种扩展区图的虚拟时钟表示法，用于解决定时自动机的双射性检查问题，该方法在平均情况下比区域图更小，并通过实验验证了其有效性。
2026-08-31 cs.FL
MTL-Model Checking of One-Clock Parametric Timed Automata is Undecidable
参数时间自动机扩展了时间自动机（Alfrer和Dill，1991），因为它们允许指定时钟值的参数边界。自1993年由Alfred，Henzinger和Vardi提出以来，已知具有一个时钟的参数时间自动机的空性问题是可判定的，而如果自动机使用三个或更多个参数时钟，则是不可判定的。该问题是开放的参数时间自动机与两个参数时钟。度量时态逻辑（Metric Temporal Logic，简称MTL）是一种广泛应用于实时系统的规约语言。时间自动机的MTL-模型检验是可判定的，无论时间自动机中使用多少时钟。本文证明了参数时间自动机的MTL-模型检验是不可判定的，即使该自动机只使用一个时钟和一个参数并且是确定的。
2014-04-01 cs.FL cs.LO
Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis
概率系统的模型检测问题主要依赖于将LTL转换为确定性Rabin自动机（DRW）。我们最近的Safraless翻译的LTL（F，G）片段产生较小的自动机相比，传统的方法。在这项工作中，而不是DRW，我们认为确定性自动机的接受条件作为广义拉宾对（DGRW）的析取。与DRW相比，LTL（F，G）公式到DGRW的Safraless翻译导致更小的自动机。我们提出了概率模型检测算法以及DGRW条件下的博弈求解。我们的新算法在理论界和实际评价方面都有所改进。我们比较PRISM与我们的新的翻译，并表明，新的翻译导致显着的改善。
2013-04-18 cs.FL cs.LO
Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata
Technische Universität Dresden（德累斯顿工业大学）
本文提出使用确定性有限自动机族(FDFA)和无歧义有限自动机族(FUFA)表示ω-正则性质，并给出多项式时间算法计算离散时间马尔可夫链满足该性质的概率，其中FUFA比FDFA更简洁。
2026-06-29 cs.FL
Model Checking Flat Freeze LTL on One-Counter Automata
本文解决了单计数器自动机上平坦冻结线性时序逻辑模型检测的可判定性开放问题，通过归约到带参数化相等性测试的可达性问题并转化为Presburger算术证明其可判定。
2018-12-06 cs.FL cs.LO
Equivalence Checking and Intersection of Deterministic Timed Finite State Machines
人们对定义具有丰富时间的自动机模型越来越感兴趣，例如用时钟扩展的有限自动机（时间自动机）。在本文中，我们研究确定性时间有限状态机（TFSM），即，有限状态机具有单个时钟、定时保护和超时，其将定时输入字转换为定时输出字。我们解决了等价性检查的问题，通过定义一个互模拟定时FSM的untimed的，反之亦然。此外，我们应用这些互模拟关系来建立两个定时有限状态机的交集，通过对它们进行反定时，相交并转换回定时交集。
2021-03-08 cs.FL
Model-Checking of Ordered Multi-Pushdown Automata
我们解决了有序多下推自动机的验证问题：下推自动机的多栈扩展，具有对栈转换的约束，使得弹出只能在第一个非空栈上执行。首先，我们证明了有序多下推自动机的空问题是在2 ETIME。然后，我们证明了，对于一个有序的多下推自动机，一个正则配置集的所有前身的集合是一个有效的可构造正则集。我们利用这一结果来解决全球模型检验，其中包括在计算一个有序的多下推自动机，满足给定的w-正则性质（可表示在线性时间的时间逻辑或线性时间μ演算）的所有配置的集合。作为一个直接的后果，我们得到了一个2 ETIME上界的有序多下推自动机的w-正则性质的模型检验问题（匹配其下限）。
2012-09-19 cs.FL cs.LO
Synchronized CTL over One-Counter Automata
该研究解决了单计数器自动机上同步计算树逻辑的模型检测问题，证明了其可判定性，并针对核心片段给出了非初等上界及基于分段周期性的复杂度结果。
2023-12-21 cs.FL
The Complexity of Checking Non-Emptiness in Symbolic Tree Automata
该研究将符号树自动机的可满足性问题分解为两类理论的可满足性问题，进而得到该类自动机及其带线性算术约束扩展的判定问题的紧计算复杂度界。
2023-11-09 cs.FL cs.LO
Deterministic Timed Finite State Machines: Equivalence Checking and Expressive Power
人们对定义随时间而丰富的自动机模型越来越感兴趣。例如，时间自动机被引入作为用时钟扩展的自动机。在本文中，我们研究了时间有限状态机（TFSMs）的模型，即，用时间丰富的FSM，它接受定时输入单词并生成定时输出单词。在这里，我们讨论了具有单个时钟的TFSM的一些模型：具有定时保护的TFSM、具有超时的TFSM以及具有定时保护和超时的TFSM。我们解决了所有三个模型的等价性检查的问题，我们比较他们的表达能力，特征的TFSM的子类定时警卫和TFSM的超时是等价的。
2014-08-26 cs.FL
On the Equivalence Checking Problem for Deterministic Top-Down Tree Automata
针对自顶向下确定性有限树自动机（DFTAs）的状态语言等价判定问题，提出将其转化为语言理论方程系统可解性检查的高效算法，通过代入与冲突检测开发判定程序，并证明其正确性、终止性及$O(n^2)$最坏时间复杂度。
2025-04-05 cs.FL math.LO
Polynomial Interrupt Timed Automata
时间自动机（ITA）是秒表自动机的一个子类，它的可达性和时间模型检验的一些变体即使在参数存在的情况下也是可判定的。它们非常适合于建模和分析实时操作系统。在这里，我们用多项式保护和更新来扩展ITA，从而得到多项式ITA（PolITA）类。我们证明了可达性和模型检验的一个定时版本的CTL的一阶理论的圆柱形分解方法的适应性的可判定性。与以前的方法相比，我们的程序以统一的方式处理参数和时钟。此外，我们表明，Polita是不可比拟的秒表自动机。最后，在保持可判定性的同时引入了额外的功能。
2015-04-17 cs.FL
A Pattern Logic for Automata with Outputs
我们引入了一个逻辑来表达自动机的结构特性与字符串输入，并可能在一些幺半群的输出。在这个逻辑中，讨论输出值的谓词集是参数的，我们提供了模型检查问题可判定的谓词的充分条件。然后，我们考虑三个特定的自动机模型（有限自动机，传感器和自动机加权整数-求和自动机-），并实例化的通用逻辑为他们每个人。我们给紧的复杂性结果的三个逻辑和模型检测问题，这取决于公式是否是固定的。我们研究我们的逻辑的表达能力，通过表达经典的结构模式，例如有限的模糊性和多项式模糊性的情况下，有限自动机，可确定性和有限值的情况下，传感器和求和自动机的特点。因此，我们的复杂性的结果，我们直接得到这些经典性质可以决定在PTIME。
2018-10-08 cs.FL
LTL Semantic Tableaux and Alternating $ω$-automata via Linear Factors
线性时态逻辑（LTL）是一种广泛使用的系统线性时间特性的规范框架。验证这些属性的标准方法是将LTL公式转换为合适的$ω$自动机，然后应用模型检验。我们重温Vardi的变换的LTL公式交替$ω$ -自动机和Wolper的LTL表方法的可满足性检查。我们观察到，这两种结构有效地依赖于分解成线性因子的公式。线性因子之前已经由Antimirov在正则表达式的上下文中引入。我们建立了线性因子的概念，并验证了基本性质，如扩展和有限性。我们的研究结果揭示了交替$ω$ -自动机和语义表之间的连接的新见解。
2017-10-18 cs.FL
Automata-Based Software Model Checking of Hyperproperties
我们开发了时态流逻辑（TSL）和超时态流逻辑（HyperTSL）模理论的模型检验算法。TSL扩展了线性时序逻辑（LTL）的存储单元，功能和谓词，使其成为一个方便的和表达的逻辑推理软件和其他系统的无限数据域。HyperTSL进一步将TSL扩展到hyperproperties的规范-与多个系统执行相关的属性。因此，HyperTSL可以在软件系统中表达信息流策略，如不干涉。我们用理论扩充了HyperTSL，得到了HyperTSL（T），并建立在LTL软件验证的方法上，得到了TSL和HyperTSL（T）的模型检验算法。这导致了一个合理但不一定完整的算法，用于HyperTSL（T）的forall*exists* 片段中包含的规范。我们的方法构成了第一个软件模型检验算法的时间hyperproperties与量词交替，不依赖于有限状态的抽象。
2023-03-26 cs.FL cs.LO
Verifying Quantum Circuits with Level-Synchronized Tree Automata (Technical Report)
本文提出基于层级同步树自动机的量子电路符号验证方法，将门操作复杂度降至至多二次方，并支持参数化验证，实验表明其可处理规模远超现有工具的问题。
2024-10-24 cs.FL cs.LO
History-Deterministic Parity Automata: Games, Complexity, and the 2-Token Theorem
University of Warwick（华威大学）
本文通过双令牌博弈刻画奇偶自动机的历史确定性，证明固定奇偶指数时可在多项式时间内判定，并给出历史确定性Büchi自动机的多项式时间确定化过程。
2025-01-21 cs.FL
UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata
本文介绍了实时验证工具uppaal的主要扩展uppaalsmc。UPPAALSMC允许在自然随机语义下对定价时间自动机的网络的性能特性进行有效分析。特别是，uppaalsmc依赖于统计模型检验方法的一系列扩展，该方法被推广用于处理实时系统和估计不可判定的问题。UPPAALSMC与友好的用户界面结合在一起，该用户界面允许用户以有效的方式指定复杂的问题，以及以概率分布的形式获得反馈，并比较概率以分析系统的性能方面。调查的重点是该工具的演变-包括建模和规范形式主义以及应用技术-连同该工具的应用案例研究。
2012-07-04 cs.FL cs.LO
Timed Automata Robustness Analysis via Model Checking
本文针对时间自动机在设计阶段因时间常数不确定及实现扰动导致规范违反的问题，提出了通过模型检查进行鲁棒性分析的概念与技术，以辅助修复模型并确保可达性与安全规范。
2022-07-28 cs.FL cs.LO
Markov Chains and Unambiguous Automata
本文提出一种多项式时间算法，用于对表示为无歧义自动机的ω-正则规范进行离散时间Markov链的模型检测，证明其复杂度属于NC，与确定性自动机界限匹配且更具简洁性。
2023-04-07 cs.FL cs.LO
Space Complexity of Stack Automata Models
本文研究了栈自动机变体的空间复杂度的几种度量：非擦除栈自动机和检查栈自动机。这些度量捕获接受自动机语言中的每个单词所需的最小堆栈大小（弱度量），在任何接受单词的任何接受计算中使用的最大堆栈大小（接受度量），以及在任何计算中使用的最大堆栈大小（强度量）。我们给出了检查堆栈自动机的接受和强空间复杂度度量的详细特征。三种情况中的一种可能发生：复杂度要么被常数限制，表现得像线性函数，要么它不能被输入单词长度的任何函数限制（并且可以确定哪种情况发生）。然而，这个结果不适用于非擦除堆栈自动机;我们提供了一个例子，其中空间复杂度与输入长度的平方根成比例增长。此外，我们还研究了接受给定语言的机器的复杂性界，以及空间复杂度性质的可判定性。
2022-12-01 cs.FL
Equivalence checking for weak bi-Kleene algebra
本文刻画了允许语言等价性判定的Pomset自动机片段，证明其与序列有理表达式对应，从而给出序列有理表达式等价性可判定的新证明。
2021-08-11 cs.FL
Proving Safety with Trace Automata and Bounded Model Checking
循环欠近似是一种技术，它通过额外的分支来丰富C程序，这些分支代表了（有限的）循环迭代范围的效果。虽然这种技术可以显著地加速错误的检测，但它引入了冗余的执行跟踪，这可能使程序的验证复杂化。这对于基于有界模型检验的验证工具尤其如此，该工具结合了简化的算法来确定是否已经考虑了循环的所有可行迭代。我们提出了一种技术，使用\emph{trace automata}，以消除执行循环加速后的冗余执行。该方法减小了分析下的程序的直径，这在某些情况下足以允许使用有界模型检验的安全性证明。我们的转换是精确的-它不会引入假阳性，也不会掩盖任何错误。我们已经实现了分析作为一个源到源的转换，并提出了实验结果显示该技术的适用性。
2014-10-21 cs.FL cs.LO cs.PL
Symbolic Register Automata
符号有限自动机和寄存器自动机是有限自动机的两个正交扩展，它们的动机是现实世界中数据可能具有无界域的问题。这些自动机分别解决了对大型或无限字母表模型的需求。这两种自动机模型都有有趣的应用，并且本身就很成功。在本文中，我们介绍了符号寄存器自动机，一个新的模型，结合了符号和寄存器自动机的功能，与以前的应用程序是遥不可及的。我们研究了它们的性质，并提供了空性，包含性和等价性检查的算法，以及实验结果。
2019-05-23 cs.FL
TEMPORA: Efficient Verification of Metric Temporal Properties with Past in Pointwise Semantics
Indian Institute of Technology Bombay（印度理工学院孟买分校）；Université Paris-Saclay（巴黎萨克雷大学）；The Institute of Mathematical Sciences（数学科学研究所）；Homi Bhabha National Institute（霍米·巴巴国立研究所）；Chennai Mathematical Institute（金奈数学研究所）
本文提出了一种在点语义下高效验证度量时间属性的方法，通过将过去模态整合到转换网络中，并在翻译自动机时最大化确定性，从而提高了MITL模型检查的效率。
2026-05-18 cs.FL
On finitely ambiguous Büchi automata
Unambient Büchi自动机（Unambient Büchi automata），即每个字只允许一次接受运行的Büchi自动机，是Büchi自动机的一个有用的限制，非常适合于概率模型检查。在本文中，我们提出了一个更宽容的变种，即模糊不清的Büchi自动机，一个推广，每个字最多有$k$接受运行，一些固定的$k$。我们适应现有的概念和结果，有限和有界的模糊性的有限自动机的设置$ω$语言，并提出了一个翻译从任意不确定的Büchi自动机与$n$状态的模糊自动机与最多$3^n$状态和最多$n$接受运行每个字。
2018-09-25 cs.FL
Refinement Checking for Multirate Hybrid ZIA
混杂系统是一个既有离散分量又有连续分量的动态系统。为了研究混合系统的建模和验证问题，本文首先介绍了一种结合接口自动机、初始化多速率混合自动机和Z语言的规范化方法MZIA。同时，我们提出了一个加细关系MZIA。在此基础上，给出了有限域MZIA之间加细关系的检验算法，并证明了算法的正确性。
2014-10-13 cs.FL cs.LO
Tree Regular Model Checking for Lattice-Based Automata
树规则模型检验（TRMC）是分析无限状态系统的一系列技术的名称，其中状态由项表示，状态集由树自动机（TA）表示。TRMC的核心问题是判断一组坏状态是否可达。计算表示可达状态集合（的过近似）的TA的问题是不可判定的，但是存在基于树换能器的完成或迭代的有效解决方案。不幸的是，TRMC框架无法有效地捕获系统的复杂结构及其某些功能。作为示例，对于JAVA程序，项的结构主要用于捕获系统的状态的结构。相反，Java程序的整数必须用Peano数编码，这意味着任何代数运算都可能由数千个重写规则的应用程序表示。在本文中，我们提出了格树自动机（LTA），树自动机的扩展版本，其叶子配备了格。LTA允许我们表示可能无限的解释术语集。这些术语能够以有效的方式表示复杂的域和相关操作。我们还将经典的布尔运算扩展到LTA。最后，作为一个主要的贡献，我们引入了一个新的基于完成的算法计算可能无限的可达解释条款在有限的时间。
2012-03-07 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
The Power of Proofs: New Algorithms for Timed Automata Model Checking (with Appendix)
本文提出了第一个模型检测算法的表达模态μ演算的时间自动机，$L^{\mathit{rel}, \mathit{af}}_{ν,μ}$，并报告性能结果的实现。该μ演算包含扩展的时间模态算子，可以表示所有的TCTL。我们的算法方法使用了一个“在飞”的基础上证明搜索的策略，作为一种手段，确保高性能的积极和消极的答案模型检查问题。特别是，一组证明规则解决模型检查问题，并证明了健全和完整的，我们编码我们的算法在这些证明规则和模型检查的属性，通过构建一个证明（或显示不存在）使用这些规则。我们的技术的一个值得注意的方面是，我们表明，验证性能可以提高与\emph{derived rules}，其正确性可以推断出更原始的规则，他们是基于。在本文中，我们给出了基本的证明规则，我们的方法，描述派生的证明规则，以提高性能，并比较我们的实现这个模型检查器的UPPAAL工具。
2014-08-28 cs.FL cs.SE
Checking in Polynomial Time whether or not a Regular Tree Language is Deterministic Top-Down
本文纠正了既有多项式时间判定方法的错误，提出适用于任意确定性自底向上树自动机的正确性质，以判定正则树语言能否由确定性自顶向下树自动机识别。
2023-06-01 cs.FL
Direct Construction of Program Alignment Automata for Equivalence Checking
检查两个程序在语义上是否等价的问题有着广泛的应用，因此具有非常重要的意义。有几种技术可以解决这个问题，主要是通过构建一个产品程序，使其更容易获得有用的不变量。一个新的除了这些是一种技术，使用对齐谓词来对齐两个程序的痕迹，以构建一个程序对齐自动机。由谓词引导不仅有利于处理句法差异，而且有利于保持与属性的相关性。然而，基于跟踪的技术也存在缺点。获得覆盖所有程序行为的跟踪是困难的，并且任何欠近似都可能导致不完整的产品程序。此外，这种间接结构不知道缺失的行为，并且无法控制上述不完整性。针对这些问题，本文提出了一种直接构造程序对齐自动机的算法。
2021-09-04 cs.FL cs.SE
Model Checking Regular Language Constraints
即使是最快的SMT求解器在处理来自真实程序的正则表达式时也会遇到性能问题。由于这些性能问题通常来自问题表示（例如，非确定性有限自动机得到确定和正则表达式得到展开），我们重新审视布尔有限自动机，它允许直接和自然的表示任何正则语言的布尔组合。将IC3模型检验算法应用于布尔有限自动机，不仅可以有效地回答空性和普适性问题，而且通过扩展，可以判定多变量串成员问题的可满足性。我们证明了所产生的系统的有效性，一些流行的基准和正则表达式。
2017-08-30 cs.FL cs.LO cs.SC
Mata, a Fast and Simple Finite Automata Library (Technical Report)
本文介绍了一个用 C++ 编写的快速且简单的有限自动机库 Mata，它实现了模拟归约和反链语言包含检查等算法，提供 C++ 和 Python 接口，并在大规模基准上显著快于其他自动机库，同时支撑了高性能字符串求解器 Z3-Noodler。
2024-03-27 cs.FL
Experiments with Synchronizing Automata
本文改进了一种产生具有大长度最短复位字的同步自动机的算法。这已经通过改进一些已知的结果，关于复位长度的界限。我们的改进使得有可能考虑一些acquitures和开放的问题，同步自动机，检查它们的自动机与少量的状态和讨论的结果。特别是，我们已经验证了Čern猜想的所有二元自动机与最多12个状态，和所有三进制自动机与最多8个状态。
2016-07-14 cs.FL
An Automata-theoretic Basis for Specification and Type Checking of Multiparty Protocols
提出基于自动机的多方协议框架AMP，引入协议状态机与通信状态机规范，并提供完备的PSPACE投影操作与类型系统，显著提升了Multiparty Session Types的表达性、解耦性与鲁棒性。
2025-01-28 cs.FL cs.PL
A Linear-Time Nominal $μ$-Calculus with Name Allocation
无限字母表语言的逻辑和自动机模型，如Freeze LTL和寄存器自动机，用于验证过程或带有数据的文档。它们与名义集上的形式主义密切相关，例如非确定性轨道有限自动机（NOFA），其中名称扮演数据的角色。在这种形式主义中的推理问题在计算上往往是困难的。名字绑定的名义自动机模型，如规则的非确定性名义自动机（RNAs）已被证明是计算上更容易处理。在本文中，我们介绍了一个线性时间不动点逻辑Bar-muTL有限字在一个无限的字母表，它的特点是完全否定和冻结量化通过名称绑定。我们通过对扩展的正则非确定性名义自动机的非平凡约简表明，尽管Bar-muTL允许无限制的非确定性和无限多的寄存器，但RNAs上的模型检验Bar-muTL和可满足性检验都具有基本的复杂性.例如，模型检验在2 ExpSpace中，更准确地说是在参数化的ExpSpace中，有效地将寄存器的数量作为参数。
2021-08-20 cs.FL cs.LO
Fluid Model Checking of Timed Properties
我们解决的问题，验证马尔可夫模型的大人口的相互作用的代理，建模为有限状态自动机的时间属性。特别是，我们专注于时间有界的属性（随机）指定的确定性时间自动机（DTA）赋予一个单一的时钟个别代理。利用流体近似的思想，我们估计的DTA属性的满意概率，减少它的一个子类的时间非齐次马尔可夫更新过程的瞬态概率的计算与指数和确定性定时过渡，和一个小的状态空间。对于这个子类的模型，我们展示了如何推导出一组延迟微分方程（DDE），其数值解提供了一个快速和准确的估计满意的概率。本文还证明了该方法的渐近收敛性，并将其推广到一个简单的传染病传播模型上。最后，我们还展示了如何构建一个系统的DDE有效地近似平均数的代理，满足DTA规范。
2015-06-19 cs.FL
Interrupt Timed Automata: verification and expressiveness
我们介绍了类的混合时间自动机（ITA），一个子类的混合自动机非常适合于描述的时间多任务系统在单处理器环境中的中断。虽然可达性问题是不可判定的混合自动机，我们证明了它是可判定的ITA。更确切地说，我们证明了untimed语言的ITA是定期的，通过建立一个有限自动机作为一个广义类图。然后，我们建立ITA的可达性问题是在NEXPTIME和PTIME时，时钟的数量是固定的。为了证明第一个结果，我们定义了ITA的一个子类ITA-，并证明了（1）任何ITA都可以在ITA-中约简为一个语言等价的自动机，（2）这个子类中的可达性问题在NEXPTIME中（没有任何类图）。在接下来的步骤中，我们将研究ITA上实时的属性的验证。我们证明了模型检验SCL，一个片段的时间线性时间逻辑，是不可判定的。另一方面，我们给出了两个定时分支时间逻辑片段的模型检验过程。我们还比较了经典的时间自动机和ITA的表达能力，并证明了相应的家庭接受的语言是无与伦比的。结果也适用于受控实时自动机（CRTA），扩展时间自动机接受的语言。最后，我们结合ITA与CRTA，在一个模型，其中包括两个类，并表明可达性问题仍然是可判定的。此外，我们表明，ITA的语言既不是封闭的互补下，也没有交叉。
2012-03-29 cs.FL
A Note on Fault Diagnosis Algorithms
在本文中，我们审查算法检查离散事件系统和时间自动机的可诊断性。我们指出，在这两种情况下的可诊断性问题减少到空性问题（定时）Büchi自动机。此外，它是已知的，检查是否离散事件系统是可诊断的，也可以减少到检查有界可诊断性。我们建立了一个类似的时间自动机的结果。我们还提供了一个综合的复杂性结果，为不同的故障诊断问题。
2010-04-16 cs.FL cs.LO
From Automata Learning to Model Checking: Formal Security Verification of Black-Box Protocols
Mälardalen University（马尔默达尔大学）；AVL List GmbH（AVL李斯特有限公司）；AIT Austrian Institute of Technology GmbH（奥地利技术研究所有限公司）；KTH Royal Institute of Technology（皇家理工学院）
本文提出结合自动机学习与模型检查的方法，用于系统验证通信协议的安全属性，通过自动化流程减少建模工作量并提高安全性验证的自动化水平。
2026-09-14 cs.CR cs.FL
From $μ$-Calculus to Alternating Tree Automata using Parity Games
$μ$ -无限树上的微积分和自动机是描述无限树语言的互补方式。利用$μ$ -Calculus与交替树自动机之间的对应关系，将模式$μ$ -Calculus公式编译成交替树自动机，解决了可满足性和模型检验问题.因此提倡一个自动机模型，专门为工作模式$μ$ -微积分。与Janin和Walukiewicz提出的自动机模型相比，自动机模型的优点是能够以更简单的方式处理任意分支。这两个问题（即，模型检验和可满足性）分别通过约简到交替树自动机的相应问题，即接受问题和非空问题来解决。这些问题，反过来，解决使用奇偶性游戏的语义交替树自动机被翻译成一个获胜的战略，在一个适当的奇偶性游戏。
2016-02-02 cs.FL cs.LO
Precedence Automata and Languages
操作符先后次序语法定义了一个经典的布尔和确定性上下文无关族（称为Floyd语言或FL）。FL已经被证明严格包括众所周知的可见下推语言，并享受同样好的闭包属性。我们在这里介绍弗洛伊德自动机，一个等价的操作形式主义定义FL。这也允许扩展类来处理无限字符串，以执行例如模型检验。
2011-11-30 cs.FL
Certifying Emptiness of Timed Büchi Automata
时间自动机的模型检测器被广泛用于验证安全关键的实时系统。最先进的工具通过复杂的抽象实现可伸缩性。我们的目标是进一步提高他们的验证结果的信任，特别是检查活性属性。为此，我们开发了一种方法提取证书的空时间Büchi自动机从模型检验运行。这些证书可以由我们在Isabelle/HOL中正式验证的认证者进行双重检查。我们在一个抽象的环境中研究活性证书，并表明我们的方法是健全和完整的。为了证明它的可行性，我们提取了几个模型的证书，这些模型由Tandem和Imitator检查，并使用我们经过验证的认证器对其进行验证。
2020-07-08 cs.FL cs.LO
Higher-Order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties
本文研究一类非常一般的无限秩树的逻辑性质，即由高阶递归方案生成的无限秩树。我们考虑，对于一元二阶逻辑和模态μ演算，三个主要问题：模型检查，逻辑反射（又名全局模型检查，要求公式成立的元素集的有限描述）和选择（要求，如果存在的话，要求具有二阶自由变量的MSO公式成立的元素集的有限描述）。对于每一个问题，我们都提供了有效的解决方案。这是由于高阶递归方案和可折叠下推自动机之间的已知连接，并在以前的工作有关奇偶校验游戏上的过渡图的可折叠下推自动机。
2021-03-02 cs.FL cs.LO
Equivalence of Deterministic Weighted Real-time One-Counter Automata
本文引入了确定性加权实时单计数器自动机（DWROCA），并为其等价性问题提供了更简证明与更优多项式时间算法。
2024-11-17 cs.FL
Reduction of Nondeterministic Tree Automata
我们提出了一个有效的算法，以减少非确定性树自动机的大小，同时保留他们的语言。它是基于新的过渡修剪技术，和状态空间w.r.t.合适的等价物。它使用基于树上的向下和向上模拟前序的组合以及更一般的向下和向上语言包含的标准。由于树语言包含是EXPTIME完全的，我们描述的方法来计算良好的近似在多项式时间。我们实现了我们的算法作为一个模块的著名的libvata树自动机库，并测试其性能的一个给定的收集树自动机从各种应用程序的libvata定期模型检验和形状分析，以及对各类随机生成的树自动机。我们的算法产生的自动机大大小于和稀疏比所有以前已知的减少技术，它仍然是足够快，以处理大型实例。
2016-01-06 cs.FL
Deterministic Parikh automata on infinite words
本文研究无限字上所有帕里克自动机变体的确定性版本，比较其表现力并分析闭包性质与决策问题，发现确定性极限帕里克自动机最具优势，是唯一推广$\omega$-正则语言、布尔运算封闭且决策问题可判定的模型。
2024-05-24 cs.FL
Reducing Clocks in Timed Automata while Preserving Bisimulation
随着时钟数目的增加，模型检验时间自动机变得越来越复杂。因此，人们希望用尽可能少的时钟来构造一个自动机。检查是否存在一个具有较少时钟的时间自动机，使得原始自动机接受的时间语言被保留的问题是不可判定的。在本文中，我们给出了一个结构，它对任何给定的时间自动机产生一个时间双相似自动机与最少数量的时钟。此外，我们表明，这样一个自动机的最小可能数量的时钟可以构建的时间是双指数的原始自动机的时钟的数量。
2015-05-20 cs.FL 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
