An analogue to Dixon's theorem for automaton groups
狄克逊的著名定理指出，由有限集的两个随机置换生成的群一般是整个对称群或交错群。在随机生成有限群的上下文中，这意味着通过绘制随机排列并查看生成的群来希望均匀分布-甚至非平凡分布-是无望的。Mealy自动机是生成群的有力工具，包括所有的有限群和许多有趣的无限群，由此产生了通过抽取随机Mealy自动机生成随机有限群的思想。本文证明了，对于一类只生成有限群的Mealy自动机，由于所生成的群一般是交错群的直积与由置换元组生成的群之间的半直积，所以其分布远不是均匀的.
2016-10-11 cs.DM cs.FL math.GR
On the Finiteness Problem for Automaton (Semi)groups
本文讨论了Grigorchuk，Nekrashevich和Sushchanskii强调的一个决策问题，即自动机（半）群的有限性问题。对于半群，我们给出了有限性的一个有效的充分但非必要条件，对于群，我们给出了一个有效的必要但非充分条件。通过对所有具有小状态集和小字母表的Mealy自动机的测试，证明了新准则的有效性。最后，对于群体，我们提供了一个不直接导致决策过程的充分必要条件。
2011-05-24 cs.FL math.GR
Generic properties in some classes of automaton groups
我们证明，各种重要类的Mealy自动机，几乎所有的生成群有一个元素的无限阶。在某些情况下，它还意味着其他结果，如指数增长。
2019-03-27 cs.DM cs.FL math.GR
The finiteness problem for automaton semigroups is undecidable
自动机群和自动机半群的有限性问题已得到广泛的研究，并有几个部分正结果。然而，我们证明，在最一般的情况下，问题是不可判定的。我们研究了自动机半群的情形。给定一个NW-确定的Wang瓦片集，构造一个Mealy自动机，使得该平面上存在一个有效的Wang瓦片当且仅当Mealy自动机生成一个有限半群.该构造类似于卡里的构造，用于证明细胞自动机的幂零性问题是不可解的。Kari还证明了对于NW-确定的Wang tile集，平面的平铺是不可判定的。自动机半群的有限性问题是不可判定的。
2014-03-20 cs.DM cs.FL
Automatic semigroups vs automaton semigroups
我们发展了一种有效而自然的方法来解释任何允许一种特殊的贪婪范式语言的半群作为一个自动机半群，即由Mealy自动机生成的半群编码这种贪婪范式语言在单侧乘法下的行为。（自动）半群：有限幺半群、自由半群、自由交换幺半群、迹或可除幺半群、辫幺半群或Artin-Tits幺半群或Krammer幺半群或Garside幺半群、Baumslag-Solitar半群等。像plasticmonoid或Chinesemonoid一样，本文还研究了一些既不是左可消也不是右可消的自动半群，以及双圈幺半群的一些剩余有限变式。它提供了从一类自动半群到一类自动机半群的第一个已知的联系。值得注意的是，在所有这些情况下，“是一个自动半群”和“是一个自动机半群”成为一个非常自动机理论意义上的对偶性质。二次重写系统和相关的平铺出现作为我们的建设的基石。
2018-12-05 cs.FL math.GR
Active Learning of Symbolic Mealy Automata
本文提出主动学习算法 $Λ^*_M$，通过引入本质输入字符概念，解决符号化 Mealy 自动机在无限输入字母表与多输出字符结合下的学习难题，并证明其终止性、给出查询复杂度上下界及实验验证。
2025-09-18 cs.FL
A characterization of those automata that structurally generate finite groups
Antonenko和Russyev独立地证明了任何没有带出口的循环的Mealy自动机-也就是说，底层有向图中的每个循环都是汇组件-生成有限（半）群，而不管生产函数的选择。Antonenko证明了这在不可逆情形下构成了一个刻画，并要求可逆情形，本文证明了这一点。
2013-10-26 cs.FL math.GR
Groups and Semigroups Defined by Colorings of Synchronizing Automata
在本文中，我们结合的代数性质的Mealy机生成自相似群和相应的确定性有限自动机（DFA）的组合性质。特别是，我们涉及有界自动机的同步自动机和特征的有限自动机组在相应的DFA的幂零性。此外，我们给出了自动机群中存在自由半群的一个可判定的充分条件。给出了一系列的例子和应用，特别是给出了一种将De Bruijn自动机着色为Mealy自动机的方法，该Mealy自动机的伴随半群是自由的，并给出了一些与伴随群有关的结构结果.
2013-10-19 cs.FL math.CO math.GR
Knapsack problem for automaton groups
背包问题是一个经典的优化问题，最近已扩展到组的设置。它的研究表明是有趣的，因为它提供了许多不同的行为，这取决于所考虑的群体类别。在本文中，我们处理的群体所产生的Mealy自动机，一类是经常被用来研究组理论programmures-and证明背包问题是不可判定的这一类。在第二次，我们构造一个图，如果有限，提供了一个背包问题的解决方案。我们推断，背包问题是可判定的所谓的有界自动机组，一类的顺序和共轭问题已经知道是可判定的。
2016-12-14 cs.DM cs.FL math.GR
Emptiness of zero automata is decidable
零自动机是奇偶自动机在无限树上的概率扩展。mso的一个概率变体tmso + zero的可满足性归结为零自动机的空性问题。我们引入一个变种的零自动机称为非零自动机。我们证明了，对于每一个零自动机有一个等价的非零自动机的平方大小和空问题的非零自动机是可判定的，在NP和在coNP。这些结果意味着tmso +零具有可判定的可满足性。
2017-03-28 cs.FL cs.GT
A new hierarchy for automaton semigroups
我们定义了一个新的严格的和可计算的自动机半群族的层次，它反映了各种渐近行为的状态活动的增长。这种层次结构扩展了Sidki给出的自动机群，也给了后者新的见解。它的指数部分与某些相关自动机的熵概念相吻合。证明了当状态-活动有界时，序问题是可判定的。顺序问题在这个层次结构的下一个层次仍然是开放的，也就是说，当状态-活动是线性的。Gillibert表明，这是不可决定的，在整个家庭。前者的结果实施，并将在GAP包FR开发的第一作者。
2018-05-13 cs.FL math.GR
Algorithmic decidability of Engel's property for automaton groups
我们认为可判定性问题与恩格尔的身份（$[\cdots[[x,y],y],\dots,y]=1$足够长的换向器序列）在由自动机产生的群体。我们给出了一个部分算法，决定，给定$x,y$，恩格尔恒等式是否满足。重要的是，它成功地证明了Grigorchuk的$2$ -群不是Engel。接下来，我们考虑识别恩格尔元素，即元素$y$，使得映射$x\mapsto[x,y]$吸引到$\{1\}$的问题。虽然这个问题似乎棘手的一般情况下，我们证明，它是可判定的Grigorchuk的组：恩格尔元素正是那些为了最多$2$。我们的计算是使用计算机代数系统GAP中的FR包实现的。
2015-12-06 cs.FL math.GR
Observation and Distinction. Representing Information in Infinite Games
我们比较了两种方法建模不完美的信息在无限游戏中使用有限状态自动机。第一种更标准的方法将信息视为由顺序Mealy机驱动的观察过程的结果。相比之下，第二种方法的特点是由同步两带自动机描述的不可分割关系。事实证明，不可否认性关系模型比基于观察的模型更有表达力。我们提出了一个表征的不可分割的关系，承认作为一个有限状态观测函数的表示。我们表明，特征是可判定的，并给出了一个程序来构建一个相应的Mealy机，只要一个存在。
2020-01-30 cs.FL cs.GT
Deciding the value 1 problem for probabilistic leaktight automata
值1问题是一个概率自动机在有限词上的决策问题：给定一个概率自动机，是否有概率任意接近1的词被接受？这个问题最近被证明是不可判定的;为了克服这个问题，提出了几类不同性质的概率自动机，其中值1问题已被证明是可判定的。在本文中，我们介绍了另一类概率自动机，称为leaktight自动机，它严格包含所有类的概率自动机的值1的问题是已知的可判定的。我们证明，对于密封自动机，值1的问题是可判定的（事实上，PSPACE完全）通过构建一个饱和算法的基础上计算的幺半群抽象的自动机的行为。我们依靠西蒙开发的代数技术来证明这种抽象是完整的。此外，我们适应这种饱和算法来决定是否一个自动机是密封的。最后，我们展示了一个减少，允许我们的可判定性结果从有限字到无限的，这意味着值1的问题的概率leaktight奇偶自动机是可判定的。
2015-06-22 cs.FL
Deciding Top-Down Determinism of Regular Tree Languages
众所周知，对于规则树语言，它是否能被确定性自顶向下树自动机（DTA）识别是可判定的。然而，该问题的计算复杂性还没有被研究过。我们表明，对于一个给定的确定性自下而上的树自动机，它可以决定在二次时间是否可以识别其语言的DTA。由于有有限树语言，不能被识别的DTA，我们也考虑有限工会的\DTAs，并表明，也在这里，确定性自下而上的树自动机内的可定义性是可判定的二次时间。
2021-07-07 cs.FL
Determinisability of one-clock timed automata
时间自动机的确定性成员问题是关于被非确定性时间自动机识别的时间语言是否能被确定性时间自动机识别。我们表明，当输入自动机是一个单时钟的非确定性时间自动机没有转换和确定性时间自动机的时钟数是固定的，这个问题是可判定的。我们表明，在所有其他情况下的问题是不可判定的，即，当1）输入非确定性定时自动机具有两个或更多个时钟，或2）它使用双跳变，或3）输出确定性自动机的时钟数量不固定时。
2020-07-18 cs.FL
Orbit Expandability of Automaton Semigroups and Groups
我们在自动机半群和群的上下文中引入可扩展性的概念：一个词是k-可扩展的，如果一个人可以附加一个后缀到它，使得在自动机的作用下轨道的大小增加至少k。这个定义是由ω-词是否允许无限轨道的问题所激发的：对于这样的词，每个前缀都是可扩展的。在本文中，我们证明了，在输入一个词u，一个自动机T和一个数k，它是可判定的，以检查是否u是k-可扩展的关于T的行动。事实上，这可以在指数非确定性空间中完成。从这个非确定性算法，我们得到了一个潜在的轨道增加后缀x的长度上的界限。此外，我们调查的情况下，如果自动机是可逆的，并产生一个组。在这种情况下，我们给出了一个代数特征的扩展性的字的基础上，其移位稳定。我们还给出了一个更有效的算法来决定一个词的可扩展性的情况下，自动机组，这使得我们能够提高上界的最大轨道增加后缀长度。然后，我们研究了可逆（和完全）自动机的情况，并得到每个字是可扩展的关于这些自动机。最后，我们给出了一个轨道增加后缀长度的下界例子。
2020-01-15 cs.FL math.GR
Determinisability of register and timed automata
该研究解决了寄存器自动机与时间自动机的确定性成员问题，绘制了完整可判定性图景，并证明在单寄存器/单时钟且输出资源数固定时可判定，其余情况不可判定。
2022-05-09 cs.FL
The Containment Problem for Unambiguous Register Automata
我们调查的复杂性的遏制问题“$L(A)\subseteq L(B)$举行？“，其中$B$是明确的寄存器自动机，而$A$是任意寄存器自动机。我们证明了这个问题是可判定的，并给出了上界的计算复杂性在一般情况下，当$B$被限制为有一个固定数量的寄存器。
2019-01-20 cs.FL
Two-State Max-Plus Comparison Is Decidable
Google（谷歌）
该研究解决了状态数2到552中两状态的极大加自动机比较问题，证明任意有限极大加自动机与至多两状态的极大加自动机的比较可判定，进而得到两状态极大加的比较、等价性和正性均可判定的结论。
2026-09-04 cs.DS 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
Deciding the Value 1 Problem of Probabilistic Leaktight Automata
值1问题是有限词上的概率自动机的一个判定问题：给定一个概率自动机A，是否存在A以任意接近1的概率接受的词？这个问题最近被证明是不可判定的。我们锐化这一结果，表明不可判定性的结果，即使概率自动机只有一个概率的过渡。我们的主要贡献是引入一类新的概率自动机，称为leaktight自动机，其中值1的问题是可判定的（和PSPACE完全）。我们构造了一个算法的基础上计算的幺半群抽象的行为的自动机，并依靠代数技术开发的西蒙的正确性证明。类的leaktight自动机是可判定的PSPACE，包括所有子类的概率自动机的值1的问题是已知的可判定的（特别是确定性自动机），并关闭下两个自然的组合算子。
2012-01-26 cs.FL cs.GT
New Techniques for Universality in Unambiguous Register Automata
寄存器自动机是有限自动机，配备了一组有限的寄存器，范围覆盖某些关系结构（如$(\mathbb N;=)$或$(\mathbb Q;<)$）的域。寄存器自动机处理域上的字，并且沿着自动机的运行，寄存器可以存储来自输入字的数据以供稍后比较。众所周知，普遍性问题，即，决定给定寄存器自动机是否接受域上的所有词的问题是不可判定的。最近，我们证明了在2-ExpSpace中，如果所研究的寄存器自动机是在$(\mathbb N;=)$上的并且是无歧义的，即，每个输入单词最多有一次接受运行; Barloy和Clemente不久后将该结果改进为2-ExpTime。在本文中，我们更进一步，证明了问题是在ExpSpace中，并在PSpace中，如果寄存器的数量是固定的。我们的证明是基于新的技术，另外使我们能够表明，问题是在PSpace的单寄存器自动机超过$(\mathbb Q;<)$。作为第三个技术贡献，我们证明了这个问题是可判定的（在ExpSpace）的一个更有表现力的模型，明确的寄存器自动机，其中的寄存器可以采取值nondeterministically，如果定义在$(\mathbb N;=)$和只有一个寄存器使用。
2021-02-16 cs.FL
Decision Problems for Restricted Variants of Two-Dimensional Automata
二维的【形】有限自动机具有只读输入头，其在由输入字母表的符号标记的有限单元阵列上沿四个方向移动。一个三向二维的【形】自动机被禁止向上移动，而一个双向二维的【形】自动机只能向下移动。我们证明了一元三路非确定二维的【形】自动机的语言空性问题是NP-完全的，而一般字母表双向非确定二维的【形】自动机的语言空性问题是P中的。我们证明了双向确定二维的【形】自动机的语言等价性问题是可判定的，而双向非确定二维的【形】自动机的等价性和普适性问题都是不可判定的.确定性的情况下是第一个已知的积极的可判定性结果的等价问题的二维的【形】自动机在一般字母表。我们证明了存在一个具有非正则列投影的一元三路确定二维的【形】自动机，并且我们证明了一元三路非确定二维的【形】自动机的行投影总是正则的。
2019-04-24 cs.FL
Computing the linear hull: Deciding Deterministic? and Unambiguous? for weighted automata over fields
University of Waterloo（滑铁卢大学）；University of Graz（格拉茨大学）
本文研究了域上加权自动机的线性包络计算，证明了确定性和无歧义性的判定问题可解，并提供了相应的计算方法。
2023-06-06 cs.FL math.CO
Leafy Automata for Higher-Order Concurrency
有限理想化并发算法（Finitary Idealized Concurrent Algol，FICA）是一种结合了函数式、命令式和并发计算的原型程序设计语言。存在一个完全抽象的FICA博弈模型，原则上可以用来证明FICA程序的等价性和安全性。不幸的是，这些问题对于整个语言来说都是不可判定的，并且只知道非常基本的可判定子语言。我们提出叶自动机作为一个专门的自动机理论的形式主义表示游戏语义的FICA。自动机使用具有树结构无限字母表。我们表明，游戏语义的任何FICA长期可以表示的痕迹，一个树叶自动机。相反，任何叶子自动机的迹都可以用FICA项表示。由于与FICA的密切匹配，我们认为叶自动机作为一个很有前途的起点，寻找可判定的语言子类，更一般地说，提供了一个新的视角高阶并发计算模型。此外，我们确定了一个片段的FICA，是适合验证翻译成一个特定的类叶自动机。使用后一类的局部性，其中级别之间的通信是有限的，每隔一级有界的，我们表明，他们的空虚问题是可判定的减少到Petri网的可达性。
2021-01-21 cs.FL cs.PL
On the decidability of $k$-Block determinism
Brüggemann-Klein和Wood定义了一个无二义性的正则语言，它可以被确定的Glushkov自动机识别。他们给出了一个程序上执行的最小DFA，BW测试，以确定是否一个语言是一个明确的。块决定论是一元无歧义的扩展，它把非虚词看作符号，把无前缀看作决定论。一个块自动机是紧凑的，如果它没有两个等价的状态（相同的右语言）。我们证明了一种语言是$k$ -块确定的，如果它被通过BW-测试的确定性$k$ -块自动机识别。在本文中，我们证明了任何$k$块确定性语言是由一个紧凑的确定性$k$块自动机通过BW测试。我们还给出了一个程序，枚举，对于一个给定的语言，有限集紧凑的确定性$k$块自动机。它为我们提供了一个可判定的过程来测试一个语言是否是$k$ -块确定的。
2017-05-30 cs.FL
Determinisation and Unambiguisation of Polynomially-Ambiguous Rational Weighted Automata
本文研究有理数域上加权自动机的确定化与去歧义化问题，证明对多项式模糊加权自动机，这两个问题均属于 PSPACE，填补了 Bell 和 Smertnig 可判定性结果中复杂度界限的空白。
2025-05-27 cs.FL cs.LO
On the Distance between Timed Automata
包含时间自动机$A$接受的语言的问题（例如，实现）以$B$接受的语言（例如，规范）在非确定性时间自动机类中通常是不可判定的。为了解决这个令人不安的问题，我们展示了如何有效地构建确定性的时间自动机$A_d$和$B_d$的离散化（数字化）的非确定性的时间自动机$A$和$B$和不同的原始自动机在最多$\frac{1}{6}$的时间单位上的每个事件的发生。离散时间自动机中的语言包含是可判定的，当我们考虑$\overline{\mathfrak{L}(B)}$而不是$\mathfrak{L}(B)$时，它也是可判定的，$\overline{\mathfrak{L}(B)}$是${\mathfrak{L}(B)}$在欧几里德拓扑中的闭包：如果$\mathfrak{L}(A_d) \nsubseteq \mathfrak{L}(B_d)$，则$\mathfrak{L}(A) \nsubseteq \mathfrak{L}(B)$，如果$\mathfrak{L}(A_d) \subseteq \mathfrak{L}(B_d)$，则$\mathfrak{L}(A) \subseteq \overline{\mathfrak{L}(B)}$。此外，如果$\mathfrak{L}(A_d) \nsubseteq \mathfrak{L}(B_d)$，我们想知道$\mathfrak{L}(A_d)$离被…
2019-09-23 cs.FL
A note on decidability of cellularity
一个正则语言L称为细胞语言，如果存在一个1维细胞自动机CA，使得L是由与CA相关联的有限块组成的语言。它表明，一个正则语言的细胞是可判定的使用细胞语言的一个新的特征制定的Freiling，Goldstein和Moews和隐含的深刻结果Boyle在符号动力学。
2010-04-12 cs.FL
Büchi automata recognizing sets of reals definable in first-order logic with addition and order
这项工作考虑弱确定性Büchi自动机阅读编码的非负实数在一个固定的基地。实数自动机是一种自动机，它可以识别一组实数的所有元素的编码。它解释了如何决定在线性时间是否一组reals承认一个给定的最小弱确定性RNA是${FO}[\mathbb R;+,<,1]$ -可定义的。此外，它解释了如何计算在准二次（分别，准线性）时间存在（分别，存在普遍）${FO}[\mathbb R;+,<,1]$ -公式，定义了一套真正的自动机。它还表明，由Muchnik和Honkala的自动机在向量的自然数的技术也适用于向量的实数。这意味着一些问题，如判定实数元组集$R\subseteq\mathbb R^{d}$是否是$(\mathbb R^{d},+)$的子半群或是否是${FO}[\mathbb R;+,<,1]$ -可定义的，是可判定的.
2016-11-11 cs.FL
Formalized Run-Time Analysis of Active Learning -- Coalgebraically in Agda
Friedrich-Alexander-Universität Erlangen-Nürnberg（弗里德里希·亚历山大·埃尔朗根-纽伦堡大学）
本文在Agda中利用合子论方法，通过将学习算法视为广义自动机，形式化证明了主动学习算法的运行时间复杂度为O(log n)。
2026-07-21 cs.FL
A decidability result for the halting problem of cellular automata in the pentagrid
本文研究了确定性细胞自动机在五角网格上的停机问题。我们证明了这个问题是可判定的，当元胞自动机从一个有限的配置开始其计算时，它最多有两个状态，其中之一是一个静态的。
2018-12-10 cs.FL nlin.CG
Phase Space Invertible Asynchronous Cellular Automata
虽然对于同步确定性细胞自动机有一个公认的可逆性定义，但异步细胞自动机的情况不太清楚。我们首先讨论了几种可能性，然后研究我们称之为相空间可逆异步细胞自动机更详细。我们将证明，对于每一个图灵机，都有这样一个元胞自动机来模拟它，并且即使在更高的维度上，异步元胞自动机是否具有这种性质也是可判定的。
2012-08-14 cs.CC cs.DM cs.FL
Sequentializing cellular automata
我们研究了在不引入任何中间状态的情况下，仅在磁带上执行可逆置换的元胞自动机的序列化问题。我们给出了细胞自动机的一个可判定的特征，它可以被写为一个从左到右的双射规则在一个无限带上的单次从左到右的扫描。
2018-04-06 cs.FL math.DS
Decidability of Timed Communicating Automata
研究了时间通信网络的可达性问题。每个进程都是一个时间自动机，通过在无界FIFO通道上交换消息与其他进程进行通信。消息携带时钟，该时钟在发送和接收时以适当的定时约束进行检查。每个自动机只能访问它的本地时钟和发送/接收消息的消息时钟集。时间是密集的，所有的时钟都以相同的速度进化。我们的主要贡献是一个完整的特征的可判定和不可判定的通信拓扑结构概括和统一以前的工作。从技术的角度来看，我们使用量词消去和减少计数器自动机与寄存器。
2018-04-20 cs.DC cs.FL cs.LO
Relating timed and register automata
时间自动机和寄存器自动机分别是时间字和数据字上的著名计算模型。前者具有允许测试两个事件之间的时间流逝的时钟，而后者包括可以存储数据值以供稍后比较的寄存器。虽然这两个模型在外观上表现不同，但两个模型的几个决策问题具有相同的（非）可判定性和复杂性结果。作为一个突出的例子，空性是可判定的交替自动机与一个时钟或寄存器，都具有非原始递归复杂性。这不是偶然的。这项工作证实了这两个模型之间确实存在紧密的关系。我们表明，运行的时间自动机可以模拟的寄存器自动机，反之，运行的寄存器自动机可以模拟的时间自动机。我们的研究结果允许在这两种模型之间来回转移复杂性和可判定性结果。我们证明这些减少的有用性，通过获得新的结果注册自动机。
2010-11-30 cs.FL cs.LO
Communicating Timed Processes with Perfect Timed Channels
我们引入了通信时间自动机（CTA）的模型，扩展了经典的有限状态进程通过FIFO完美通道和时间自动机进行通信的模型，在这个意义上，有限状态进程被时间自动机所取代，完美通道内的消息配备有代表其年龄的时钟。除了标准操作（重置时钟，检查时钟的保护），每个自动机可以（1）将消息附加到具有初始年龄的通道的尾部，或者（2）如果其年龄满足一组给定的约束，则在通道的头部接收消息。在本文中，我们表明，可达性问题是不可判定的，即使在两个时间自动机连接一个单向定时通道的情况下，如果允许全球时钟（这两个自动机可以检查和操纵）。我们证明了这种不可判定性仍然成立，即使CTA由三个定时自动机和两个单向定时通道（没有任何全局时钟）。然而，可达性问题变得可判定（在$\mathsf{EXPTIME}$）的情况下，两个自动机链接一个单向定时通道，没有全局时钟。最后，我们考虑有界上下文的情况下，在每个上下文中，只有一个定时自动机被允许从一个通道接收消息，同时能够发送消息到所有其他定时通道。在这种情况下，我们证明了可达性问题是可判定的。
2018-03-18 cs.FL
Variations of Checking Stack Automata: Obtaining Unexpected Decidability Properties
我们引入了一个单向语言接受者模型（检查栈自动机的一个变体），并证明了以下可判定性性质：（1）确定性版本具有可判定的成员问题，但具有不可判定的空性问题。(2)非确定性版本有一个不可判定的成员问题和空性问题。有许多接受设备的模型，对于这些问题，确定性和非确定性版本之间没有区别，同样适用于空性问题。据我们所知，我们上面介绍的模型是第一个表现出性质（1）和（2）的单向模型。我们定义了另一个单向接受器族，其中非确定性版本具有不可判定的空问题，但确定性版本具有可判定的空问题。我们也不知道在文献中有其他模型具有这种性质。我们还研究了检查堆栈自动机的其他变体的可判定性特性（例如，允许多个堆栈、双向输入等）。令人惊讶的是，双向确定性机器与多个检查堆栈和多个反向有界计数器被证明有一个可判定的成员资格问题，一个非常一般的模型与此属性。
2019-03-07 cs.FL
Techniques for Showing the Decidability of the Boundedness Problem of Language Acceptors
本文针对多数自动机/文法模型有界性问题可判定性未知的背景，提出多带自动机刻画、存储语言两种新技术，归约证明更大类单向非确定自动机和文法模型的有界性可判定。
2024-05-17 cs.FL
Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures
提出$ω$MSO$\Join$BAPA逻辑，通过Parikh-Muller树自动机证明其在树可解释结构上的可满足性可判定，并推广至带高级计数的双变量逻辑与$μ$-演算。
2023-11-23 cs.FL cs.LO
Set Automata and Limits of Decidability of Two-Variable Logic on Data Words
Tata Institute of Fundamental Research（塔塔基础研究所）；Indian Institute of Technology Goa（印度理工学院果阿分校）
研究扩展数据词双变量逻辑以包含guarded regular二元谓词，定义了idempotent monoids的决定性条件，并引入set automata形式化，证明其与ordered quasi-normal set automata的等价性。
2026-05-09 cs.FL cs.LO
Register Automata with Extrema Constraints, and an Application to Two-Variable Logic
本文提出带极值约束的寄存器自动机模型，证明其空性问题可判定，并应用于二变量逻辑，在树序和线性序存在时证明其可数可满足性及可满足性问题可判定。
2022-03-21 cs.FL cs.LO
Representing One Letter Weighted Automata Over the Tropical Semiring
Technion（以色列理工学院）；Université Marie et Louis Pasteur, CNRS, institut FEMTO-ST（玛丽与路易·巴斯德大学，法国国家科学研究中心，FEMTO-ST研究所）；University of Warsaw（华沙大学）；University of Liverpool（利物浦大学）；Max Planck Institute for Software Systems (MPI-SWS)（马克斯·普朗克软件系统研究所）
研究热带半环上单字母加权自动机的确定化与寄存器最小化问题，通过推广Chrobak范式实现多项式时间转换，证明这些问题是coNP完全的且参数化后非FPT。
2026-08-31 cs.FL
Decidability of minimization of fuzzy automata
状态最小化是自动机理论中的一个基本问题。该问题在模糊自动机的研究中也具有重要意义。然而，大多数文献只考虑模糊自动机的状态约简，而模糊自动机的状态最小化问题几乎没有涉及。因此，在本文中，我们专注于后一个问题。形式上，模糊自动机极小化问题的判定形式如下：\begin{itemize} \item Given a fuzzy automaton $\mathcal{A}$ and a natural number $k$, that is, a pair $\langle \mathcal{A}, k\rangle$, is there a $k$-state fuzzy automaton equivalent to $\mathcal{A}$? \end{itemize}我们首次证明了全序格上模糊自动机的上述问题是可判定的。为此，我们首先给出了模糊多项式方程组的概念，然后提出了一个程序来解决这些系统。然后，我们将模糊多项式方程组的可解性应用于上述极小化问题，得到了可判定性。最后，我们指出，上述问题至少是PSAPCE-完全一样难。
2013-05-18 cs.FL
Jump Complexity of Deterministic Finite Automata with Translucent Letters
本文研究具有透字母的确定性有限自动机的跳跃复杂度，证明其复杂度要么常数有界要么线性，给出判定算法并证明相关等价性问题可判定，同时部分解决了正则性判定问题。
2025-06-23 cs.FL
From Two-Way to One-Way Finite State Transducers
任何双向有限状态自动机都等价于某个单向有限状态自动机。这个著名的结果，由Rabin和Scott以及Shepherdson独立证明，指出双向有限状态自动机（甚至是非确定性的）表征了正则语言的类。我们也知道这个结果并不适用于有限弦转换：（确定性的）双向有限状态转换器严格地扩展了（功能性的）单向转换器的表达能力。特别是确定性的双向传感器捕捉正是类的有限字符串的MSO转导。在本文中，我们解决以下定义性问题：给定一个功能定义的双向有限状态转换器，它是可定义的单向有限状态转换器？通过扩展拉宾和斯科特的证明转导，我们表明，这个问题是可判定的。我们的程序建立一个单向换能器，这是等效的双向换能器，只要一个存在。
2013-04-26 cs.FL cs.LO
On von Neumann regularity of cellular automata
我们证明了有限型一维双边混合子移位上的元胞自动机是元胞自动机半群中的vonNeumann正则元当且仅当它在sofic移位和块映射范畴中分裂到它的像上。从作者和Törmä以前的联合工作可以看出，冯·诺依曼正则性是一个可判定的条件，我们对所有初等CA都判定它，从而获得弱广义逆的最佳半径。非正则性的两个充分条件是有一个适当的sofic图像或图像中的一个点没有相同周期的原像。我们发现，非正规ECA 9和28不能证明非正规使用这些方法。我们还表明，一个随机的细胞自动机是不规则的高概率。
2022-09-27 cs.FL math.DS math.RA
Von Neumann regularity, split epicness and elementary cellular automata
证明了有限型混合子移位上的元胞自动机是元胞自动机半群中的VonNeumann正则元当且仅当它在sofic移位和块映射范畴中分裂到它的像上.它来自于[S]。Törmä，2015]冯·诺依曼正则性是可判定的条件，我们对所有初等CA都判定它。
2018-10-10 cs.FL math.DS nlin.CG
A Divide and Conquer Algorithm for Deciding Group Cellular Automata Dynamics
本文提出一种分治算法，将群元胞自动机分解为更简单的子自动机以判定其动力学性质，并证明单射性、满射性和敏感性可判定，同时得出非阿贝尔群上不存在强传递和正扩张性质的结论。
2025-07-13 cs.DM cs.FL
A Nivat Theorem for Weighted Alternating Automata over Commutative Semirings
本文连接了 WAFA、WFTA 和 PA 三类自动机，通过运行语义中的树使用证明交换半环上 WAFA 行为的 Nivat 刻画，揭示了其与 PA 的反转等价性，并证明了有理数权重下 ZERONESS 问题的可判定性。
2023-12-19 cs.FL cs.LO
Effective Projections on Group Shifts to Decide Properties of Group Cellular Automata
许多关于元胞自动机的决策问题在代数元胞自动机的情况下是可判定的，也就是说，当状态集具有代数结构并且自动机充当态射时。研究最多的例子包括有限域、有限交换环和有限交换群。在本文中，我们提供的方法来推广这些结果更广泛的情况下，组细胞自动机，即状态集是一个有限的（可能是非交换的）有限组的情况下。位形空间甚至不一定是全移位，而是一个子移位--称为群移位--它是Z^d上全移位的一个子群，对于任意维数d。特别地，我们证明了群元胞自动机的内射性、满射性、等度连续性、敏感性和幂零性是可判定的，非传递性是半可判定的。内射性总是蕴涵满射性，并且联合周期点在极限集中是稠密的。伊甸园定理的摩尔方向对所有群细胞自动机都成立，而Myhill方向在某些情况下失败。证明是基于有效的投影操作组移位，特别是适用于组元胞自动机的有效的空间-时间图的集合。这使得人们能够有效地构造群元胞自动机的迹和极限集。这项工作的初步版本在2020年计算机科学数学基础会议上发表。
2023-01-26 cs.DM cs.FL
Automata on $S$-adic words
本文研究 $S$-adic 无限字的自动机接受问题，通过构造一个自动机来判定给定替换序列是否引导出被给定 Büchi 自动机接受的字，从而回答哪些 $S$-adic 字被接受。
2025-06-20 cs.FL cs.LO
Reversible Weighted Automata over Finite Rings and Monoids with Commuting Idempotents
Comenius University in Bratislava（布拉迪斯拉发康斯坦丁神学家大学）
本文研究了有限环和独异点上的可逆加权自动机，揭示了其与可交换幂等元有理语言的关系，并证明了相关问题的可判定性。
2026-01-14 cs.FL
