arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 2601.18429

Algebraic Characterizations of Classes of Regular Languages in DynFO

Corentin Barloy·Felix Tschirbs·Nils Vortmeier·Thomas Zeume
View original source ↗Read source document ↗Export metadata ↓

Abstract

This paper explores the fine-grained structure of classes of regular languages maintainable in fragments of first-order logic within the dynamic descriptive complexity framework of Patnaik and Immerman. A result by Hesse states that the class of regular languages is maintainable by first-order formulas even if only unary auxiliary relations can be used. Another result by Gelade, Marquardt,and Schwentick states that the class of regular languages coincides with the class of languages maintainable by quantifier-free formulas with binary auxiliary relations. We refine Hesse's result and show that with unary auxiliary data formulas with one quantifier alternation can maintain all regular languages. We then obtain precise algebraic characterizations of the classes of languages maintainable with quantifier-free formulas and positive existential formulas in the presence of unary auxiliary relations.

Explore related subjects

cs.LOcs.FL

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Corentin Barloy, Felix Tschirbs, Nils Vortmeier, Thomas Zeume. 2026-01-26. Algebraic Characterizations of Classes of Regular Languages in DynFO. https://arxiv.org/abs/2601.18429

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

A Probabilistic Choreography Language for PRISM

We present a choreographic framework for modelling and analysing concurrent probabilistic systems based on the PRISM model-checker. This is achieved through the development of a choreography language, which is a specification language that allows to describe the desired interactions within a concurrent system from a global viewpoint. Using choreographies gives a clear and complete view of system interactions, making it easier to understand the process flow and identify potential errors, which helps ensure correct execution and improves system reliability. We equip our language with a probabilistic semantics and then define a formal encoding into the PRISM language and discuss its correctness. Properties of programs written in our choreographic language can be model-checked by the PRISM model-checker via their translation into the PRISM language. Finally, we implement a compiler for our language and demonstrate its practical applicability via examples drawn from the use cases featured in the PRISM website.

cs.LO↗
arXiv2026

Monotone weak distributive laws over the lifted powerset monad in categories of algebras

Noticing the similarity between the monotone weak distributive laws combining two layers of nondeterminism in sets and in compact Hausdorff spaces, we study whether the latter law can be obtained automatically as a weak lifting of the former. This holds partially, but does not generalize to other categories of algebras: we then characterize when exactly monotone weak distributive laws over powerset monads in categories of algebras exist, exhibiting a law combining probabilities and non-determinism in compact Hausdorff spaces and showing on the other hand that such laws do not exist in a lot of other cases.

cs.LO↗
arXiv2026

Identifying and Explaining (Non-)Equivalence of First-Order Logic Formulas

First-order logic is the basis for many knowledge representation formalisms and methods. Providing technological support for learning to write first-order formulas for natural language specifications requires methods to test formulas for (non-)equivalence and to provide explanations for non-equivalence. We propose such methods based on both theoretical insights and existing tools, implement them, and report on experiments testing their effectiveness on a large educational data set with > 100,000 pairs of first-order formulas.

cs.LO↗