Complementation of Emerson-Lei Automata (Technical Report)
本文提出了基于秩的 Büchi 自动机求补方法修改的 Emerson-Lei 自动机子类求补新构造，包括针对 Inf 接受条件布尔组合的专门构造和广义 Rabin 自动机求补技术，部分类别的上限比现有技术好指数倍。
2024-10-15 cs.FL cs.LO
A Tight Lower Bound for Streett Complementation
无限词上的有限自动机（$ω$ -automata）被证明是对反应系统的无限行为进行建模和推理的有力武器。补充$ω$ -自动机是至关重要的，在许多这些应用程序。但问题是不平凡的，即使经过广泛的研究，在过去的四十年中，我们仍然有一个重要类型的$ω$ -自动机，即Streett自动机，其中目前最好的下限$2^{Ω(n \lg nk)}$和上限$2^{Ω(nk \lg nk)}$之间的差距是巨大的，Streett指数大小$k$可以指数的状态数$n$。在arXiv：1102.2960中，我们给出了一个构造，用于补充Streett自动机，对于$k = O(n)$具有上界$2^{O(n \lg n+nk \lg k)}$，对于$k=ω(n)$具有上界$2^{O(n^{2} \lg n)}$。在本文中，我们建立了一个匹配的下限$2^{Ω(n \lg n+nk \lg k)}$的$k = O(n)$和$2^{Ω(n^{2} \lg n)}$的$k = ω(n)$，并因此表明，该结构是渐近最优的$2^{Θ(\cdot)}$符号。
2011-09-18 cs.FL cs.LO
Tight Upper Bounds for Streett and Parity Complementation
有限自动机在无限字上的互补问题不仅是自动机理论中的一个基本问题，而且是解决数理逻辑、模型检验、程序分析和验证等众多决策问题的基石。对于Streett互补，在当前下限$2^{Ω(n\lg nk)}$和上限$2^{O(nk\lg nk)}$之间存在显著的间隙，其中$n$是状态大小，$k$是Streett对的数量，并且$k$可以与$2^{n}$一样大。自80年代末以来，确定Streett互补的复杂性一直是一个悬而未决的问题。本文给出了一个互补结构，其上界$2^{O(n \lg n+nk \lg k)}$用于$k = O(n)$，$2^{O(n^{2} \lg n)}$用于$k = ω(n)$，它与\cite{CZ11a}中得到的下界匹配良好。我们还得到了一个紧的上限$2^{O(n \lg n)}$奇偶互补。
2011-06-13 cs.FL cs.LO
Kofola 1.0: A Modular Approach to ω-Regular Complementation and Inclusion Checking (Technical Report)
Brno University of Technology（布尔诺理工大学）；Aalborg University（奥尔堡大学）；Key Lab. of System Software (Chinese Academy of Sciences), ISCAS（中国科学院系统软件重点实验室）；Slovak University of Technology in Bratislava（布拉迪斯拉发斯洛伐克科技大学）
Kofola 1.0 提出了一种高效的 Büchi 自动机补集与包含检查工具，基于模块化补集框架，结合新启发式方法，实验证明其在实际应用中性能优越。
2026-06-29 cs.FL cs.LO
Approximate Automata for Omega-Regular Languages
无限词上的自动机，也被称为欧米伽自动机，在反应系统的验证和综合中起着关键作用。欧米茄自动机的谱由两个特征定义：接受条件（例如Büchi或宇称）和决定论（例如，确定性或非确定性）的自动机。这些特性在自动机理论的应用中起着至关重要的作用。例如，某些验收条件可以通过专用工具和算法比其他条件更有效地处理。此外，一些应用程序，如合成和概率模型检验，要求属性表示为某种类型的确定性欧米茄自动机。然而，属性并不总是由具有期望的接受条件和确定性的自动机表示。在本文中，我们研究的问题，逼近线性时间性质的自动机在一个给定的类。我们的近似是基于保留的语言，以用户定义的精度，在有限的套索表示的无限的执行，保留的大小。我们研究了不同类型的近似自动机的状态复杂性，并提供了不同的自动机类内的近似结构，例如，近似一个给定的自动机的一个更简单的接受条件。
2020-12-29 cs.FL cs.LO
Extending Büchi Automata with Constraints on Data Values
最近，数据树和数据字在XML推理和系统验证方面受到了相当大的关注。这些是树或词，除了来自有限字母表的标签之外，还携带来自无限字母表的数据值（数据）。一般来说，很难获得足够表达的数据字和树的逻辑，但对于可满足性问题仍然具有合理的复杂性。在本文中，我们扩展和研究的概念，Büchi自动机的欧米茄字的数据。我们证明了这种扩张的空性问题在初等复杂性下是可判定的。然后，我们应用我们的结果来显示两种逻辑的可判定性的欧米茄字的数据：一阶逻辑的两个变量的片段和一些经典的线性时序逻辑的欧米茄字的数据的扩展。
2012-06-23 cs.LO
Small witnesses, accepting lassos and winning strategies in omega-automata and games
在欧米茄自动机和具有欧米茄规则获胜条件的博弈中获得接受套索、证人和获胜策略是当今实践中常见的许多形式化方法的组成部分。尽管事实上，在大多数应用中，套索，证人和策略应该尽可能小，但很少有人知道获得这种小证书的难度。在本文中，我们调查已知的硬度的结果，并完成的情况下，在文献中没有考虑到的复杂性景观。我们特别注意的近似硬度的问题近似小的解决方案通常在实践中就足够了。
2011-08-01 cs.FL cs.LO
Profile Trees for Büchi Word Automata, with Application to Determinization
Buchi自动机的确定性问题是一个著名的问题，在综合、概率验证和多智能体系统中有着广泛的应用。自20世纪60年代以来，建筑一直在稳步发展：由McNaughton，Safra，Piterman，Schewe和其他人。尽管解决方案激增，但它们本质上都是特别的结构，除了正确性的证明之外，几乎没有理论支持。自Safra以来，所有的最优构造都采用树作为确定性自动机的状态，并且状态之间的转换在这些树上操作地定义。这些构造的操作性质使理解、实现和推理变得复杂，并且应该与互补形成对比，在互补中，自动机运行DAG的坚实理论是现代构造的基础。在2010年，我们描述了一种基于档案的布奇互补方法，其中档案只是访问接受国的历史。我们开发了一个结构理论的配置文件，并用它来描述一个互补建设，是确定性的限制。在这里，我们扩展了理论的配置文件证明，每一个运行DAG包含一个配置文件树，最多有一个有限数量的无限分支。然后，我们表明，这一属性提供了一个新的确定性建设的理论基础，其中宏观状态是双预序集的状态。与现存的确定性构造相反，新构造中的转换是声明性地而不是操作性地描述的。
2013-07-17 cs.FL cs.LO cs.SE
On the Generative Power of Omega-Grammars and Omega-Automata
ω-文法是用于生成ω-词（即无限长词）的形式文法，而ω-自动机是用于识别ω-词的自动机。本文给出了ω-文法和ω-自动机的干净而统一的定义，系统地研究了ω-文法相对于ω-自动机的生成能力，并给出了各种类型的ω-文法和接受模式的完整结果。我们使用元组（σ，ρ，π）来表示各种接受模式，其中σ表示某些指定的元素应该至少出现一次或无限次，ρ表示两个集合之间的某种二元关系，π表示正常或最左导子。在技术上，我们提出了（σ，ρ，π）-接受ω-文法，并系统地研究了它们相对于（σ，ρ）-接受ω-自动机的生成能力。我们给出了如何构造一些特殊形式的ω-文法，如ε-产生式自由ω-文法.通过建立转换技巧，研究了ω$-文法与ω-自动机之间的等价或包含关系.特别地，我们证明了对于某些接受模式，ω-CFG的生成能力严格弱于ω-PDA，而ω-CSG的生成能力等于ω-TM（而不是线性有界的ω-自动机类器件）.此外，我们提出了一些剩余的两个接受模式的开放问题。
2013-08-21 cs.FL cs.LO
First-Order Quantification over Automata
针对无限字模型上全称量化依赖补全自动机的难题，本文提出直接计算一元编码自然数公式中全称一阶量词对自动机影响的算法，以支持多种算术理论的可实现判定过程。
2023-06-07 cs.LO
Exploiting the Temporal Logic Hierarchy and the Non-Confluence Property for Efficient LTL Synthesis
从线性时序逻辑（LTL）规范合成反应系统的经典方法首先将给定的LTL公式转换为等价的omega-自动机，然后计算相应的omega-正则博弈的获胜策略。为此，所获得的欧米茄自动机必须（伪）确定，其中通常使用萨夫拉的确定过程的变体。在本文中，我们表明，这一确定步骤可以显着改善工具的实现取代萨夫拉的确定更简单的确定程序。特别地，我们利用（1）对应于由安全、活性、Buechi和co-Buechi自动机以及它们的布尔闭包组成的著名自动机层次的时态逻辑层次，（2）由LTL公式的某些平移产生的omega-自动机的非汇合性质，（3）Rabin-Scott和Miyano-Hayashi断点构造的确定过程的符号实现。特别是，我们提出了令人信服的实验结果，证明了我们的新的合成过程的实用性。
2010-06-08 cs.LO
A decidable class of (nominal) omega-regular languages over an infinite alphabet
我们定义了一类在无限个字母表上有无限个词的语言，以及相应的自动机。用于识别的自动机是确定性Muller自动机的一个推广，以设置名义集。值得注意的是，所获得的语言是由它们最终的周期性片段决定的，就像经典的情况一样。在补、并、交下的封闭性，以及空性和等价性的可判定性都被推广所保持。这是通过使用有限表示（否则无限状态）定义类的自动机。
2013-10-15 cs.FL cs.LO
Reward Shaping for Reinforcement Learning with Omega-Regular Objectives
Queen’s University Belfast（贝尔法斯特女王大学）；Institute of Software, CAS（中国科学院软件研究所）；University of Colorado Boulder（科罗拉多大学博尔德分校）；University of Liverpool（利物浦大学）
最近，已经成功地利用良好的MDP自动机（Büchi自动机与非确定性的限制形式）的无模型强化学习，一类自动机，包括良好的游戏自动机和最广泛的一类限制确定性自动机。使用这些Büchi自动机的基础是，Büchi条件，对于良好的MDP自动机，可以转化为可达性。这种翻译的缺点是，平均而言，奖励很晚才获得，这需要在学习过程中长时间的插曲。我们设计了一种新的奖励塑造方法来克服这个问题。我们表明，由此产生的模型是等价于一个有偏见的折扣，简化和改善以前的工作在这个方向上的折扣收益目标。
2020-01-16 cs.LG 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 Theory of Hanoi Omega-Automata and Games
Université libre de Bruxelles（布鲁塞尔自由大学）；University of Antwerp（安特卫普大学）
本文研究了HOA编码自动机与游戏的理论复杂性，证明非空问题为NP完全，语言包含问题在多数条件下为PSPACE完全，Emerson-Lei接受条件为EXPSPACE完全，并形式化了HOG游戏。
2026-04-27 cs.FL cs.LO
Deterministic Automata for the (F,G)-fragment of LTL
当在游戏或概率系统的设置中处理线性时序逻辑属性时，人们通常需要将它们表示为确定性欧米茄自动机。为了将LTL转化为确定性的omega-自动机，传统的方法首先将公式转化为非确定性的Büchi自动机。然后执行确定性过程，例如Safra，产生确定性ω-自动机。我们提出了一个直接的翻译的（F，G）-片段的LTL到确定性ω-自动机，没有涉及确定性的过程。由于我们的方法是针对LTL的，我们经常避免通常不必要的大爆破所造成的一般确定性算法。我们调查这种翻译的复杂性，并提供实验结果，并将其与传统方法进行比较。
2012-04-23 cs.FL cs.LO
Synthesis of Temporal Causality
本研究推广时序因果性框架，提出首个针对ω-正则效应的完备原因合成算法，证明其原因具有ω-正则性，可通过原型工具实现并验证了实际性能。
2025-06-17 cs.LO
Borel Ranks and Wadge Degrees of Context Free Omega Languages
我们表明，从拓扑的角度来看，考虑Borel和Wadge层次，1-计数器Büchi自动机具有相同的接受能力比图灵机配备一个Büchi接受条件。特别地，对于每一个非空递归序数α，都存在1-计数器Büchi自动机所接受的Sigma^0_α-完全和Pi^0_α-完全的上下文无关omega语言，并且上下文无关omega语言的Borel秩集的上确界是严格大于第一个非递归序数的序数γ ^[1_2]。这个令人惊讶的结果回答了H. Lescow和W. Thomas [无限计算的逻辑规范，在：“并发的十年”，LNCS 803，Springer，1994，第583-621页]。
2007-12-09 cs.GT cs.LO math.LO
The Extended HOA Format for Synthesis
我们提出了一个小的扩展河内欧米茄自动机格式定义反应合成问题。也就是说，我们添加了一个“可控制的AP”头项，指定原子命题的子集是可控的。我们描述了新格式的语义，并提出了一个输出格式的合成策略。最后，我们还评论了工具支持，旨在鼓励快速采用扩展的河内Omega-Automata格式进行合成。
2020-05-13 cs.FL cs.LO
Some Problems in Automata Theory Which Depend on the Models of Set Theory
我们证明了一些相当基本的问题，自动机阅读无限的话依赖于模型的公理系统ZFC。已知Büchi单计数器自动机$A$接受的Ω语言$L(A)$的补数的基数只有三种可能性。本文证明了如下令人惊讶的结果：存在一个1计数器Büchi自动机$A$，使得Ω语言$L(A)$的补$L(A)^-$的基数不是由ZFC决定的：（1）.存在ZFC的模型$V_1$，其中$L(A)^-$是可数的。（二）、存在ZFC的模型$V_2$，其中$L(A)^-$具有基数$2^{\aleph_0}$。（三）、存在ZFC的模型$V_3$，其中$L(A)^-$具有带$\aleph_0<\aleph_1<2^{\aleph_0}$的基数$\aleph_1$。我们证明了一个非常相似的结果，由2-磁带Büchi自动机$B$接受的无穷理性关系的补充。作为推论，这证明了连续统假设对于1-计数器omega-语言的补和对于2-带Büchi自动机所接受的无穷有理关系的补可能不满足.从上述结果的证明中我们可以推断，关于1-逆Ω-语言或无穷有理关系的基本决策问题实际上位于分析层次的第三层。特别地，确定1-计数器Ω语言（分别为无限有理关系）的补数是否可数的问题在$Σ_3^1 \setminus (Π_2^1 \cup Σ_2^1)$中。这是相当令人惊讶的，如果比较的事实，它是可判定的是否一个无限理性关系是可数的（分别，不可数）。
2011-08-14 cs.CC cs.FL cs.LO
Omega-Regular Objectives in Model-Free Reinforcement Learning
University of Liverpool（利物浦大学）；University of Colorado Boulder（科罗拉多大学博尔德分校）
我们提供了第一个解决方案，无模型强化学习的ω-正则目标的马尔可夫决策过程（MDP）。我们提出了一个建设性的减少从几乎肯定满足ω-正则目标的几乎肯定的可达性问题，并将这种技术推广到学习如何控制一个未知的模型，使满足目标的机会最大化。我们的技术的一个关键特征是将ω-正则性质编译成极限确定性Buechi自动机而不是传统的Rabin自动机;这种选择回避了破坏以前建议的困难。我们的方法使我们能够应用无模型，现成的强化学习算法来计算最佳策略的MDP的观察。我们提出了一个实验评估我们的技术对基准学习问题。
2018-09-26 cs.LG cs.LO stat.ML
On Decidability Properties of One-Dimensional Cellular Automata
在最近的一篇论文中，Sutner证明了一维元胞自动机$\mathcal{A}$的相空间$\mathcal{S}_\mathcal{A}=(Q^\mathbb{Z}, \longrightarrow)$的一阶理论是可判定的，该元胞自动机的配置是$Q^\mathbb{Z}$的元素，对于有限的一组状态$Q$，其中$\longrightarrow$是“下一个配置关系”。他问这个结果是否可以扩展到一个更有表现力的逻辑。本文证明了这一点。我们首先表明，对于每个一维元胞自动机$\mathcal{A}$，相空间$\mathcal{S}_\mathcal{A}$是一个欧米茄自动结构。然后，应用Kuske和Lohrey最近关于omega-自动结构的结果，可以得出结构$\mathcal{S}_\mathcal{A}$的一阶理论，用一些计数和基数量词扩展，是可判定的。我们给出了一维元胞自动机的一些新的可判定性质的例子。在满射元胞自动机的情况下，从Kuske和Lohrey关于有界度结构的结果可以推出一些更有效的算法。另一方面，我们表明，细胞自动机的情况下，自动图给出了新的结果。
2009-06-01 cs.CC cs.LO math.LO
RNN Generalization to Omega-Regular Languages
Imperial College London, UK（伦敦帝国学院）
本研究首次探究RNN对LTL导出的ω-正则语言的泛化能力，通过训练RNN复现Büchi自动机行为并测试分布外长序列，证实其在多数复杂任务上可实现高精度泛化，为神经符号验证提供了可行性支撑。
2025-09-02 cs.FL cs.LG cs.LO
Upper bounds for Newton's method on monotone polynomial systems, and P-time model checking of probabilistic one-counter automata
各类无穷状态递归概率系统分析和模型检验的中心计算问题（包括拟生灭过程、多类型分支过程、随机上下文无关文法、概率下推自动机和递归马尔可夫链）是{ \em终止概率}的计算，并且计算这些概率又归结为计算对应的{ \em单调多项式系统}（MPS）的方程的{ \em最小不动点}（LFP）解，表示为x=P（x）。Etessami和Yannakakis证明了牛顿方法的分解变体对于任何具有非负解的MPS单调收敛于LFP解。随后，Esparza，Kiefer和Luttenberger得到了牛顿方法对某些类型MPS的收敛速度的上界。最近，更好的上限已获得特殊类的MPS。然而，在本文之前，对于任意（不一定是强连接的）MPS，牛顿方法的收敛速度作为输入MPS的编码大小|P|的函数，x=P（x），根本没有上界。在本文中，我们提供了最坏情况下的上界，作为输入编码大小|P|和Σ> 0的函数，对于具有LFP解q^* 的任何MPS，分解牛顿法（即使有舍入）在q^* 的加性误差Σ> 0内收敛所需的迭代次数。我们的上界基本上是最优的几个重要参数。使用我们的上界，并建立在以前的工作，我们获得了第一个P-时间算法（在标准图灵计算模型）的定量模型检验，在所需的精度，离散时间QBD和（等效）概率1-计数器自动机，相对于任何（固定）ω-正则或LTL属性。
2013-04-26 cs.CC cs.LO
