Skip to Main content Skip to Navigation
Theses

Automates infinis et traces de Mazurkiewicz

Abstract : We introduce the notion of level-regularity for Mazurkiewicz trace languages and we consider recognizable trace rewriting systems with level-regular contexts (RTLsystem). We prove that an automaton for which the underlying graph is the rewriting graph of a RTL system and for which the sets of initial vertices and final vertices are level-regular (RTL automaton), is word-automatic. In particular, the first-order theory of a RTL automaton is decidable. Then, we prove that, enriched with thereachability relation, an automaton for which the underlying graph is the concurrent unfolding of a finite concurrent graph, and for which the sets of initial vertices and final vertices are level-regular, is RTL. In particular, the first-order theory with the reachability predicate of such an automaton is decidable. Besides, it is known that this property also holds for ground term rewriting graphs (GTR graph). We highlight various concurrent unfoldings of finite concurrent graphs that are not GTRgraphs. The infinite quarter grid tree is such an unfolding. The class of concurrent unfoldings of finite concurrent graphs is therefore a class of word-automatic graphs for which the first-order theory with the reachability predicate is decidable and that contains some non GTR graphs. We define the operations of level-length synchronization and level-length superposition of trace automata (automata for which vertices are Mazurkiewicz traces) and we prove that if a family F of trace automata is closed under these operations, then for any deterministic trace automaton H 2 F, the languages accepted by the deterministic trace automata belonging to F and that are length-reducible to H, form a Boolean algebra; the length of a trace being the length of its Foata normal form, a trace automaton G is length-reducible to a trace automaton H if there exists a length-preserving morphism from G to H. Then, we show that the family of trace suffix automata with level regular contexts, the extension of word suffix automata to Mazurkiewicz traces, satisfies these closure properties. We define a generalized Petri net as a trace suffix automaton over a dependence alphabet for which the dependence is reduced to the equality and we show that the subfamily of generalized Petri nets also satisfies the closure properties above. In particular, this yields various Boolean algebras of word languages accepted by deterministic generalized Petri nets.
Document type :
Theses
Complete list of metadata

https://tel.archives-ouvertes.fr/tel-03150688
Contributor : Abes Star :  Contact
Submitted on : Wednesday, February 24, 2021 - 1:01:11 AM
Last modification on : Wednesday, November 3, 2021 - 6:03:25 AM
Long-term archiving on: : Tuesday, May 25, 2021 - 6:08:38 PM

File

2020LARE0022_A_Mansard.pdf
Version validated by the jury (STAR)

Identifiers

  • HAL Id : tel-03150688, version 1

Citation

Alexandre Mansard. Automates infinis et traces de Mazurkiewicz. Automatique. Université de la Réunion, 2020. Français. ⟨NNT : 2020LARE0022⟩. ⟨tel-03150688⟩

Share

Metrics

Record views

196

Files downloads

105