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 this theory is an attempt to relate the properties of these monoids to the properties of I. Following the work initiated by Buchi we show that when the reflexive closure of I is transitive (the trace monoid is then 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 rational. This logic essentially utilizes a predicate based on the partial ordering defined by the dependence graph and a predicate related to a restricted use of the comparison of cardinality.