AN EXTENSION OF KLEENE AND OCHMANSKI THEOREMS TO INFINITE TRACES

As was noted by Mazurkiewicz, traces constitute a convenient tool for describing finite behaviour of concurrent systems. Extending in a natu ral way Mazurkiewicz's original definition, infinite traces have recen tly been introduced enabling one to deal with infinite behaviour of no nterminating concurrent systems. In this paper we examine the basic fa milies of recognizable sets and of rational sets of infinite traces. T he seminal Kleene characterization of recognizable subsets of the free monoid and its subsequent extensions to infinite words due to Buchi a nd to finite traces due to Ochmanski are the cornerstones of the corre sponding theories. The main result of our paper is an extension of the se characterizations to the domain of infinite traces. Using recognizi ng and weakly recognizing morphisms as well as a generalization of the Schutzenberger product of monoids, we prove various closure propertie s of recognizable trace languages. Moreover, we establish normal-form representations for recognizable and rational sets of infinite traces.