Coalgebraic Semantics for Nominal Automata
本文提出了一种共代数方法来研究两种类型的非确定性自动机在名义集上的语言语义：非确定性轨道有限自动机（NOFA）和规则名义非确定性自动机（RNAs），这是在以前的工作中介绍。虽然NOFA是非确定性自动机的直接名义版本，但RNAs具有普通和名称绑定转换的功能。相应地，RNAs接受的单词是由普通字母和名称绑定字母组成的字符串。Bar语言是这些词模$α$等价的集合，并且对于RNA的每个状态，都关联其接受的Bar语言。我们表明，NOFA和RNAs的语义，分别出现作为一个实例的Kleisli风格的coalgebraic跟踪语义，以及实例的coalgebraic语言语义通过广义确定。在路上，我们重温coalgebraic迹语义一般，并给出了一个新的紧凑证明的主要结果，在该理论指出，初始代数的函子产生终端coalgebra的Kleisli扩展函子。我们的证明需要更少的假设函子比所有以前的。
2022-03-29 cs.LO
An Expressive Coalgebraic Modal Logic for Cellular Automata
Leiden University（莱顿大学）；Tallinn University of Technology（塔林理工大学）
本文提出了一种用于细胞自动机的余代数模态逻辑，通过行为等价性推断其行为，并证明了Hennessy-Milner定理。
2025-12-16 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
Fair Simulation for Nondeterministic and Probabilistic Buechi Automata: a Coalgebraic Perspective
本文从余代数视角统一推广公平模拟至非确定性树自动机和概率词自动机，并证明其可靠性以验证语言包含。
2017-09-05 cs.LO
A coalgebraic higher-order modal fixed-point logic
University of Sheffield（谢菲尔德大学）
研究引入高阶模态不动点逻辑的余代数扩展，包含HFL及其概率扩展，证明非确定性有限自动机空集问题和概率自动机值为1问题可归结为该余代数形式的模型检查问题。
2026-07-22 cs.LO
A coalgebraic take on regular and $ω$-regular behaviours
本文提出一个上代数框架，用单子定义有限和无限行为，并给出上代数Kleene型定理，适用于非确定性、树和概率自动机。
2021-12-22 cs.LO
Coalgebraic Automata Theory: Basic Results
我们将自动机理论中的一些中心结果推广到余代数的抽象层次，从而奠定了在无限对象上操作的自动机的普遍理论的基础。设F是任何保持弱拉回的集合函子。我们证明了F-余代数的可识别语言类在取联合、交集和投影下是封闭的。我们还证明了，如果一个非确定性的F-自动机接受一些余代数，它接受一个有限的自动机的大小。我们的主要技术成果涉及一个明确的建设，将一个给定的交替F-自动机到一个等价的不确定性，其大小是指数约束的大小的原始自动机。
2008-11-21 cs.LO
Uniform Interpolation for Coalgebraic Fixpoint Logic
利用自动机与逻辑之间的联系，证明了一类广泛的余代数不动点逻辑具有一致插值性。为此，首先，我们推广的核心结果之一，在共代数自动机理论，即闭包下的投影，这是众所周知的，持有弱拉回保持函子，一类更一般的函子，即;具有准函子lax扩张的函子。然后证明了投影闭包蕴含互模拟量词的可定义性，最后证明了一致插值定理。
2015-03-08 cs.LO
Fibrational Perspectives on Determinization of Finite-State Automata
本文从纤维化视角重新分析有限状态自动机的确定化，通过局部伴随和多重集相对伴随，改进并推广了确定化过程，提供了典范的前向及前向-后向模拟。
2025-09-24 cs.FL cs.LO math.CT
Coalgebraic Trace Semantics for Buechi and Parity Automata
尽管其成功地产生了许多一般性的结果，基于状态的动力学，理论的coalgebra一直在努力适应Buechi接受条件-一个基本概念，在理论的自动机无限的话或树。在本文中，我们提出了一个干净的答案的问题，建立在“极大性”的表征无限的痕迹（由雅各布斯和Cirstea）：公认的语言的Buechi自动机的特点是两个交换图，一个最小的同态和其他最大的，很像在一个系统（最小和最大）的不动点方程。这种特性对于非确定性分支和概率分支都是一致的，对于单词和树也是一样。我们提出了我们的结果的奇偶验收条件，推广Buechi的。
2016-06-30 cs.LO
Can Nondeterminism Help Complementation?
可补性和确定性是自动机理论中的两个基本概念。两者之间的密切关系在文献中已经得到很好的观察。在有限字上的非确定性有限自动机（NFA）的情况下，互补和确定具有相同的状态复杂度，即Theta（2^n），其中n是状态大小。对于布奇自动机，确定和互补之间也有相同的相似性，其中两种操作都具有2^Θ（n lg n）的状态复杂度。一个有趣的问题是，是否存在一种类型的欧米茄自动机，其确定性是相当困难的比它的补充。在本文中，我们证明了对于所有常见类型的omega-自动机，确定性问题具有相同的状态复杂性作为相应的补充问题的粒度为2^Θ（.）。
2012-10-09 cs.FL cs.LO
A Tighter Bound for the Determinization of Visibly Pushdown Automata
可视下推自动机（VPA）是下推自动机的一个子类，它的堆栈行为完全由输入符号按照输入字母表的固定划分来决定。自其引入以来，VPA已被证明在各种情况下是有用的，例如，作为验证的规范形式主义和处理XML流的自动机模型。然而，由于复杂性高，基于VPA框架的形式化验证的实现是一个挑战。在本文中，我们考虑的问题，实现基于VPA的模型检验算法。为此，我们首先提出了一个改进的上限确定VPA。接下来，我们提出简单的动态算法来检查该自动机类的普适性和包含问题。然后，我们在一个原型工具中实现了所提出的算法。最后，我们对随机生成的VPA进行了实验。实验结果表明，所提出的算法是相当快的比标准的。
2009-11-17 cs.FL cs.LO
Determinization of $ω$-automata unified
我们描述了一个统一的结构转换$ω$-自动机与任意接受条件（基于无限集的概念，即一组状态访问无限经常在运行的自动机）等价的确定性奇偶自动机（DPW）。给定一个具有$n$状态的非确定性自动机，我们的构造给出了一个最多具有$2^{O(n^2 \log n)}$状态和$O(n^2)$奇偶索引的DPW。因此，时间复杂度是O（n）的。时间复杂度O（n）当用$Ω{(2^n)}$接受对确定Rabin或Streett自动机时，我们的算法给出了状态数和奇偶指数的更好的渐近界，其中$n > 1$。我们证明了这一点，通过描述一个家庭的Streett（和拉宾）自动机与$2^{n}$非冗余的接受对，其中最有名的确定技术给出了一个DPW至少$Ω{(2^{(n^3)})}$状态，而我们的建设建设与$2^{O(n^2\log n)}$状态的DRW/DPW。一个简单的推论，我们的建设是，一个$ω$-语言拉宾指数$k$不能识别的任何$ω$-自动机（确定性或非确定性）少于$O(\sqrt{k})$状态。
2011-01-11 cs.FL cs.LO
On Complementation of Nondeterministic Finite Automata without Full Determinization (Technical Report)
本文研究避免完全确定化的NFA求补替代方法，基于逆幂集构造及两种利用NFA常见结构的新颖构造，实验证明这些方法在多数情况下能生成显著更小的补集。
2025-07-14 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
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
Proof Systems for the Modal $μ$-Calculus Obtained by Determinizing Automata
本文提出一种二叉树构造以确定化非确定性奇偶流自动机，并据此得到公式由二进制字符串元组标注的循环证明系统 $\mathsf{BT}$，其可靠性与完备性由确定化正确性直接导出。
2023-07-14 cs.LO
Exact and Approximate Determinization of Discounted-Sum Automata
折扣和自动机（NDA）是具有边权重的非确定性有限自动机，通过访问边权重的折扣和来评估游程。更准确地说，将行程的第i个位置的权重除以$λ^i$，其中折扣因子$λ$是大于1的固定有理数。一个词的值是自动机在其上运行的最小值。贴现求和是一种常见而有用的测量方案，特别是对于无限序列，反映了早期权重比后期权重更重要的假设。不幸的是，NDA的确定通常是形式化验证中必不可少的，但通常是不可能的。我们提供了积极的消息，表明每一个完整的折扣因子的NDA是可确定的。我们完成了图片证明，整数的特点正是折扣因子，保证可确定性：对于每一个非整数的合理折扣因子$λ$，有一个不可确定的$λ$ -NDA。我们还证明了具有积分折扣因子的NDA类在代数运算min，max，加法和减法下具有封闭性，这对于一般NDA和确定性NDA都不是这种情况。对于一般的NDA，我们研究近似确定，这总是可能的，因为一个词的后缀的影响衰减。我们表明，天真的方法，展开的自动机计算到一个足够的水平，是双指数的折扣因子。我们提供了一个替代的建设近似确定，这是单指数的折扣因子，在精度和状态的数量。我们还证明了匹配下界，这三个参数的指数依赖性是无法避免的。我们的所有结果同样适用于有限词上的自动机和无限词上的自动机。
2014-02-12 cs.FL cs.LO
A Coalgebraic Approach to Kleene Algebra with Tests
带有测试的Kleene代数是Kleene代数（正则表达式代数）的扩展，可用于推理程序。我们开发了一个coalgebraic理论的Kleene代数测试，沿线的coalgebraic理论的正则表达式的基础上确定性自动机。由于已知的自动机理论表示的Kleene代数与测试不借给自己的一个coalgebraic理论，我们定义了一个新的解释Kleene代数与测试表达式和相应的自动机理论表示。该理论的一个成果是一个共归纳证明原理，它可以用来建立我们的Kleene代数与测试表达式的等价性。
2004-05-26 cs.LO cs.PL
From Nondeterministic Büchi and Streett Automata to Deterministic Parity Automata
在本文中，我们重新Safra的确定性结构的自动机上无限的话。我们将展示如何构造具有较少状态的确定性自动机，最重要的是，奇偶校验接受条件。确定性在许多应用中被使用，例如树自动机的推理，CTL* 的可满足性，以及逻辑规范的可实现性和综合。所有这些应用的上界减少使用我们的建设产生的较小的确定性自动机。此外，奇偶校验接受条件允许使用更有效的算法（与处理Rabin或Streett接受条件相比）。
2007-08-14 cs.FL cs.LO
A No-go Theorem for Coalgebraic Product Construction
Research Institute for Mathematical Sciences, Kyoto University（京都大学数学科学研究所）；National Institute of Informatics（国立情报学研究所）；The Graduate University for Advanced Studies (SOKENDAI)（高级研究院（SOKENDAI））
本文提出关于代数积构造的不可行定理，并展示MC与MFAs的代数积构造作为新实例，解决多项式时间内的模型检查问题。
2026-02-21 cs.LO
On Delay and Regret Determinization of Max-Plus Automata
半环$(\mathbb{Z} \cup {-\infty}, \max, +)$上加权自动机的决定性问题是一个长期存在的问题。我们提出了两种方法来接近它通过限制搜索空间的确定性WA：k-延迟和r-遗憾。一个WA N是k-延迟可确定的，如果存在一个确定性自动机D，它定义了与N相同的函数，并且对于N语言中的所有词α，D在α上的接受游程总是与N在α上的最大接受游程最多相距k。也就是说，沿着相同长度的所有前缀，两个游程的权重的游程和之间的绝对差至多为k。一个WA N是r-后悔可决定的，如果对于它的语言中的所有词α，它的非决定性可以被动态地解决，以构造N的游程，使得它的值与N赋予α的值之间的绝对差至多是r。我们证明了WA是可确定的当且仅当它是k-延迟可确定的。因此，确定某个k的存在性与一般的确定性问题一样困难。当k和r被给定为输入时，k-延迟和r-后悔决定问题被证明是EXPtime-complete的.我们还表明，确定是否WA是r-后悔可确定的一些r是在EXPtime。
2017-03-03 cs.FL cs.GT cs.LO
Sound and complete axiomatizations of coalgebraic language equivalence
余代数提供了一个统一的框架来研究动力系统，包括几种类型的自动机。在本文中，我们利用系统的coalgebraic视图调查，在一个统一的方式，在何种条件下，是健全的和完整的行为等价的演算可以扩展到一个粗糙的coalgebraic语言等价，这产生于一个广义的powerset建设，确定coalgebras。我们表明，建立健全性和完整性证明表达式模公理的微积分形式的合理不动点的给定类型函子。我们的主要结果是函子$FT$的有理不动点，其中$T$是描述系统分支的单子（例如非确定性，权重，概率等），有一个商的合理不动点的“确定”型函子$\bar F$，提升$F$的范畴$T$ -代数。我们应用我们的框架加权自动机的具体例子，我们提出了一个新的声音和完整的演算加权语言等价。作为一个特殊的情况下，我们得到非确定性自动机，在那里我们恢复Rabinovich的声音和完整的演算语言等价。
2017-03-17 cs.LO math.CT
Deciding Entailments in Inductive Separation Logic with Tree Automata
具有归纳定义的分离逻辑（SL）是用于指定复杂递归数据结构的自然形式主义，用于操作此类结构的程序的组合验证。任何基于SL的自动验证过程的关键要素是蕴涵问题的可判定性。在这项工作中，我们减少了蕴涵问题的一个非平凡的子集SL描述树（和超越）的语言包含树自动机（TA）。我们的减少提供了严格的复杂性界限的问题，并表明在我们的片段的蕴涵是EXPTIME完成。出于实用的目的，我们利用自动机理论的最新进展，如包含检查非确定性TA避免明确的确定性。我们实现了我们的方法，并提出了有前途的初步实验结果。
2014-02-11 cs.LO
Combining Weak Distributive Laws: Application to Up-To Techniques
交替自动机和概率自动机的共代数建模长期以来一直受到阻碍的情况下分配律的幂集单子本身，分别幂集单子的有限分布单子。这可以用弱分配律的框架来解决。我们扩展这个框架的情况下，其中一个单子只是一个函子。我们提供了抽象的组合性结果，广义的确定过程，和系统的健全的技术。一路上，我们将这些结果作为一个激励的例子交替自动机。另一个例子是概率自动机，我们的结果产生的相互模拟的可靠性高达凸包。
2020-10-02 cs.LO
A Survey on Satisfiability Checking for the $μ$-Calculus through Tree Automata
用于模态$μ$演算的模型检验和可满足性的算法通过将公式转换为交替奇偶校验树自动机来开始。这样，模型检验就归结为树自动机的可接受性检验和树自动机的可满足性检验。第一个直接归结为平价博弈的解，但第二个更复杂。我们回顾了交替树自动机的非空性检查，通过减少到解决某种结构的奇偶游戏，所谓的空游戏。由于交替树自动机的空性问题是EXPTIME完全的，这些游戏的大小是输入自动机状态数的指数。我们展示了如何建设的空虚游戏相结合的（固定）结构部分与（历史）确定奇偶校验字自动机。对于具有某些句法结构的树自动机，可以使用更简单的方法来处理词自动机的处理，然后词自动机可以比一般情况下渐近地更小。这些结果有直接的后果，可满足性和有效性检查（各种片段）的模式$μ$演算。
2022-08-23 cs.LO
On Star Expressions and Coalgebraic Completeness Theorems
一个开放的问题所提出的米尔纳要求证明，一定axiomatisation，米尔纳表明是健全的关于双相似性的正则表达式，也是完整的。这个问题的主要困难之一是缺乏一个完整的Kleene定理，因为有自动机，不能指定，直到双相似性，由一个表达式。Grabmayer and Fokkink（2020）证明了那些可以用正则表达式表示而不需要常数1的自动机，并使用这种特征来对Milner关于这个表达式子集的问题给出肯定的回答。本文从泛余代数的角度分析了Grabmayer和Fokkink关于完备性的证明，并由此抽象地说明了他们的证明方法。然后，我们比较这种证明方法的另一种方法，从共代数语言理论的完整性证明。这最终导致了两种抽象的完整性证明方法，我们称之为局部和全局方法，以及一种方法何时可以代替另一种方法的描述。
2022-03-08 cs.FL cs.LO
From LTL to Deterministic Automata: A Safraless Compositional Approach
我们提出了一个新的算法来构造一个确定性拉宾自动机的LTL公式$φ$。该自动机是一个主自动机和一个从自动机数组的乘积，每个从自动机对应于$φ$的每个$G$子公式。$Gψ$的从属自动机负责识别$FGψ$是否成立。与标准的确定过程相反，我们所有自动机的状态都有一个清晰的逻辑结构，这允许应用各种优化。我们的建设包括前LTL片段的算法。实验结果表明，与现有的方法相比，改进的自动机的大小。
2014-09-24 cs.FL cs.LO
Nested Antichains for WS1S
我们提出了一种新的方法来应对交替量化的非初等复杂性的决定WS 1 S公式的主要来源。我们的方法是适用于国家的最先进的基于自动机的WS 1 S决策过程中实施，例如在MONA。标准决策过程处理量词的方式涉及确定，其最坏情况下的指数复杂性，对于公式前缀中的每个量词交替。我们的算法避免了建立确定性自动机-相反，它只构造那些需要（disprove）公式的有效性的状态。它使用一个符号表示的状态，这有一个深深的嵌套结构，源于重复的隐式子集建设，并修剪搜索空间的嵌套包容关系，一个泛化的所谓的反链算法用于处理不确定自动机。我们已经获得了令人鼓舞的实验结果，在某些情况下，超过MONA的几个数量级。
2015-01-15 cs.LO
History-deterministic Timed Automata
本文研究了无限时间字上的历史确定性时间自动机，证明其识别语言类别严格介于确定性与非确定性自动机之间，并证明了其普遍性、包含性和综合问题的可判定性及EXPTIME完全性。
2024-10-09 cs.FL cs.LO
Modular Mix-and-Match Complementation of Büchi Automata (Technical Report)
不确定Büchi自动机（BA）的可补性是自动机理论中的一个重要问题，在形式化验证中有着广泛的应用，如程序的终止性分析、模型检验以及某些逻辑的判定过程等。我们建立在最近的工作的想法BA确定李等。并提出了一个新的模块化算法BA互补。我们的算法允许结合几个BA互补程序在一起，一个程序的一个子集的BA的强连接组件（SCC）。以这种方式，可以利用特定SCC的结构（例如当它们固有地弱或确定性时）并使用更有效的专用算法，而不管整个BA的结构如何。我们给出了一个一般的框架，部分互补程序可以插入，它的实例化与几个算法。一般来说，该框架可以产生具有Emerson-Lei接受条件的补集，该补集通常可以更紧凑。使用该算法，我们能够建立一个指数更好的新的上限$O(4n)$补充最近推出的电梯自动机类。我们实现了该算法的原型，并进行了一系列全面的实验上的一个大的基准测试，表明我们的框架补充以及最先进的，它可以作为未来的高效BA互补和包含检查算法的基础。
2023-01-05 cs.FL cs.LO
