Infinite traces

Abstract

Trace languages are used in computer science to provide a description of the behaviours of concurrent systems. If we are interested in systems which never stop then we have to consider languages of infinite traces. In this paper, we generalize to infinite traces three well known points of view about finite traces: equivalence class of words, projections on the dependence cliques and dependence graphs. These approaches are complementary and, depending on the problem we deal with, each of them can prove to be more appropriate than the others. In this way, we obtain an infinitary trace monoid and extend Levi's lemma and the Foata normal form. Next, we prove that the infinitary trace monoid is a completely coherent PoSet. We also define an ultrametric distance and prove that it is a complete metric space. Therefore, either the PoSet or the topological framework can be used to solve fix-point equations and then to provide semantics of recursive constructs. Finally, we introduce recognizable languages of finite and infinite traces. We prove that they are characterized by a syntactic congruence and that the family of recognizable languages is closed by concatenation and by the Boolean operations: union, intersection and complement.