moteur de recherche

Séminaire Algo - Amazigh Amrane
Séminaire Algo - Amazigh Amrane
10-Mar-2020 14:00
Age: 316 days

Amazigh Amrane

Scattered and countable series-parallel posets : logic and equational theory

Salle de séminaire (4B125) - Bâtiment Copernic

Abstract: Since it was established by Büchi, Elgot and Trakhtenbrot in the early 60's, the connection between automata theory and formal logic has been intensively developed in many directions.

An important application is decision algorithms for logical theories. Since then, many notions of automata have been introduced: automata on trees, on linear orderings, etc. Among these automata, we focus on automata over SP\diamond(A): the class of all countable N-free posets labeled by A, in which chains are scattered linear orderings and antichains are finite.This class is the one built from the empty and the singleton poset, using finite sequential product, finite parallel product, ω and -ω products.

Automata over SP\diamond(A) were introduced by N. Bedon and C. Rispal.They are a generalization of branching automata of P. Weil and K. Lodaya, over finite N-free posets, and of automata of V. Bruyère and O. Carton, over scattered and countable linear orderings.We give an effective logical characterization of the class of languages recognized by such automata. The logic involved is an extension of MSO with Presburger arithmetic, named P-MSO. The effective construction of an automaton from a formula of P-MSO is a mere adaptation of the case of finite words. A decision procedure for the P-MSO theory of SP\diamond(A) follows.On the other hand, the usual techniques for building a P-MSO formula from an automaton can not be directly applied.

Starting from a rational expression (effectively equivalent to automata), we build a graph that we parse and transform into a formula of P-MSO. In the parsing of the graph, recursivity is avoided by a MSO-expressible identification of particular factors of posets.From the algebraic point of view, SP\diamond(A) is freely generated by A in its corresponding variety.

By removing the parallel product, it follows that the class of scattered and countable words is also a free algebra in its corresponding variety.We also consider the class ω SP(A) where the ω and -ω products are replaced by ω and -ω powers.

It is freely generated in its corresponding variety, and has a decidable equational theory. This work is carried out in cooperation with Nicolas Bedon.

<- Back to: Accueil