Portal de Periódicos da CAPES

An extension of Kleene's and Ochmański's theorems to infinite traces

1994; Elsevier BV; Volume: 125; Issue: 2 Linguagem: Francês

10.1016/0304-3975(94)90254-2

1879-2294

Paul Gastin, Antoine Petit, Wiesław Zielonka,

Logic, programming, and type systems

As was noted by Mazurkiewicz, traces constitute a convenient tool for describing finite behaviour of concurrent systems. Extending in a natural way Mazurkiewicz's original definition, infinite traces have recently been introduced enabling one to deal with infinite behaviour of nonterminating concurrent systems. In this paper we examine the basic families of recognizable sets and of rational sets of infinite traces. The seminal Kleene characterization of recognizable subsets of the free monoid and its subsequent extensions to infinite words due to Büchi and to finite traces due to Ochmański are the cornerstones of the corresponding theories. The main result of our paper is an extension of these characterizations to the domain of infinite traces. Using recognizing and weakly recognizing morphisms, as well as a generalization of the Schützenberger product of monoids, we prove various closure properties of recognizable trace languages. Moreover, we establish normal-form representations for recognizable and rational sets of infinite traces. Mazurkiewicz a montré que le monoïde des traces forme un modèle tout à fait adapté à la description des comportements des systèmes concurrents. En étendant de façon très naturelle la définition originale de Mazurkiewicz, les traces infinies ont été récemment introduites afin de modéliser les comportements infinis des systèmes concurrents qui ne s'arrêtent pas. Ce papier est consacré à l'étude des familles de langages reconnaissables et de langages rationnels de traces infinies. Le théorème de Kleene, son extension aux mots infinis par Büchi et son extension aux traces finies par Ochmański sont des résultats fondamentaux de ces théories. Le résultat principal de cet article étend ce théorème aux langages de traces infinies. En utilisant la notion de morphismes reconnaissants et faiblement reconnaissants ainsi qu'une généralisation du produit de Schützenberger pour les monoïdes, on prouve des propriétés de clôture de la famille des langages reconnaissables de traces infinies. De plus, on établit des formes normales permettant de représenter les langages rationnels et reconnaissables de traces infinies.