Forbidden Patterns for FO2 Alternation Over Finite and Infinite Words

DOI10.1142/S0129054123440021arXiv2105.09291OpenAlexW4321498545MaRDI QIDQ6169964FDOQ6169964

Authors: Viktor Henriksson, Manfred Kufleitner 

Publication date: 15 August 2023

Published in: International Journal of Foundations of Computer Science (Search for Journal in Brave)

Abstract: We consider two-variable first-order logic $ext{FO}^2$ and its quantifier alternation hierarchies over both finite and infinite words. Our main results are forbidden patterns for deterministic automata (finite words) and for Carton-Michel automata (infinite words). In order to give concise patterns, we allow the use of subwords on paths in finite graphs. This concept is formalized as subword-patterns. For certain types of subword-patterns there exists a non-deterministic logspace algorithm to decide their presence or absence in a given automaton. In particular, this leads to $mathbfNL$ algorithms for deciding the levels of the $ext{FO}^2$ quantifier alternation hierarchies. This applies to both full and half levels, each over finite and infinite words. Moreover, we show that these problems are $mathbfNL$-hard and, hence, $mathbfNL$-complete.

Full work available at URL: https://arxiv.org/abs/2105.09291

zbMATH Keywords

finite model theoryregular languageautomataforbidden patterninfinite words

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Model theory of finite structures (03C13) Descriptive complexity and finite models (68Q19)

Cites Work

• Title not available (Why is that?)
• Complexity of some problems from the theory of automata
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• On finite monoids having only trivial subgroups
• Title not available (Why is that?)
• Characterizations of some classes of regular events
• On the expressive power of temporal logic
• Languages of dot-depth 3/2
• Finite-automaton aperiodicity is PSPACE-complete
• Unambiguous Büchi automata.
• A SURVEY ON SMALL FRAGMENTS OF FIRST-ORDER LOGIC OVER FINITE WORDS
• First-order fragments with successor over infinite words
• Fragments of first-order logic over infinite words
• Structure Theorem and Strict Alternation Hierarchy for FO^2 on Words
• Level two of the quantifier alternation hierarchy over infinite words
• Varieties
• The half-levels of the \(\mathrm {FO}_2\) alternation hierarchy
• An Effective Characterization of the Alternation Hierarchy in Two-Variable Logic
• The \(\mathrm{FO}^2\) alternation hierarchy is decidable
• Forbidden patterns for ordered automata
• Effective characterizations of simple fragments of temporal logic using Carton-Michel automata
• Deciding \(\mathrm{FO}^2\) alternation for automata over finite and infinite words

This page was built for publication: Forbidden Patterns for FO² Alternation Over Finite and Infinite Words

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6169964)