无限词上的概率自动机：表达性、效率和可判定性

五网格中元胞自动机停机问题的一个可判定性结果

A decidability result for the halting problem of cellular automata in the pentagrid

本文研究了确定性细胞自动机在五角网格上的停机问题。我们证明了这个问题是可判定的，当元胞自动机从一个有限的配置开始其计算时，它最多有两个状态，其中之一是一个静态的。

再论有限多带自动机的等价问题

Revisiting the Equivalence Problem for Finite Multitape Automata

确定性多带自动机（或转换器）的判定等价性是一个长期存在的开放问题，直到Harju和Karhumäki在20世纪90年代初解决。他们的可判定性证明产生了一个co_NP上界，但显然对问题的复杂性知之甚少。在本文中，我们给出了另一种证明的可判定性，它遵循的基本策略的Harju和Karhumaki，但取代他们使用群论的结果矩阵代数。从我们的证明，我们得到一个简单的随机算法，决定语言等价的确定性多带自动机，更一般地说，多重性等价的非确定性多带自动机。该算法只涉及矩阵求幂，并在多项式时间内运行每个固定数量的磁带。如果两个输入自动机是不等价的，那么算法输出一个它们不同的词。

群元胞自动机的可判定性与扩张性刻画

Decidability and Characterization of Expansivity for Group Cellular Automata

本文刻画了阿贝尔群上群元胞自动机的扩张性，证明了一般群上扩张性的可判定性，并指出扩张类严格包含于拓扑传递单射类。

Decidability, Complexity, and Expressiveness of First-Order Logic Over the Subword Ordering

We consider first-order logic over the subword ordering on finite words, where each word is available as a constant. Our first result is that the $Σ_1$ theory is undecidable (already over two letters). We investigate the decidability border by considering fragments where all but a certain number of variables are alternation bounded, meaning that the variable must always be quantified over languages with a bounded number of letter alternations. We prove that when at most two variables are not alternation bounded, the $Σ_1$ fragment is decidable, and that it becomes undecidable when three variab…

语言接受器有界性问题可判定性的证明技术

Techniques for Showing the Decidability of the Boundedness Problem of Language Acceptors

本文针对多数自动机/文法模型有界性问题可判定性未知的背景，提出多带自动机刻画、存储语言两种新技术，归约证明更大类单向非确定自动机和文法模型的有界性可判定。

数据自动机的可判定扩展

A Decidable Extension of Data Automata

数据词上的数据自动机（Data Automata on Data Words）是Bojaetczyk等人在2006年提出的一种可判定模型。类自动机是最近由Bojaczyk和Lasota提出的，它是数据自动机的一种扩展，它统一了数据字上不同的自动机模型。类自动机的非空性是不可判定的，因为类自动机可以模拟两计数器机器。本文提出了一种具有优先级条件的可判定类自动机模型，它限制了类自动机，但严格扩展了数据自动机。该模型的可判定性是通过与优先级多计数器自动机建立对应关系而获得的。这种对应关系也完成了类自动机的各种类条件和计数器机器的各种模型之间的联系。此外，该模型被应用到扩展的可判定性的结果，在数组访问程序的算法分析的Alberr，Cernandal和Weinstein。

非均匀元胞自动机：类，动力学和可判定性

Non-Uniform Cellular Automata: classes, dynamics, and decidability

将非均匀元胞自动机的动力学行为与经典元胞自动机的动力学行为进行了比较。通过一系列的例子指出了几个区别和相似之处。还建立了满射性和内射性等基本性质的判定性。最后一部分研究了特别适用于非一致元胞自动机的等度连续性的一种强形式。

多带自动机综述

A Survey of Multi-Tape Automata

本文总结了基本的表达性，封闭性和可判定性的各种有限状态自动机类与多个输入磁带。它还包括一个原始算法的交叉单向非确定性有限状态自动机。

无限词上确定下推自动机的判定问题

Decision Problems for Deterministic Pushdown Automata on Infinite Words

本文调查了DPDA在无限词上的一些可判定性结果（Omega-DPDA）。我们总结了最近的一些结果的可判定性的正则性和等价性问题的类弱omega-DPDA。此外，我们提出了一些新的结果的奇偶指数问题的omega-DPDA。对于奇偶校验条件的规范，omega-DPDA的状态被分配优先级（自然数），并且如果在运行期间无限频繁出现的最高优先级是偶数，则运行是接受的。基本的简化问题是，是否可以确定接受给定Omega-DPDA语言所需的最小优先级数量。我们提供了一些决定性的结果，这个问题的变化，某些类别的欧米茄-DPDA。

Parikh自动机及其相关模型的表达性

On the expressiveness of Parikh automata and related models

Parikh有限词自动机（PA）是Klaedtke和Ruess在2003年提出并研究的。PA的自然变体产生于将PA等效地视为自动机，该自动机保持其转换的计数并半线性地约束其数量。在这里，我们采用这种观点，并定义仿射PA（APA），它通过每个转换在PA寄存器上引起仿射变换来扩展PA，以及字母上的PA（LPA），它通过迫使同一字母上的任何两个转换同等地影响寄存器来限制PA。然后，我们报告的表现力，封闭性和可判定性等PA的变种。我们注意到，确定性PA严格弱于确定性反向有界计数器机器。我们开发泵式引理，并确定一个明确的PA语言没有确定性PA。

概率自动机何时可判定包容性？

When is Containment Decidable for Probabilistic Automata?

概率自动机的空性和包含性问题是经典布尔自动机空性和包含性问题的自然定量推广。众所周知，这两个问题都是不可判定的。在本文中，我们提供了一个更精细的查看这些问题的概率自动机的模糊程度。我们表明，空性问题的间隙版本（这是已知的不可判定的一般）成为可判定的多项式模糊自动机。我们补充这一积极的结果表明，空性问题仍然是不可判定的，即使限制自动机的线性模糊性。然后我们转向无歧义自动机。在这里，我们展示的情况下，一个自动机被假定为是明确的，而另一个是允许的，是不明确的包容性的可判定性。我们对这最后一个结果的证明依赖于实指数化理论的可判定性，麦金太尔和威尔基已经证明了这一点，但受制于沙奈尔猜想。

时间通信自动机的可判定性

Decidability of Timed Communicating Automata

研究了时间通信网络的可达性问题。每个进程都是一个时间自动机，通过在无界FIFO通道上交换消息与其他进程进行通信。消息携带时钟，该时钟在发送和接收时以适当的定时约束进行检查。每个自动机只能访问它的本地时钟和发送/接收消息的消息时钟集。时间是密集的，所有的时钟都以相同的速度进化。我们的主要贡献是一个完整的特征的可判定和不可判定的通信拓扑结构概括和统一以前的工作。从技术的角度来看，我们使用量词消去和减少计数器自动机与寄存器。

数据词上的双变量逻辑与决定性的极限

Set Automata and Limits of Decidability of Two-Variable Logic on Data Words

研究扩展数据词双变量逻辑以包含guarded regular二元谓词，定义了idempotent monoids的决定性条件，并引入set automata形式化，证明其与ordered quasi-normal set automata的等价性。

关于时间自动机中不透明性可判定性的新见解

New Insights into the Decidability of Opacity in Timed Automata

本文研究时间自动机不透明性的可判定性，通过提供充分必要条件识别出新的可判定子类IRTA并给出验证算法，同时证明在入侵者仅能离散观察时间的假设下一般TA的不透明性也可判定，为安全分析奠定理论基础。

用“Hilbert方法”解决传感器等价问题到寄存器自动机问题

Reducing Transducer Equivalence to Register Automata Problems Solved by "Hilbert Method"

在过去的几十年中，代数的经典结果，包括希尔伯特的基本定理，在形式语言中有各种应用，包括Escherichfeucht猜想的证明，HDT0L序列等价的可判定性，以及函数树到串转换器的等价问题的可判定性。在本文中，我们研究了上述代数方法的范围，特别是适用于寄存器自动机的等价问题。我们提供了两个结果，一个阳性，一个阴性。结果表明，无序森林上的MSO变换是等价的。否定的结果来自于尝试将该方法扩展到确定宏树换能器的等效性。我们减少了宏树换能器等价的等价问题，一类寄存器自动机自然相关的我们的方法。然后，我们证明后一个问题是不可判定的。

概率自动机的无限同步字（勘误）

Infinite Synchronizing Words for Probabilistic Automata (Erratum)

在[1]中，我们介绍了概率自动机的弱同步语言。在这篇报告中，我们证明了概率自动机弱同步语言的空性问题是不可判定的。这意味着[1-3]关于弱同步语言空性问题的可判定性结果是不正确的。

关于Word-MIX语言的无穷性和等价性问题的注记

Note on the Infiniteness and Equivalence Problems for Word-MIX Languages

在本文中，我们提供了一个（可判定的）图形结构的表征的无限的$L(w_1, ..., w_k)$，其中$L(w_1, ..., w_k) = \{w \in A^* | |w|_{w_1} = \cdots = |w|_{w_k}\}$是一组的所有字，包含相同数量的子字出现的参数字$w_1, ..., w_k$。我们还提供了这些语言的等价性的可判定的表征。虽然这两个可判定性结果也是从更一般的已知的无模糊约束自动机的可判定性结果中得到的，但本文试图给出可判定性的一个自包含的（不需要关于约束自动机的知识）证明。

随机元胞自动机：相关性、可判定性与模拟

Stochastic Cellular Automata: Correlations, Decidability and Simulations

本文介绍了一种简单的形式化方法，用于统一地、可组合地处理确定性、非确定性和随机性细胞自动机。这种形式主义允许局部概率相关性，这是不存在于通常的定义中的功能。我们表明，这个功能允许严格更多的行为（例如，数量守恒的随机细胞自动机需要这些本地概率相关性）。我们还表明，几个问题，这是看似简单的通常的定义，成为不可判定的，当我们允许当地的概率相关性，即使在一维。有了这种形式主义，我们扩展了确定性细胞自动机之间的内在模拟的概念，非确定性和随机设置。虽然内在的模拟关系在二维和更高的维度上变得不可判定，我们提供了明确的工具来证明或反驳任何两个给定的随机细胞自动机之间存在这样的模拟。这些工具依赖于平等的随机全球地图的表征，被证明是等价的随机源之间的随机耦合的存在。我们应用它们证明了不存在普适的随机元胞自动机。然而，我们提供了随机细胞自动机实现最佳的部分普遍性，以及一个普遍的非确定性细胞自动机。

字母有界输入下概率有限自动机割点隔离的可判定性

Decidability of cutpoint isolation for probabilistic finite automata on letter-bounded inputs

我们展示了一个令人惊讶的结果，断点隔离问题是可判定的概率有限自动机（PFA）的输入单词是从一个字母有界的上下文无关的语言。当$\mathcal{L} \subseteq a_1^*a_2^* \cdots a_\ell^*$对于某个有限的$\ell > 0$，其中每个字母都是不同的时，上下文无关语言$\mathcal{L}$是字母有界的。一个分界点是孤立的，当它不能任意接近。这个问题的可判定性是在显着对比的情况下，为PFA的（严格）空问题，这是不可判定的甚至更严格的限制下，PFA与多项式的歧义，交换矩阵和输入在一个字母有界的语言，以及注入性问题，这是不可判定的PFA在字母有界的语言。我们提供了一个建设性的非确定性算法来解决割点隔离问题，即使当PFA是指数模糊的。我们还表明，该问题至少是NP-难的，并使用我们的决策过程来解决几个相关的问题。

Shuffle投影下的闭语言对

Pairs of Languages Closed under Shuffle Projection

Shuffle投影的动机是验证特殊参数化系统的安全性。基本定义和性质，特别是有关字母同态，提出。迭代洗牌产品和洗牌投影之间的关系。引入了一类特殊的多计数器自动机，用变换表示的自动机的计算来表示洗牌投影。这种重新表述的洗牌投影导致的建设原则对语言关闭洗牌投影。此外，它表明，在一定条件下，这些转换是合理的，这意味着对洗牌投影闭包的可判定性。对于正则语言证明了这些条件的可判定性。最后，在没有附加条件的情况下，证明了一对正则语言在shuffle投影下是否封闭的问题的可判定性。在附录中讨论了两种语言的shuffle投影和shuffle乘积之间的关系。此外，还定义了一种用于S-自动机计算的混洗积。

Equivalence of pushdown automata via first-order grammars

A decidability proof for bisimulation equivalence of first-order grammars is given. It is an alternative proof for a result by Sénizergues (1998, 2005) that subsumes his affirmative solution of the famous decidability question for deterministic pushdown automata. The presented proof is conceptually simpler, and a particular novelty is that it is not given as two semidecision procedures but it provides an explicit algorithm that might be amenable to a complexity analysis.

时间自动机：验证和表达

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的语言既不是封闭的互补下，也没有交叉。

森林逻辑的代数刻画

Algebraic Characterization of Forest Logics

在本文中，我们定义了未来时间的分支时间逻辑评估森林，即有序的元组，但排名，有限的树。我们将时间逻辑的丰富类FL[ $\mathcal{L}$ ]与（常规）模态的每个集合L相关联。然后，我们定义了一个代数产品的操作，我们称之为摩尔产品，这对森林自动机，代数设备识别森林语言。我们展示了有限森林自动机的伪变种之间的格同构，封闭的摩尔产品，和语言类的形式FL[ $\mathcal{L}$ ]。我们证明了有用的代数方法，通过显示一个特定的伪品种的有限森林自动机的成员资格问题的可判定性，这意味着可判定性的FL[EF]片段的逻辑CTL的可定义性问题。然后，使用相同的方法，我们还制定了一个猜想，关于FL[AF]片段的可判定特性，目前具有未知的可判定性状态（也在设置的排名树）。

单计数器网弱模拟的可判定性

Decidability of Weak Simulation on One-counter Nets

单计数器网（OCN）是具有唯一无界库所的Petri网。它们等价于只有弱零测试的单计数器自动机的子类。我们证明了OCN的弱模拟预序是可判定的，并且弱模拟逼近在水平ω上不收敛，而仅在ω ^2上收敛。相比之下，其他语义关系如弱互模拟对于OCN是不可判定的，弱（和强）迹包含也是如此。

多字母量子有限自动机等价性的判定

Decidability of the Equivalence of Multi-Letter Quantum Finite Automata

多字母{ \it量子有限自动机}（QFA）是经典{ \it单向多头有限自动机}的量子变体（J. Hromkovietum，Acta Informatica 19（1983）377-384），并且已经表明，这种新的单向QFA（多字母QFA）可以毫无错误地接受某些常规语言$(a+b)^{*}b$，这些常规语言是先前的单向QFA所不能接受的。本文研究了多字母QFA等价性的判定问题，主要技术贡献如下：（1）我们证明了在同一个输入字母表$Σ$上的任意两个自动机，一个$k_{1}$ -字母QFA ${\cal A}_1$和一个$k_{2}$ -字母QFA ${\cal A}_2$是等价的当且仅当它们是$(n^2m^{k-1}-m^{k-1}+k)$ -等价的，其中$m=|Σ|$是$Σ$的基数，$k=\max(k_{1},k_{2})$，和$n=n_{1}+n_{2}$，其中$n_{1}$和$n_{2}$分别是${\cal A}_{1}$和${\cal A}_{2}$的状态数。当$k=1$时，我们得到了文献中一次测量QFA等价性的可判定性。值得一提的是，我们的技术方法本质上不同于单输入字母情况下的可判定性（即，$m=1$）。(2)然而，如果我们通过检查长度不超过$ n^2m^{k-1}-m^{k-1}+k$的所有字符串来确定多字母QFA的等价性，那么最差的时间复杂度是指数的，即，$O(n^6m^…

无序树的确定自动机

Deterministic Automata for Unordered Trees

无序无序树的自动机与定义Json或Xml格式的数据树的模式和查询有关。虽然现有的概念是很好的研究有关的表现力，他们都缺乏一个适当的概念，决定论，这使得它很难区分子类的自动机，其中的问题，如包容性，等价性和最小化可以有效地解决。在本文中，我们提出并研究了不同的概念“水平决定论”，从自动机的水平评价是由有限状态自动机进行的未排名的树。我们表明，限制合流水平评估导致多项式时间的空虚和普遍性，但仍然遭受从二进制交叉点的空虚的coNP-完全性。最后，有效的算法可以通过对类中的所有自动机全局施加水平评估的顺序来获得。根据顺序的选择，我们得到不同类别的自动机，其中每一个具有相同的表现力CMSO。

A Generic Solution to Register-bounded Synthesis with an Application to Discrete Orders

We study synthesis of reactive systems interacting with environments using an infinite data domain. A popular formalism for specifying and modelling such systems is register automata and transducers. They extend finite-state automata by adding registers to store data values and to compare the incoming data values against stored ones. Synthesis from nondeterministic or universal register automata is undecidable in general. However, its register-bounded variant, where additionally a bound on the number of registers in a sought transducer is given, is known to be decidable for universal register …

异步自动机的控制

On the Control of Asynchronous Automata

Ramadge和Wonham控制器综合问题的分布式版本的可判定性是一个具有挑战性的公开问题，其中对象和控制器都被建模为异步自动机，并且控制器具有因果记忆。存在三类对象，其具有因果记忆的正确控制器的存在已被证明是可判定的：当动作的依赖图是串并行时，当进程连接地通信时，以及当进程的依赖图是树时。设计了一类具有可判定控制器综合问题的可分解对策，给出了已有的三个可判定性结果的统一证明，并给出了可判定对策的新例子.

线性高阶元胞自动机的动力学行为及其可判定性

On the dynamical behaviour of linear higher-order cellular automata and its decidability

高阶元胞自动机（HOCA）是元胞自动机（CA）的一种变体，在许多应用中得到了应用（例如，从秘密共享方案的设计到数据压缩和图像处理），并且其中系统在时间$t$的全局状态不仅取决于在时间$t-1$的状态，如在原始模型中，而且取决于在时间$t-2, \ldots, t-n$的状态，其中，$n$是HOCA的内存大小。我们提供了两个重要的动力学性质，即，对初始条件的敏感性和等度连续性，线性HOCA在字母表$\mathbb{Z}_m$可判定的特征。这种特征扩展了[23]中所示的线性CA（LCA）在字母表$\mathbb{Z}^{n}_m$上的特征，在$n=1$的情况下。我们还证明了，线性HOCA的大小记忆$n$在$\mathbb{Z}_m$形成一类是不可区分的LCA的特定子类在$\mathbb{Z}_m^n$。这使得能够使用[2]和[19]中提供的用于$\mathbb{Z}^n_m$上的LCA的内射性和满射性的可判定特征来判定$n$上的$\mathbb{Z}_m$上的线性HOCA的内射性和满射性。最后，我们证明了在$\mathbb{Z}_m^n$上的LCA和一类重要的非均匀CA之间的等价性，非均匀CA是CA在许多应用中的另一种变体。

图幺半群上的价自动机的空性问题

The Emptiness Problem for Valence Automata over Graph Monoids

这项工作的研究，在自动机的存储机制，允许可判定性的空虚问题。这个问题是正式使用价自动机，一个抽象的自动机模型，其中的存储机制是由幺半群。对于各种存储机制中的每一种，可以选择一个（通常是无限的）幺半群$M$，使得$M$上的价自动机等价于具有这种存储类型的（单向）自动机。事实上，许多重要的存储机制可以通过有限图定义的幺半群来实现，称为图幺半群。示例包括下推堆栈、部分盲计数器（其表现得像Petri网位置）、盲计数器（其可以获得负值）及其组合。因此，我们研究的图幺半群的空性问题的价自动机是可判定的。图幺半群实现的一个特殊模型是具有下推堆栈的Petri网。对于这些，可判定性是一个长期存在的开放性问题，我们在这里不回答它。然而，如果排除对应于该模型的子图，则可以实现特征化。此外，我们提供了一个描述的存储机制，决策仍然开放。这导致了一个模型，自然推广了下推Petri网和Reinhardt引入的优先级多计数器机。被证明是可判定的情况构成了一个自然的和显然是新的扩展的Petri网与可判定的可达性。最后表明，该模型可以与另一个这样的扩展Atig和Ganty：我们提出了进一步的可判定性结果，包括这两个Petri网扩展。

A Generic Solution to Register-bounded Synthesis with an Application to Discrete Orders

We study synthesis of reactive systems interacting with environments using an infinite data domain. A popular formalism for specifying and modelling such systems is register automata and transducers. They extend finite-state automata by adding registers to store data values and to compare the incoming data values against stored ones. Synthesis from nondeterministic or universal register automata is undecidable in general. However, its register-bounded variant, where additionally a bound on the number of registers in a sought transducer is given, is known to be decidable for universal register …

具有辅助时钟和参数的时间自动机

Interrupt Timed Automata with Auxiliary Clocks and Parameters

时间自动机（ITA）是一种表达性的时间模型，根据级别考虑中断。由于这一特点，这种形式主义是不可比拟的时间自动机。然而，已经获得了一些与可达性和模型检验相关的可判定性结果。我们添加辅助时钟ITA，从而扩大其表达能力，同时保持可达性的可判定性。此外，我们定义了一个参数化版本的ITA，多项式的参数出现在警卫和更新。虽然参数推理与时间模型特别相关，但它经常导致不可判定性结果。我们证明了各种可达性问题，包括“强大的”可达性，是可判定的这个模型，我们给一个固定或可变数量的时钟，水平和参数的复杂性上界。

On Linear Time Decidability of Differential Privacy for Programs with Unbounded Inputs

We introduce an automata model for describing interesting classes of differential privacy mechanisms/algorithms that include known mechanisms from the literature. These automata can model algorithms whose inputs can be an unbounded sequence of real-valued query answers. We consider the problem of checking whether there exists a constant $d$ such that the algorithm described by these automata are $dε$-differentially private for all positive values of the privacy budget parameter $ε$. We show that this problem can be decided in time linear in the automaton's size by identifying a necessary and s…

并行组合正则表达式的模双相似性（扩展摘要）

Expressiveness modulo Bisimilarity of Regular Expressions with Parallel Composition (Extended Abstract)

有限自动机所接受的语言正是由正则表达式表示的语言。相比之下，有限自动机可能会表现出无法用正则表达式描述的行为。在本文中，我们考虑扩展的正则表达式的理论与各种形式的并行组合，并研究对表现力的影响。首先，我们证明了纯交错的正则表达式理论严格增加其表达性的双相似性。然后，我们证明，ACP风格的并行组合取代纯交织的操作给出了进一步增加的表现力。最后，我们证明了ACP风格的并行组合和封装的正则表达式的理论是足够的表达，以表示所有的有限自动机的双相似。我们的结果扩展了Bergstra，Bethke和Ponse的过程代数（的二元变体）Kleene的星操作的表现力的结果。

Parikh Automata on Infinite Words

Parikh automata on finite words were first introduced by Klaedtke and Rueß [Automata, Languages and Programming, 2003]. In this paper, we introduce several variants of Parikh automata on infinite words and study their expressiveness. We show that one of our new models is equivalent to synchronous blind counter machines introduced by Fernau and Stiebe [Fundamenta Informaticae, 2008]. All our models admit ε-elimination, which to the best of our knowledge is an open question for blind counter automata. We then study the classical decision problems of the new automata models.

概率语义下的定量自动机

Quantitative Automata under Probabilistic Semantics

本研究首次在概率语义下研究定量自动机，证明监视器计数器自动机与嵌套加权自动机等价，并揭示原本不可判定的问题在概率语义下可判定，给出完整的可判定性及近乎完整的复杂性图景。

数据自动机的一种扩展，用于捕获

An extension of data automata that captures XPath

我们定义了一种新的自动机识别数据字或数据树的属性，并证明了自动机捕获所有的查询定义在正则表达式。我们表明，自动机理论的方法可以应用于回答可判定性和可表达性问题的可预测性。

由2字母可逆Mealy自动机生成的群的有限性是可判定的

The finiteness of a group generated by a 2-letter invertible-reversible Mealy automaton is decidable

证明了由可逆二态Mealy自动机生成的半群是有限的或无秩2的。这一事实导致了由两状态或两字母可逆-可逆Mealy自动机生成的群的有限性的可判定性和由两状态可逆-可逆Mealy自动机生成的半群的自由性的可判定性。

弱嵌套类记忆自动机

Weak and Nested Class Memory Automata

无限字母表上的自动机作为解决验证和数据库理论问题的潜在有用工具，最近得到了广泛的研究。一个流行的模型研究的自动机是类记忆自动机（CMA），其中的空性问题相当于Petri网的可达性。我们确定了一个限制-我们称之为弱点-CMA，并表明其空性问题是等价于Petri网的覆盖性。此外，我们表明，在确定性的情况下，他们是封闭的所有布尔运算。我们澄清弱CMA和现有的自动机之间的连接数据语言。我们还扩展CMA操作多层次的嵌套数据值，并表明，虽然这些具有不可判定的空虚一般，增加弱点约束恢复可判定性的空虚，通过减少覆盖良好结构的过渡系统。我们还研究了嵌套数据与现有自动机的连接。

可见下推换能器的表达性

Expressiveness of Visibly Pushdown Transducers

可见下推传感器（VPT）是扩展了输出的可见下推自动机。它们已经被引入到嵌套单词的模型转换中，即具有调用/返回结构的单词。由于树和更一般的对冲可以线性化为（良好）嵌套的单词，VPT是一种自然的形式主义来表达在流中评估的树转换。本文的目的是精确地表征相对于其他树传感器模型的VPT的表达能力。

参数时间自动机中不变量的表达能力

On the expressive power of invariants in parametric timed automata

结合硬时序约束和并发性的系统的验证是具有挑战性的。当一些定时常数丢失或未知时，这个挑战变得更加困难。参数定时形式主义，如参数定时自动机（PTA），解决了这样的定时常数（被视为参数）的合成，其中一个属性成立。这样的形式主义是高度表达，但也不可判定，并提出了一些可判定的子类。在这里，我们提出了一个语法限制的PTA组成的删除警卫（限制过渡），只保持不变（限制位置）。虽然这种限制保留了PTA的表达能力（因此也保留了它们的不可判定性），但对约束类型的附加限制不仅允许证明可判定性，而且还允许执行满足可达性的参数估值的精确合成。这种形式主义，乍一看似乎微不足道，因为它受益于可达性问题的可判定性，具有比时间自动机（TA）更好的复杂性，但却受到TA相反享受的整个TCTL逻辑的不可判定性的影响。我们相信我们的形式主义允许一个有趣的权衡之间的可判定性和实际的表现力，因此是有前途的。我们在一个小的案例研究中展示了它的适用性。

The boundedness and zero isolation problems for weighted automata over nonnegative rationals

We consider linear cost-register automata (equivalent to weighted automata) over the semiring of nonnegative rationals, which generalise probabilistic automata. The two problems of boundedness and zero isolation ask whether there is a sequence of words that converge to infinity and to zero, respectively. In the general model both problems are undecidable so we focus on the copyless linear restriction. There, we show that the boundedness problem is decidable. As for the zero isolation problem we need to further restrict the class. We obtain a model, where zero isolation becomes equivalent to un…

无限词概率自动机的判定问题

Decidable Problems for Probabilistic Automata on Infinite Words

我们考虑概率自动机上的无限的话接受定义的奇偶校验条件。我们考虑三个定性决策问题：（i）正决策问题询问是否有一个词以正概率被接受;（ii）几乎决策问题询问是否有一个词以概率1被接受;（iii）极限决策问题询问是否对于每个n> 0，有一个词以至少1 -n的概率被接受。我们统一和推广的概率自动机在无限的话几个可判定性的结果，并确定一个强大的概率自动机（关闭下的工会和交集）子类，所有的定性决策问题是可判定的奇偶校验条件。我们还表明，如果输入的字被限制为套索形状（定期）的话，那么积极的和几乎的问题是可判定的所有概率自动机与奇偶校验条件。对于大多数可判定的问题，我们展示了一个最佳的PSPACE-完全复杂性界。

无穷字上的跳跃自动机

Jumping Automata over Infinite Words

本文引入并研究了无穷字上的跳跃自动机，针对无穷字重排序不明确的问题提出了三种语义，并分析了这些模型的表达能力、闭包性质和算法性质。

Parikh Automata over Infinite Words

Parikh automata extend finite automata by counters that can be tested for membership in a semilinear set, but only at the end of a run, thereby preserving many of the desirable algorithmic properties of finite automata. Here, we study the extension of the classical framework onto infinite inputs: We introduce reachability, safety, Büchi, and co-Büchi Parikh automata on infinite words and study expressiveness, closure properties, and the complexity of verification problems. We show that almost all classes of automata have pairwise incomparable expressiveness, both in the deterministic and the n…

概率自动机中基于分布的互模拟与互模拟度量

Distribution-based Bisimulation and Bisimulation Metric in Probabilistic Automata

概率自动机是拉宾在1963年作为语言接受者引入的。两个自动机是等价的，当且仅当它们以相同的概率接受每个单词。另一方面，在过程代数领域，Segala于1995年重新提出了概率自动机，它比Rabin的自动机更具有一般性。互模拟已经提出了Segala的自动机来表征它们之间的等价性。到目前为止，这两个概念的等价性和他们的特点，主要是独立的研究。在本文中，我们考虑Segala的自动机，并提出了一个新的概念，基于分布的互模拟加入现有的等价性和双相似性。我们通过研究基于分布的互模拟度量证明了我们的定义的实用性，这产生了一个强大的概念，相当于拉宾的自动机。我们比较我们的互模拟的概念，一些现有的基于分布的互模拟，并讨论其组合性和关系，跟踪等价。最后，我们展示了所有关系的可判定性和复杂性。

参数区间概率时间自动机的一致性

Consistency in Parametric Interval Probabilistic Timed Automata

基于参数时间自动机和区间马尔可夫链的扩展，我们提出了一种新的概率时间系统的抽象形式：参数区间概率时间自动机。在这种情况下，我们考虑的一致性问题，决定是否一个给定的规范承认至少一个实现。在区间概率时间自动机（没有时间参数）的背景下，我们证明了这个问题是可判定的，并提出了一个建设性的算法解决。我们表明，存在的时间参数估值，确保一致性是不可判定的一般情况下，但仍然表现出一个语法条件的参数，以确保可判定性。我们还提出了程序，解决了一致性和一致的可达性问题时，参数概率区域图是有限的。

历史寄存器自动机

History-Register Automata

程序与动态分配能够创建和使用无限数量的新鲜资源，如引用，对象，文件等，我们提出了历史寄存器自动机（HRA），一个新的自动机理论的形式主义建模这样的程序。HRA扩展了以前方法的表达能力，并使我们达到了可达性检查的可判定性极限。我们的机器的显着特点是它们使用无限的记忆集（历史），输入的符号可以有选择地存储和比较的符号遵循。此外，存储的符号可以通过重置来消耗或删除。我们表明，消费和复位功能的组合，使自动机足够强大，以模仿计数器机，并在所有常规操作下，除了互补收益率关闭。此外，我们还研究了较弱的概念HRAs之间的表现力和有效性的不同的平衡。

双向嵌套加权自动机

Bidirectional Nested Weighted Automata

嵌套加权自动机（NWA）提供了一个强大的和方便的自动机理论的形式化定量规格。以前的作品认为NWA只在向前的方向处理输入的单词。允许自动机向后处理输入单词也是很自然的，例如，测量响应和前一个请求之间的最大或平均时间。因此，我们介绍和研究双向NWA，可以处理输入的话在两个方向。首先，我们表明，双向NWA可以表达有趣的定量属性，是不能只向前NWA。其次，对于空性和普遍性的基本决策问题，我们建立了新框架的可判定性和复杂性结果，这些结果与仅向前NWA的特殊情况下的最著名结果相匹配。因此，对于NWA，在没有额外的计算复杂性的情况下实现了双向性的增加的表现力。这与未加权的情况形成鲜明对比，在未加权的情况下，双向有限自动机并不比只向前的自动机更具表达力，但比只向前的自动机更简洁。

概率密封自动机的值1判定问题

Deciding the value 1 problem for probabilistic leaktight automata

值1问题是一个概率自动机在有限词上的决策问题：给定一个概率自动机，是否有概率任意接近1的词被接受？这个问题最近被证明是不可判定的;为了克服这个问题，提出了几类不同性质的概率自动机，其中值1问题已被证明是可判定的。在本文中，我们介绍了另一类概率自动机，称为leaktight自动机，它严格包含所有类的概率自动机的值1的问题是已知的可判定的。我们证明，对于密封自动机，值1的问题是可判定的（事实上，PSPACE完全）通过构建一个饱和算法的基础上计算的幺半群抽象的自动机的行为。我们依靠西蒙开发的代数技术来证明这种抽象是完整的。此外，我们适应这种饱和算法来决定是否一个自动机是密封的。最后，我们展示了一个减少，允许我们的可判定性结果从有限字到无限的，这意味着值1的问题的概率leaktight奇偶自动机是可判定的。

无限字上的确定性帕里克自动机

Deterministic Parikh automata on infinite words

本文研究无限字上所有帕里克自动机变体的确定性版本，比较其表现力并分析闭包性质与决策问题，发现确定性极限帕里克自动机最具优势，是唯一推广$\omega$-正则语言、布尔运算封闭且决策问题可判定的模型。

有限字和树上的交替寄存器自动机

Alternating register automata on finite words and trees

我们研究交替寄存器自动机的数据字和数据树的逻辑。数据字（或数据树）是一个字（或树），其每个位置携带来自有限字母表的标签和来自无限域的数据值。我们研究单向自动机与交替控制数据字或树，一个寄存器存储数据和比较它们的平等。这是Demri，Lazic和Jurdzinski开始的研究的延续。从寄存器自动机模型的角度出发，本文的工作有两个目的：（1）简化已有的交替寄存器自动机空性问题的可判定性证明;（2）展示这些模型的可判定扩展。从逻辑的角度来看，我们表明，（a）在数据字的情况下，满足性的LTL与一个寄存器和量化的数据值是可判定的;和（b）满足性的问题，所谓的前向片段的XML文档是可判定的，即使在存在的DTD，甚至是关键的约束。可判定性是通过减少自动机模型介绍。这个片段包含子轴、后代轴、下一个兄弟轴和下一个兄弟轴，以及数据相等和不相等测试。

FC可定义正则语言的特征化与可判定性

Characterization and Decidability of FC-Definable Regular Languages

本文研究了FC可定义正则语言的特征化与可判定性，提出了一种基于星-Free广义正则表达式的简洁描述方法。

无限字母表上的（标称）omega-正则语言的可判定类

A decidable class of (nominal) omega-regular languages over an infinite alphabet

我们定义了一类在无限个字母表上有无限个词的语言，以及相应的自动机。用于识别的自动机是确定性Muller自动机的一个推广，以设置名义集。值得注意的是，所获得的语言是由它们最终的周期性片段决定的，就像经典的情况一样。在补、并、交下的封闭性，以及空性和等价性的可判定性都被推广所保持。这是通过使用有限表示（否则无限状态）定义类的自动机。