Author name cluster

Rémi Morvan

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

6 papers

2 author rows

CSL Conference 2025 Conference Paper

The Algebras for Automatic Relations

Rémi Morvan

We introduce "synchronous algebras", an algebraic structure tailored to recognize automatic relations (a. k. a. synchronous relations, or regular relations). They are the equivalent of monoids for regular languages, however they conceptually differ in two points: first, they are typed and second, they are equipped with a dependency relation expressing constraints between elements of different types. The interest of the proposed definition is that it allows to lift, in an effective way, pseudovarieties of regular languages to that of synchronous relations, and we show how algebraic characterizations of pseudovarieties of regular languages can be lifted to the pseudovarieties of synchronous relations that they induce. Since this construction is effective, this implies that the membership problem is decidable for (infinitely) many natural classes of automatic relations. A typical example of such a pseudovariety is the class of "group relations", defined as the relations recognized by finite-state synchronous permutation automata. In order to prove this result, we adapt two pillars of algebraic language theory to synchronous algebras: (a) any relation admits a syntactic synchronous algebra recognizing it, and moreover, the relation is synchronous if, and only if, its syntactic algebra is finite and (b) classes of synchronous relations with desirable closure properties (i. e. pseudovarieties) correspond to pseudovarieties of synchronous algebras.

Details

Highlights Conference 2024 Conference Abstract

Minimizing Conjunctive Regular Path Queries

Rémi Morvan

We study the problem of minimizing conjunctive regular path queries: given a query $\gamma$ and a natural number $k$, is there a query which is semantically equivalent to $\gamma$ with at most $k$ atoms? The number of possible candidates (CRPQs with at most $k$ atoms) is not finite, since the regular languages used in such a query can be arbitrarily complex, and so the decidability of the problem is not trivial. We show that the problem is in 2ExpSpace and is ExpSpace-hard. Moreover, we study stability results: a class of queries $\mathcal{C}$ is said to be stable when for every query $\gamma$ in $\mathcal{C}$, if $\gamma$ is not minimal, then there is a strictly smaller query $\gamma'$ in $\mathcal{C}$ which is equivalent to $\gamma$. Amongst other, we show that DAG-shaped queries are stable. This is joint work with Diego Figueira and Miguel Romero.

Details

Highlights Conference 2023 Conference Abstract

Algebras for Regular Relations

Rémi Morvan

We introduce the notion of synchronous algebra, which is a type of algebras tailored to recognize regular relations: any relation admits a syntactic synchronous algebra, and this relation is regular (i. e. accepted by a synchronous automaton) if and only if this algebra is finite. We show that these algebras naturally arises using two different constructions: 1. using Bojańczyk's theory of recognizability via monads over typed sets, 2. by encoding synchronous words as finite words over an extended alphabet: synchronous algebras arise as the class of monoids that are quotiented by the syntactic monoid of "well-formed words", namely the language of all words corresponding to some encoding. Lastly, we show why this notion of algebra is inherently more suitable to studying properties of regular relations compared to monoids or semigroups. Contributed talk given by Rémi Morvan

Details

MFCS Conference 2023 Conference Paper

Separating Automatic Relations

Pablo Barceló
Diego Figueira
Rémi Morvan

We study the separability problem for automatic relations (i. e. , relations on finite words definable by synchronous automata) in terms of recognizable relations (i. e. , finite unions of products of regular languages). This problem takes as input two automatic relations R and R', and asks if there exists a recognizable relation S that contains R and does not intersect R'. We show this problem to be undecidable when the number of products allowed in the recognizable relation is fixed. In particular, checking if there exists a recognizable relation S with at most k products of regular languages that separates R from R' is undecidable, for each fixed k ⩾ 2. Our proofs reveal tight connections, of independent interest, between the separability problem and the finite coloring problem for automatic graphs, where colors are regular languages.

Details

Highlights Conference 2022 Conference Abstract

First-order Separation over Countable Scattered Linear Orders

Rémi Morvan

We consider regular languages of words whose domain is a countable scattered linear ordering (examples of countable scattered linear orders include the set of integers or any countable ordinal). Given two regular languages, we want to decide whether there exists a formula of first-order logic that is satisfied by every word of the first language but by no word of the other. We prove that this problem is decidable using an algebraic construction: given a morphism from the set of all words to a finite scattered monoid, we show that one can effectively build a function that approximates the original morphism while being definable in first-order logic. Essentially, this approximant is obtained from the original morphism by forgetting about group-like phenomena and gap-detection using an algorithm resembling Henckell's saturation algorithm for computing aperiodic pointlike sets of finite semigroups. We also study the case of words indexed by countable ordinals (on which first-order logic admits a simpler characterisation), which was published at FoSSaCS '22, and separation by first-order logic extended with monadic quantification over Dedekind cuts. This is joint work with Thomas Colcombet and Sam van Gool.

Details

Highlights Conference 2020 Conference Abstract

A Universal Attractor Decomposition Algorithm for Parity Games

Rémi Morvan

An attractor decomposition meta-algorithm for solving parity games is given that generalizes the classic McNaughton-Zielonka algorithm and its recent quasi-polynomial variants due to Parys (2019), and to Lehtinen, Schewe, and Wojtczak (2019). The central concepts studied and exploited are attractor decompositions of dominia in parity games and the ordered trees that describe the inductive structure of attractor decompositions. The main technical results include the embeddable decomposition theorem and the dominion separation theorem that together help establish a precise structural condition for the correctness of the universal algorithm: it suffices that the two ordered trees given to the algorithm as inputs embed the trees of some attractor decompositions of the largest dominia for each of the two players, respectively. The universal algorithm yields McNaughton-Zielonka, Parys’s, and Lehtinen-Schewe-Wojtczak algorithms as special cases when suitable universal trees are given to it as inputs. The main technical results provide a unified proof of correctness and deep structural insights into those algorithms. This paper motivates a research program of developing new efficient algorithms for solving parity games by designing new classes of small trees that embed the largest dominia in relevant classes of parity games. An early success story in this research program is the recent development, by Daviaud, Jurdziński, and Thejaswini (2019), of Strahler-universal trees, which embed dominia in games of bounded register number, introduced by Lehtinen (2018). When run on these trees, the universal algorithm can solve games with bounded register number in polynomial time and in quasi-linear space. A symbolic implementation of the universal algorithm is also given that improves the symbolic space complexity of solving parity games in quasi-polynomial time from — achieved by Chatterjee, Dvořák, Henzinger, and Svozil (2018) — down to, where is the number of vertices and is the number of distinct priorities in a parity game. This not only exponentially improves the dependence on, but it also entirely removes the dependence on. Joint work with Marcin Jurdziński.

Details