LOGICAL DEFINABILITY OF SOME RATIONAL TRACE LANGUAGES

Trace monoids are obtained from free monoids by defining a subset I of pairs of letters that are allowed to commute. Most of the work of thi s theory is an attempt to relate the properties of these monoids to th e properties of I. Following the work initiated by Buchi we show that when the reflexive closure of I is transitive (the trace monoid is the n a free product of free commutative monoids) it is possible to define a second-order logic whose models are the traces viewed as dependence graphs and which characterizes exactly the sets of traces that are ra tional. This logic essentially utilizes a predicate based on the parti al ordering defined by the dependence graph and a predicate related to a restricted use of the comparison of cardinality.