Showing 1–9 of 9 results for author: Sénizergues, G

Word-Map**s of level $3$

Authors: G. Sénizergues

Abstract: Sequences of numbers (either natural integers, or integers or rational) of level $k \in \mathbb{N}$ have been defined in \cite{Fra05,Fra-Sen06} as the sequences which can be computed by deterministic pushdown automata of level $k$. This definition has been extended to sequences of {\em words} indexed by {\em words} in \cite{Sen07,Fer-Mar-Sen14}. We characterise here the sequences of level 3 as the… ▽ More Sequences of numbers (either natural integers, or integers or rational) of level $k \in \mathbb{N}$ have been defined in \cite{Fra05,Fra-Sen06} as the sequences which can be computed by deterministic pushdown automata of level $k$. This definition has been extended to sequences of {\em words} indexed by {\em words} in \cite{Sen07,Fer-Mar-Sen14}. We characterise here the sequences of level 3 as the compositions of two HDT0L-systems. Two applications are derived: - the sequences of rational numbers of level 3 are characterised by polynomial recurrences - the equality problem for sequences of rational numbers of level 3 is decidable. △ Less

Submitted 11 October, 2023; v1 submitted 24 January, 2023; originally announced January 2023.

Comments: 46 pages. 1 figure

MSC Class: 68; 40; 08 ACM Class: F.1.1; G.2.1; I.1.1

Regular matching problems for infinite trees

Authors: Carlos Camino, Volker Diekert, Besik Dundua, Mircea Marin, Géraud Sénizergues

Abstract: We study the matching problem of regular tree languages, that is, "$\exists σ:σ(L)\subseteq R$?" where $L,R$ are regular tree languages over the union of finite ranked alphabets $Σ$ and $\mathcal{X}$ where $\mathcal{X}$ is an alphabet of variables and $σ$ is a substitution such that $σ(x)$ is a set of trees in $T(Σ\cup H)\setminus H$ for all $x\in \mathcal{X}$. Here, $H$ denotes a set of "holes" w… ▽ More We study the matching problem of regular tree languages, that is, "$\exists σ:σ(L)\subseteq R$?" where $L,R$ are regular tree languages over the union of finite ranked alphabets $Σ$ and $\mathcal{X}$ where $\mathcal{X}$ is an alphabet of variables and $σ$ is a substitution such that $σ(x)$ is a set of trees in $T(Σ\cup H)\setminus H$ for all $x\in \mathcal{X}$. Here, $H$ denotes a set of "holes" which are used to define a "sorted" concatenation of trees. Conway studied this problem in the special case for languages of finite words in his classical textbook "Regular algebra and finite machines" published in 1971. He showed that if $L$ and $R$ are regular, then the problem "$\exists σ\forall x\in \mathcal{X}: σ(x)\neq \emptyset\wedge σ(L)\subseteq R$?" is decidable. Moreover, there are only finitely many maximal solutions, the maximal solutions are regular substitutions, and they are effectively computable. We extend Conway's results when $L,R$ are regular languages of finite and infinite trees, and language substitution is applied inside-out, in the sense of Engelfriet and Schmidt (1977/78). More precisely, we show that if $L\subseteq T(Σ\cup\mathcal{X})$ and $R\subseteq T(Σ)$ are regular tree languages over finite or infinite trees, then the problem "$\exists σ\forall x\in \mathcal{X}: σ(x)\neq \emptyset\wedge σ_{\mathrm{io}}(L)\subseteq R$?" is decidable. Here, the subscript "$\mathrm{io}$" in $σ_{\mathrm{io}}(L)$ refers to "inside-out". Moreover, there are only finitely many maximal solutions $σ$, the maximal solutions are regular substitutions and effectively computable. The corresponding question for the outside-in extension $σ_{\mathrm{oi}}$ remains open, even in the restricted setting of finite trees. △ Less

Submitted 31 January, 2022; v1 submitted 21 April, 2020; originally announced April 2020.

MSC Class: 68Q70; 68Q45 ACM Class: F.4

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 1 (February 1, 2022) lmcs:7241

On polynomial recursive sequences

Authors: Michaël Cadilhac, Filip Mazowiecki, Charles Paperman, Michał Pilipczuk, Géraud Sénizergues

Abstract: We study the expressive power of polynomial recursive sequences, a nonlinear extension of the well-known class of linear recursive sequences. These sequences arise naturally in the study of nonlinear extensions of weighted automata, where (non)expressiveness results translate to class separations. A typical example of a polynomial recursive sequence is b_n=n!. Our main result is that the sequence… ▽ More We study the expressive power of polynomial recursive sequences, a nonlinear extension of the well-known class of linear recursive sequences. These sequences arise naturally in the study of nonlinear extensions of weighted automata, where (non)expressiveness results translate to class separations. A typical example of a polynomial recursive sequence is b_n=n!. Our main result is that the sequence u_n=n^n is not polynomial recursive. △ Less

Submitted 20 February, 2020; originally announced February 2020.

The isomorphism problem for finite extensions of free groups is in PSPACE

Authors: Géraud Sénizergues, Armin Weiß

Abstract: We present an algorithm for the following problem: given a context-free grammar for the word problem of a virtually free group $G$, compute a finite graph of groups $\mathcal{G}$ with finite vertex groups and fundamental group $G$. Our algorithm is non-deterministic and runs in doubly exponential time. It follows that the isomorphism problem of context-free groups can be solved in doubly exponenti… ▽ More We present an algorithm for the following problem: given a context-free grammar for the word problem of a virtually free group $G$, compute a finite graph of groups $\mathcal{G}$ with finite vertex groups and fundamental group $G$. Our algorithm is non-deterministic and runs in doubly exponential time. It follows that the isomorphism problem of context-free groups can be solved in doubly exponential space. Moreover, if, instead of a grammar, a finite extension of a free group is given as input, the construction of the graph of groups is in NP and, consequently, the isomorphism problem in PSPACE. △ Less

Submitted 20 February, 2018; originally announced February 2018.

MSC Class: 68Q45; 68Q25; 05C25; 20E08; 20F10; 20F65 ACM Class: F.4.3; F.2.2; G.2.2

Equations over free inverse monoids with idempotent variables

Authors: Volker Diekert, Florent Martin, Geraud Senizergues, Pedro V. Silva

Abstract: We introduce the notion of idempotent variables for studying equations in inverse monoids. It is proved that it is decidable in singly exponential time (DEXPTIME) whether a system of equations in idempotent variables over a free inverse monoid has a solution. The result is proved by a direct reduction to solve language equations with one-sided concatenation and a known complexity result by Baade… ▽ More We introduce the notion of idempotent variables for studying equations in inverse monoids. It is proved that it is decidable in singly exponential time (DEXPTIME) whether a system of equations in idempotent variables over a free inverse monoid has a solution. The result is proved by a direct reduction to solve language equations with one-sided concatenation and a known complexity result by Baader and Narendran: Unification of concept terms in description logics, 2001. We also show that the problem becomes DEXPTIME hard , as soon as the quotient group of the free inverse monoid has rank at least two. Decidability for systems of typed equations over a free inverse monoid with one irreducible variable and at least one unbalanced equation is proved with the same complexity for the upper bound. Our results improve known complexity bounds by Deis, Meakin, and Senizergues: Equations in free inverse monoids, 2007. Our results also apply to larger families of equations where no decidability has been previously known. △ Less

Submitted 25 September, 2015; v1 submitted 11 December, 2014; originally announced December 2014.

Comments: 28 pages. The conference version of this paper appeared in the proceedings of 10th International Computer Science Symposium in Russia, CSR 2015, Listvyanka, Russia, July 13-17, 2015. Springer LNCS 9139, pp. 173-188 (2015)

MSC Class: 20M18; 20F70; 03D40 ACM Class: F.4; F.2; F.2.2

FREC 14: FRontiers of RECognizability

Authors: Géraud Sénizergues

Abstract: These proceedings are gathering twelve different research papers develop** the theory of recognizability for various kinds of discrete objects: words. terms, graphs, etc... These proceedings are gathering twelve different research papers develop** the theory of recognizability for various kinds of discrete objects: words. terms, graphs, etc... △ Less

Submitted 12 December, 2014; v1 submitted 20 November, 2014; originally announced November 2014.

Comments: Proceedings of the conference FREC 14 held in Marseille, 38-30 April 2014. 12 papers contributed by 14 authors

ACM Class: F.1.1; F.4.1; F.4.3; G.2.2

Jancar's formal system for deciding bisimulation of first-order grammars and its non-soundness

Authors: Géraud Sénizergues

Abstract: We construct an example of proof within the main formal system from arXiv:1010.4760v3, which is intended to capture the bisimulation equivalence for non-deterministic first-order grammars, and show that its conclusion is semantically false. We then locate and analyze the flawed argument in the soundness (meta)-proof of the above reference. We construct an example of proof within the main formal system from arXiv:1010.4760v3, which is intended to capture the bisimulation equivalence for non-deterministic first-order grammars, and show that its conclusion is semantically false. We then locate and analyze the flawed argument in the soundness (meta)-proof of the above reference. △ Less

Submitted 26 January, 2011; originally announced January 2011.

Comments: 12 pages, 9 figures

ACM Class: F.4.2; F.4.3

Bottom-up rewriting for words and terms

Authors: Irene Durand, Geraud Senizergues

Abstract: For the whole class of linear term rewriting systems, we define \emph{bottom-up rewriting} which is a restriction of the usual notion of rewriting. We show that bottom-up rewriting effectively inverse-preserves recognizability and analyze the complexity of the underlying construction. The Bottom-Up class (BU) is, by definition, the set of linear systems for which every derivation can be replaced b… ▽ More For the whole class of linear term rewriting systems, we define \emph{bottom-up rewriting} which is a restriction of the usual notion of rewriting. We show that bottom-up rewriting effectively inverse-preserves recognizability and analyze the complexity of the underlying construction. The Bottom-Up class (BU) is, by definition, the set of linear systems for which every derivation can be replaced by a bottom-up derivation. Membership to BU turns out to be undecidable, we are thus lead to define more restricted classes: the classes SBU(k), k in N of Strongly Bottom-Up(k) systems for which we show that membership is decidable. We define the class of Strongly Bottom-Up systems by SBU = U_{k in \} SBU(k). We give a polynomial sufficient condition for a system to be in $\SBU$. The class SBU contains (strictly) several classes of systems which were already known to inverse preserve recognizability: the inverse left-basic semi-Thue systems (viewed as unary term rewriting systems), the linear growing term rewriting systems, the inverse Linear-Finite-Path-Ordering systems. △ Less

Submitted 31 July, 2013; v1 submitted 14 March, 2009; originally announced March 2009.

Comments: 86 pages; long version to be cut into pieces for publication

The Bisimulation Problem for equational graphs of finite out-degree

Authors: G. Senizergues

Abstract: The "bisimulation problem" for equational graphs of finite out-degree is shown to be decidable. We reduce this problem to the bisimulation problem for deterministic rational (vectors of) boolean series on the alphabet of a dpda M. We then exhibit a complete formal system for deducing equivalent pairs of such vectors. The "bisimulation problem" for equational graphs of finite out-degree is shown to be decidable. We reduce this problem to the bisimulation problem for deterministic rational (vectors of) boolean series on the alphabet of a dpda M. We then exhibit a complete formal system for deducing equivalent pairs of such vectors. △ Less

Submitted 22 August, 2000; originally announced August 2000.

Comments: 98 pages, 4 figures, submitted to JACM

ACM Class: F.1.1; F.4.2; F.4.3; G.2.2