Fragments of first-order logic over infinite words
我们给出了Ω语言的一阶逻辑FO[<]的下列子类的拓扑和代数特征以及语言理论描述：Sigma_2，FO^2，FO^2和Sigma_2的交集，以及Delta_2（并通过对偶Pi_2和FO^2和Pi_2的交集）。这些描述扩展了有限词的相应结果。特别是，我们将上述片段与某些（明确的）多项式的语言类联系起来。一个直接的结果是这些类的成员资格问题的可判定性，但这是由Wilke和Bojanczyk之前证明的，因此不是我们的主要焦点。本文是关于代数，拓扑和语言理论性质的相互作用。
2009-10-02 cs.FL cs.LO
Feasible Automata for Two-Variable Logic with Successor on Data Words
我们介绍了一个自动机模型的数据字，这是在每个位置进行一个符号从一个有限的字母表和一个值从一个无界的数据域的话。该模型是（语义）的数据自动机，介绍了Bojanczyk，等的限制。在2006年，它被称为弱数据自动机。它的表达能力比数据自动机差，而表达能力又是寄存器自动机无法比拟的。弱数据自动机的表达能力与后继为+1且数据值相等\sim，EMSO 2（+1，\sim）的存在一元二阶逻辑完全对应。它遵循从以前的工作，大卫，等。等人在2010年提出了弱数据自动机的非空性问题可以在2-NEXPTIME中判定。此外，我们还研究了数据ω-串上的弱Büchi自动机。它们可以用EMSO 2（+1，\sim）的扩展来刻画，其中存在量词用于无限集合.最后，通过对弱数据自动机的非空性问题进行非确定性多项式时间约简，得到了其非空性问题的复杂性界。
2011-10-06 cs.FL cs.LO
Automata and temporal logic over arbitrary linear time
线性时序逻辑是为了推理反应系统而引入的。它通常被认为是关于无限的话，指定长期运行的系统的行为。我们可以考虑线性时间的更一般的模型，使用由任意线性排序索引的词。我们调查的时间逻辑和自动机之间的联系，线性排序，介绍了Bruyère和纸箱。我们提供了一个双指数过程，从任何LTL公式计算直到，因为，和Stavi连接词的自动机，决定该公式是否对输入字。特别地，由于这些自动机的空性问题是可判定的，这种变换给出了逻辑可满足性的判定过程。
2011-01-10 cs.FL cs.LO
An automaton over data words that captures EMSO logic
我们开发了一个通用的框架，其执行系统的规范和实施的话，或偏序，在一个无限的字母表。作为一个模型的实现，我们引入类寄存器自动机，一个单向自动机模型的话多个数据值。我们的模型结合了寄存器自动机和类记忆自动机。它有自然的解释。特别是，它捕获通信自动机与无限数量的进程，其语义可以被描述为一组（动态）消息序列图。在规范方面，我们提供了一个局部存在一元二阶逻辑，不对变量的数量施加任何限制。我们研究的可实现性问题，并表明，从逻辑的每一个公式可以有效地，并在小学的时间，翻译成一个等价的类寄存器自动机。
2011-06-10 cs.FL
Ordered Navigation on Multi-attributed Data Words
我们研究了多属性数据词的时态逻辑和自动机。最近，BD-LTL被引入作为一个时间逻辑上的数据字扩展LTL的导航沿单数据值的位置。允许航行。元组的数据值使逻辑不可判定的，我们介绍了ND-LTL，BD-LTL的一个扩展的元组导航的限制形式。虽然完整的ND-LTL仍然是不可判定的，两个自然的片段，无论是未来或过去的导航沿数据值被证明是阿克曼硬，但可判定性是通过减少嵌套多计数器系统。为此，我们介绍和研究嵌套的数据自动机的变种作为一个中间模型简化的建设。为了补充这些结果，我们表明，施加相同的限制BD-LTL产生两个2 ExpSpace完整的片段，而满足性的完整的逻辑是已知的硬可达性在Petri网。
2014-04-24 cs.FL cs.LO
Languages of Dot-depth One over Infinite Words
在有限字上，点深度为1的语言对于无交替的一阶逻辑是表达完备的。这个片段也被称为存在一阶逻辑的布尔闭包。这里，原子公式包括顺序、后继、最小和最大谓词。Knast（1983）证明了一种语言是否具有点深度是可判定的。我们将Knast的结果推广到无限词。特别是，我们描述了类的语言定义的交替自由的一阶逻辑在无限的话，我们给出了一个有效的表征这个片段。这一特征有两个组成部分。第一个组成部分是相同的Knast的代数属性有限的话，第二个组成部分是一个拓扑属性，即是一个布尔组合康托集。作为一个中间步骤，我们同时考虑有限和无限的话。然后，我们得到的结果，无限的话，以及有限的话作为特殊情况。特别地，我们给出了有限字上点深为1的语言的Knast定理的一个新证明。
2011-04-01 cs.FL cs.LO
Rankers over Infinite Words
我们考虑有限和无限字上的一阶逻辑FO[<]的四个片段FO2，Sigma2和FO2的交集，Pi2和FO2的交集，以及Delta2。对于所有四个片段，我们给出的排名方面的特征。特别是，我们推广的概念，排名无限的话在两种可能的方式。这两个扩展都是自然的，因为在有限词上，它们与经典的秩相一致，而在无限词上，它们都具有FO2的全部表达能力。此外，秩的第一个扩展允许Sigma2和FO2的交集的表征，而另一个扩展导致Pi2和FO2的交集的表征。这两种版本的排名产生的片段Delta2的表征。作为一个副产品，我们还获得了基于明确的时间逻辑和明确的时间间隔逻辑的特征。
2010-05-04 cs.FL cs.LO
Parameterized Synthesis for Fragments of First-Order Logic over Data Words
研究了具有参数化进程数的系统的综合问题。在Church的经典案例中，系统根据到目前为止运行的程序选择动作，目的是满足给定的规范。困难在于，与此同时，环境执行系统无法控制的操作。与固定的有限字母表的情况相反，这里我们考虑参数化字母表的情况。字母表反映了静态但未知的进程的数量。综合问题然后问是否有一个有限数量的过程，系统可以满足规范。这种变体对于非常有限的逻辑已经是不可判定的。因此，我们考虑一个一阶逻辑没有顺序的词的位置。我们表明，即使在这种限制的情况下，合成是不可判定的，如果系统和环境都可以访问所有的进程。另一方面，我们证明了问题是可判定的，如果环境只能访问有限数量的进程。在这种情况下，甚至有一个截止值，这意味着它足以检查有限数量的过程架构来解决综合问题。
2019-10-31 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
Regular Cost Functions, Part I: Logic and Algebra over Words
正则代价函数理论是经典正则性概念的定量扩展。成本函数将每个输入关联到非负整数值（或无穷大），而不是仅将每个输入关联到“内部”和“外部”两个值的语言。这个理论是距离自动机和类似模型的工作的延续。这些自动机模型已成功地用于解决词上一元二阶逻辑的星高问题、有限幂性质、有限替换问题、相对包含星高问题和有界性问题。我们的正则性概念可以--就像在正则语言的经典理论中一样--等价地用自动机、表达式、代数可识别性和一元二阶逻辑的变体来定义。这些等价性是相应经典结果的严格推广。本文介绍了代价一元逻辑，它是我们所使用的一元二阶逻辑概念的定量推广，并证明了这种逻辑的某些界存在性问题是可判定的。这是通过引入相应的代数形式：稳定化幺半群。
2013-08-09 cs.FL
Monadic Second Order Logic with Measure and Category Quantifiers
本文研究了在无限词和树上，将一元二阶逻辑扩展为带有基于贝尔范畴和勒贝格测度的广义“几乎全部”量词，探讨其表达能力和性质。
2018-04-09 cs.FL cs.LO math.LO
Weighted Automata and Monadic Second Order Logic
设S是交换半环。M. Droste和P.Gastin在2005年引入了加权一元二阶逻辑WMSOL，其权在S。他们使用WMSOL的语法片段RMSOL来表征加权自动机可识别的词函数（幂级数），其中量词的语义既用作算术运算，又在布尔情况下用作量化。早在2001年，B. Courcelle、J.Makowsky和U. Rotics已经引入了一种形式主义，用于在Monadic二阶逻辑中定义的图参数，这里称为MSOLEVAL，其值在环R中。它们的框架可以很容易地适应于半环S。这种形式主义清楚地将逻辑部分与算术部分分开，并且也适用于词函数。本文给出了两个证明：值在S中的RMSOL和MSOLEVAL对词具有相同的表达能力。一个证明直接表明，MSOLEVAL捕获的功能可识别的加权自动机。另一个证明展示了如何将形式主义从一个转换成另一个。
2013-07-17 cs.FL cs.LO
POTL: A First-Order Complete Temporal Logic for Operator Precedence Languages
模型检验程序的问题促进了对上下文无关结构推理的时态逻辑定义的研究。其中最值得注意的是嵌套词的时态逻辑，如CaRet和NWTL。最近，基于操作符先后次序语言（OPL）类的逻辑OPTL被引入，它比嵌套字更强大。我们定义了新的基于OPL的逻辑POTL，证明了它的FO-完全性，并提供了一个模型检验过程。POTL改进了NWTL，使制定的要求，涉及前/后条件，堆栈检查，和其他的异常结构的存在。它在OPTL的基础上进行了改进，因为它是FO完备的，并且更容易表达堆栈检查和函数局部属性。
2020-10-31 cs.FL cs.LO
The Alternation Hierarchy of First-Order Logic on Words is Decidable
本文证明了一阶逻辑FO[<]的$Σ_i[<]$片段在正则语言上的可判定性，解决了1971年以来的开放问题，核心是通过多项式闭包技术将可判定分离问题从正簇扩展至其多项式闭包。
2025-01-31 cs.FL cs.LO math.LO
Logical and Algebraic Characterizations of Rational Transductions
本文将有界非周期语言的可判定性提升至有理转换，证明可判定给定同余类中的转换，并建立逻辑-代数等价传递，从而判定一阶可定义性，且该问题为PSPACE完全。
2019-12-18 cs.FL cs.LO
Languages recognised by finite semigroups, and their generalisations to objects such as trees and graphs, with an emphasis on definability in monadic second-order logic
这些是关于正则语言的代数方法的课堂讲稿。经典的代数方法是针对有限字的;它使用半群而不是自动机。然而，代数方法可以扩展到单词以外的结构，例如~无限的单词，或者树，或者图这本书的目的是描述代数方法的方式，涵盖这些扩展。
2020-08-26 cs.FL
Conjunctive Queries for Logic-Based Information Extraction
本文提出了两种基于逻辑的信息抽取中的合取查询方法。第一种也是主要的方法是引入逻辑FC和FC[REG]的合取查询片段，分别表示为FC-CQ和FC[REG]-CQ。FC是一种基于词方程的一阶逻辑，其中语义通过将论域限制为某个有限输入词的因子来定义。FC[REG]是带有正则约束的FC扩展。第二种方法是考虑FC的动态复杂性。
2022-08-02 cs.DB cs.FL cs.LO
An Algebraic Characterisation of First-Order Logic with Neighbour
本文给出了一阶逻辑在有限字上的一个代数刻画。对于这一点，我们考虑语言的有限字的字母与对合。这类语言的自然代数是对合半群。为了证明这个逻辑，我们定义了对合半群的一种特殊的半直积，称为局部厄米积。FO与邻居的特征定理指出，一种语言在逻辑中是可定义的，当且仅当它被非周期交换对合半群和局部平凡对合半群的局部埃尔米特积所识别。然后，我们定义的概念，对合品种的语言，即类的语言关闭下布尔运算，对合，对合和逆图像的对合态射。建立了语言的对合簇与对合半群的伪簇之间的Eilenberg型对应。
2021-05-19 cs.FL cs.LO
Nesting negations in FO2 over infinite words
我们考虑无限词上的二元一阶逻辑FO 2。限制嵌套否定的数量定义了一个无限的层次结构;它的级别通常被称为FO 2量词交替层次结构的半级。对于这个层次结构的每一个层次，我们给出了一个有效的表征。对于较低的水平，这个特征是一个代数和拓扑性质的组合。对于更高的层次，代数性质证明是足够的。在二元一阶逻辑中，每个代数性质都是Ω项的一个有序恒等式。拓扑性质与没有两变量限制的量词交替层次结构的下半层相同（即，Cantor拓扑和字母拓扑）。我们的结果推广了有限词的相应结果。证明使用新的技术，是基于一个完善的Mal'cev产品有序monoid。
2020-12-02 cs.FL cs.LO
A Simple Obligation to Metric Interval Temporal Logic
Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF（巴黎萨克雷大学、法国国家科学研究中心、巴黎萨克雷高等师范学院、LMF实验室）；Chennai Mathematical Institute, India and CNRS, ReLaX, IRL 2000（印度金奈数学研究所、法国国家科学研究中心、ReLaX联合研究）
研究MITL可满足性，基于跟踪时间约束义务的想法提出新方法，通过引入时间概念增强检查LTL公式真值的方式，用简单机制消除或合并冗余义务，发展出基于区域的符号过程。
2026-07-16 cs.FL cs.LO
Level Two of the Quantifier Alternation Hierarchy over Infinite Words
逻辑片断的各种判定问题的研究在计算机科学中有着悠久的历史。本文研究无限词上的一阶逻辑片段的隶属问题，该隶属问题要求给定的语言是否在某个固定片段中可定义。引入字母拓扑作为片段$Σ_2$在无限词上的有效表征的一部分。这里，$Σ_2$由一阶公式和两个量词块组成，从一个存在量词开始。它的布尔闭包是$\mathbb{B}Σ_2$。我们的第一个主要结果是字母拓扑的布尔闭包的一个有效的刻画，即给定一个$ω$ -正则语言$L$，在字母拓扑中$L$是否是开集的布尔组合是可判定的.然后，这是用于转移地点和Zeitoun的最近的可判定性结果$\mathbb{B}Σ_2$从有限到无限的话。
2015-09-21 cs.FL cs.LO
Extensions of $ω$-Regular Languages
我们考虑一元二阶逻辑在$ω$ -词上的扩展，这是通过添加一种不是$ω$ -正则的语言而得到的。我们表明，如果添加的语言$L$有一个中立的字母，那么由此产生的逻辑必然是不可判定的。一个推论是，$ω$ -正则语言是唯一可判定的布尔封闭的完整三元组在$ω$ -字。
2020-02-21 cs.FL cs.LO
The First-Order Theory of Binary Overlap-Free Words is Decidable
我们表明，一阶逻辑理论的二进制无符号的话（更一般地说，$α$ -自由的话，合理的$α$，$2 < α \leq 7/3$），是可判定的。因此，以前通过繁琐的基于案例的证明获得的关于这类的许多结果现在可以使用决策过程“自动”证明。
2022-09-07 cs.DM cs.FL cs.LO
Deterministic Logics for UL
Schutzenberger定义了Unambient Star-Free正则语言（UL）类，它是由Unambient多项式定义的语言类。UL已经被各种各样的逻辑所表征（在有限字上），例如TL[X_a，Y_a]，TL[F，P]，FO 2 [<]，幺半群的变体DA，以及偏序双向DFA（po 2DFA）。我们重温这门语言课程，重点是明确性的概念，并为UL发展确定性逻辑的概念。确定性逻辑的公式唯一地解析一个词以评估满意度。我们发现，几个确定性逻辑鲁棒UL的特征。此外，我们得到建设性的减少，从这些逻辑的po 2DFA自动机。这些减少也使我们能够显示NP完全满意的复杂性所考虑的确定性逻辑。诸如TL[F，P]、F02 [<]的逻辑不是确定性的，并且已经被示出使用代数方法来表征UL。然而，还没有已知的建设性减少从这些逻辑po 2DFA。我们使用确定性逻辑来弥合这一差距。对于一个给定的TL[F，P]公式的语言等价po 2DFA的构造和我们分析其大小相对于TL[F，P]公式的大小。这是一个有效的约简，它给出了TL[F，P]公式的NP-完全可满足复杂性的另一种证明。
2014-01-13 cs.FL cs.LO
The theory of concatenation over finite models
我们提出了FC，一个新的逻辑的话，结合有限模型理论的串联理论-一阶逻辑，是基于字方程。与连接理论一样，FC也是建立在词方程的基础上的;与之相反，它的语义被定义为只允许有限模型，将宇宙限制在一个词及其所有因子上。因此，FC在有限模型上具有FO的许多理想属性，同时比FO[<]更具表达力。在这些理想的属性中最值得注意的是有效的模型检验的充分标准，以及通过为传递闭包或不动点添加运算符来捕获各种复杂性类。FC不仅使我们能够获得新的见解和技术的表达能力和有效的评估文件spectrum，但它也提供了一个通用的框架，逻辑的话，也有潜在的应用在其他领域。
2021-05-13 cs.DB cs.FL cs.LO
Separating Regular Languages with First-Order Logic
给定两种语言，分隔符是包含第一种语言且与第二种语言不相交的第三种语言。本文研究了如下判定问题：给定两种有限字的正则输入语言，判定是否存在一阶可定义分隔符。我们证明，为了回答这个问题，可以从识别输入语言的半群中提取足够的信息，使用不动点计算。这就产生了一个EXPTIME算法来检查一阶可分性。此外，该算法的正确性证明产生了一个更强的结果，即一个可能的分离器的描述。最后，我们推广这种技术来回答同样的问题的正则语言的无限词。
2016-03-08 cs.FL cs.LO
Tree Languages Defined in First-Order Logic with One Quantifier Alternation
我们研究了可以在Δ_2中定义的树语言。这些是树型语言，可由一阶公式定义，其量词前缀为forall exists，同时也可由一阶公式定义，其量词前缀为。对于量词自由部分，我们考虑两个签名，要么后代关系单独或连同字典序关系在节点上。本文给出了在Δ_2中可定义的树语言和森林语言的一个有效刻画。这个特征是用代数方程表示的。在词上，可定义在Δ_2中的词语言类构成了鲁棒类，Pin和Weil给出了鲁棒类的一个有效的代数刻画。
2010-10-20 cs.FL cs.LO
Decidability, Complexity, and Expressiveness of First-Order Logic Over the Subword Ordering
我们考虑一阶逻辑的子字排序有限的话，每个字是作为一个常数。我们的第一个结果是，$Σ_1$理论是不可判定的（已经超过两个字母）。我们调查的可判定性边界考虑片段，但一定数量的变量交替有界，这意味着变量必须始终量化的语言与有限数量的字母交替。我们证明了当至多两个变量不是交替有界的，$Σ_1$片段是可判定的，当三个变量不是交替有界的，它变得不可判定。对于更高的量词交替深度，我们证明了$Σ_2$片段已经是不可判定的一个变量没有交替界，当所有的变量是交替有界的，整个一阶理论是可判定的。
2021-09-24 cs.FL cs.LO
Ranked enumeration of MSO logic on words
在过去的几年中，具有有限延迟的枚举算法已经吸引了许多关注的数据管理任务。给定一个查询和数据，任务是预处理数据，然后逐个枚举查询的所有答案，不重复。这种枚举方案通常在解决方案被处理时很有用，或者当我们想在找到相关的解决方案后停止枚举时很有用。然而，在当前的方案中，解决方案的顺序没有限制，这个顺序通常取决于所使用的技术，而不是与用户的相关性。本文研究了一元二阶逻辑（MSO）在解被排序时的计数问题。我们提出了一个框架的基础上MSO成本函数，允许表达MSO公式的话与成本与每个解决方案。然后，我们证明了我们的框架，其中包括，例如，文档spectrum和定期复杂事件处理查询，并增加排名的一般性。本文的主要技术成果是一个算法，枚举所有的解决方案的公式，在成本增加的顺序有效地，即与一个线性的预处理阶段和对数延迟之间的解决方案。该算法的新颖性是基于使用功能数据结构，特别是通过扩展功能Brodal队列，以适应MSO对字的排名枚举。
2020-10-15 cs.DS cs.FL
One Quantifier Alternation in First-Order Logic with Modular Predicates
添加模谓词产生了一阶逻辑FO在词上的推广。FO[<，MOD]与顺序比较$x<y$和$x \equiv i \mod n$的谓词的表达能力已经由Barrington，Compton，Straubing和Therien研究过。FO[<，MOD]-片段的研究由Chaubard，Pin和Straubing发起。最近，Dartois和Paperman证明了双变量片段FO 2 [<，MOD]中的可定义性是可判定的。在本文中，我们继续这一工作路线。我们给出了Sigma 2 [<，MOD]中词语言的一个有效的代数刻画.片段Sigma 2由前束范式中的一阶公式组成，具有以存在块开始的两个量词块。此外，我们还证明了Sigma 2 [<，MOD]的最大子类Delta 2 [<，MOD]在否定下是封闭的，它具有与二元逻辑FO 2 [<，MOD]相同的表达能力。这将Therien和Wilke的结果FO 2 [<] = Delta 2 [<]推广到模块化谓词。作为副产品，我们获得了FO 2 [<，MOD]的另一个可判定的特征。
2014-07-01 cs.FL cs.LO
Adding successor: A transfer theorem for separation and covering
给定一个词语言类C，C-分离问题要求一个算法，给定两个正则语言作为输入，判断C中是否存在包含第一种语言的第三种语言，同时与第二种语言不相交。分离通常被研究作为获得对类C的深入理解的一种手段。在本文中，我们主要感兴趣的是由逻辑形式定义的类。这样的类通常构建在彼此之上：给定一些逻辑，通过向其签名添加新谓词来构建更强大的类。一个自然的结构是用后继关系来丰富逻辑。在本文中，我们提出了一个转移结果适用于此建设：我们表明，适当的逻辑定义的类，分离的逻辑丰富的后继关系减少到分离的原始逻辑。我们的定理也适用于一个比分离更强的问题：覆盖。此外，我们实际上提出了两个约简：一个是有限词的语言，另一个是无限词的语言。
2017-09-28 cs.FL
Structure Theorem and Strict Alternation Hierarchy for FO^2 on Words
众所周知，词的每个一阶属性最多可以使用三个变量来表达。仅用两个变量可表达的性质的子类也很有趣，并且得到了很好的研究。我们证明了精确的结构定理，其特征在于精确的表达能力的一阶逻辑与两个变量的话。我们的结果适用于有和没有后继关系的情况。对于这两种语言，我们的结构定理准确地显示了使用给定的量词深度n和使用m个交替量词块，对于任何m \leq n，可以表达什么。使用这些特征，我们证明，除其他结果外，有一个严格的层次结构交替量词的两种语言。是否存在这样一种等级制度的问题是完全公开的。作为我们的结构结果的另一个后果，我们表明，可满足性的一阶逻辑与两个变量没有继任者，这是NEXP-完全的一般情况下，成为NP-完全的，一旦我们只考虑有界大小的字母表。
2009-08-03 cs.FL cs.LO
Boundedness in languages of infinite words
本文定义了严格扩展ω-正则语言的新语言类，通过引入两种新的Kleene星号变体（有界和无界）及对应的自动机模型，并证明了补集引理，从而为相关逻辑MSOLB获得部分可判定性结果。
2017-10-25 cs.FL cs.LO
Alternating register automata on finite words and trees
我们研究交替寄存器自动机的数据字和数据树的逻辑。数据字（或数据树）是一个字（或树），其每个位置携带来自有限字母表的标签和来自无限域的数据值。我们研究单向自动机与交替控制数据字或树，一个寄存器存储数据和比较它们的平等。这是Demri，Lazic和Jurdzinski开始的研究的延续。从寄存器自动机模型的角度出发，本文的工作有两个目的：（1）简化已有的交替寄存器自动机空性问题的可判定性证明;（2）展示这些模型的可判定扩展。从逻辑的角度来看，我们表明，（a）在数据字的情况下，满足性的LTL与一个寄存器和量化的数据值是可判定的;和（b）满足性的问题，所谓的前向片段的XML文档是可判定的，即使在存在的DTD，甚至是关键的约束。可判定性是通过减少自动机模型介绍。这个片段包含子轴、后代轴、下一个兄弟轴和下一个兄弟轴，以及数据相等和不相等测试。
2012-03-07 cs.DB cs.FL cs.LO
Going higher in the First-order Quantifier Alternation Hierarchy on Words
本文研究了一阶逻辑中有限词的量词交替层次。此层次结构中的级别是通过计算公式中量词交替的次数来定义的。我们证明了一个可以决定成员的正则语言的水平$\mathcal{B}Σ_2$（布尔组合的公式只有1交替）和$Σ_3$（公式只有2交替开始的存在块）。我们的证明是通过考虑一个更深层次的问题来实现的，这个问题称为分离，一旦解决了较低层次的问题，我们就可以解决更高层次的成员资格问题。
2014-04-27 cs.FL cs.LO
Learning Formulas in Finite Variable Logics
我们考虑有限变量逻辑中公式和项的语法限制的精确学习。我们提出了一种新的和通用的自动机理论技术来解决这些问题。我们首先展示了学习公式的结果，这些公式对一组正标记和负标记的结构进行分类。我们给算法的实现和合成等公式的上限和下限。我们还建立了积极的结果，使用我们的技术为其他逻辑和变体的学习问题，包括一阶逻辑与最少不动点定义，高阶逻辑，和合成的查询和术语与递归定义的功能。
2021-11-12 cs.FL cs.LO cs.PL
Decidable Problems for Probabilistic Automata on Infinite Words
我们考虑概率自动机上的无限的话接受定义的奇偶校验条件。我们考虑三个定性决策问题：（i）正决策问题询问是否有一个词以正概率被接受;（ii）几乎决策问题询问是否有一个词以概率1被接受;（iii）极限决策问题询问是否对于每个n> 0，有一个词以至少1 -n的概率被接受。我们统一和推广的概率自动机在无限的话几个可判定性的结果，并确定一个强大的概率自动机（关闭下的工会和交集）子类，所有的定性决策问题是可判定的奇偶校验条件。我们还表明，如果输入的字被限制为套索形状（定期）的话，那么积极的和几乎的问题是可判定的所有概率自动机与奇偶校验条件。对于大多数可判定的问题，我们展示了一个最佳的PSPACE-完全复杂性界。
2011-07-11 cs.FL
A Transfer Theorem for the Separation Problem
我们研究了C类正则词语言的两个问题。C-成员问题需要一个算法来判断输入语言是否属于C。C-分离问题要求一种算法，给定两种正则语言作为输入，判断C中是否存在包含第一种语言的第三种语言，同时与第二种语言不相交。这些问题被认为是手段，以获得一个深刻的理解类C。这类类通常由逻辑形式定义。逻辑通常通过添加新的谓词建立在彼此之上。一个自然的结构是用后继关系来丰富逻辑。本文给出了两个转移结果的简单的自包含证明：证明了对于适当的逻辑定义类，成员关系，用后继关系丰富的类的分离问题简化为原始类的相同问题。我们的约简对有限词和无限词的语言都有效。证明大多是自包含的，只需要正则语言的基本背景。因此，本文给出了新的，简单的证明结果，被认为是困难的，如决定性的隶属度问题的水平1，3/2，2和5/2的点深度层次。
2015-01-03 cs.FL
