Boolean Algebras from Trace Automata - Université de La Réunion Access content directly
Conference Papers Year : 2019

Boolean Algebras from Trace Automata


We consider trace automata. Their vertices are Mazurkiewicz traces and they accept finite words. Considering the length of a trace as the length of its Foata normal form, we define the operations of level-length synchronization and of superposition of trace automata. We show that if a family F of trace automata is closed under these operations, then for any deterministic automaton H ∈ F, the word languages accepted by the deterministic automata of F that are length-reducible to H form a Boolean algebra. We show that the family of trace suffix automata with level-regular contexts and the subfamily of vector addition systems satisfy these closure properties. In particular, this yields various Boolean algebras of word languages accepted by deterministic vector addition systems. 2012 ACM Subject Classification Theory of computation → Formal languages and automata theory In automatic verification, it is useful to highlight families of languages with good closure properties, as for example Boolean algebras of languages. For example, the fact that the first-order theory of any word-automatic graph 1 is decidable essentially relies on the Boolean closure properties of regular languages: to any relation defined by a first-order formula, there corresponds (in an effective way) a regular language and the problem of deciding whether the graph satisfies a given statement reduces to the problem of deciding emptiness for the corresponding regular language [13]. The regular, context-free, context-sensitive and recursively enumerable languages form a famous increasing hierarchy of formal language families defined by Chomsky in [8] from grammars of increasing complexity. It can also be obtained from families of automata. Indeed, regular languages are accepted by finite automata, context-free languages are accepted by pushdown automata (or more generally by word suffix automata [2]), context-sensitive languages are accepted, for instance, by bounded synchronized automata [20], and recursively enumerable languages are accepted by Turing machines [4]. And if it is well-known that regular languages or context-sensitive languages form a Boolean algebra, it is also well-known that it is not the case of context-free languages. Nevertheless, it was shown that various subclasses of context-free languages form Boolean algebras [17, 18, 5], as for example visibly pushdown languages with respect to a given pushdown alphabet [1]. Besides, pushdown automata model sequential computations. For parallel computations, a relevant family of automata consists of vector addition systems. Hence, the question arises of which Boolean algebras can be obtained from this family of automata. 1 A word-automatic graph is a graph of which the vertex set is a regular language and each relation is recognized by a finite letter by letter synchronized transducer.
Fichier principal
Vignette du fichier
LIPIcs-FSTTCS-2019-48.pdf (696 Ko) Télécharger le fichier
Origin Publisher files allowed on an open archive

Dates and versions

hal-03009734 , version 1 (17-11-2020)




Alexandre Mansard. Boolean Algebras from Trace Automata. 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019), Dec 2019, Bombay, India. pp.48:1-48:15, ⟨10.4230/LIPIcs.FSTTCS.2019.48⟩. ⟨hal-03009734⟩
104 View
75 Download



Gmail Mastodon Facebook X LinkedIn More