A note on the logical definability of rational trace languages (Q2893298)

This paper is a contribution to the study of the correspondence between recognizable languages and logic in the spirit of \textit{J. R. Büchi} [Z. Math. Logik Grundlagen Math. 6, 66--92 (1960; Zbl 0103.24705)]. More precisely, it shows the equivalence, for trace languages, of being rational and definable in a suitable logic. NEWLINENEWLINENEWLINE For \(A\) a finite alphabet (set) and \(I\) an irreflexive and symmetric binary relation on \(A\), the trace monoid \(M(A,I)\) is the quotient of the free monoid \(A^*\) over the congruence generated by the pairs \((ab,ba)\), where \((a,b)\in I\). The intuition being that a pair \((a,b)\in I\) represents commuting letters. An element of \(M(A,I)\) is called a trace. NEWLINENEWLINENEWLINE A subset \(S\) of \(M(A,I)\) is called rational if there exists a finite state automaton on \(A^*\) which recognizes at least one representative of each \(s\in S\). NEWLINENEWLINENEWLINE Similarly to the fact that a word of \(A^*\) is represented by a finite sequence of elements of \(A\), a trace can be represented by a finite acyclic graph whose vertices are \(A\)-labeled. The author furthermore represents a trace \(t\) as a structure \(\langle V\cup \{v_-,v_+\}; \preceq_t,(Q_a)_{a\in A}\rangle\), where \(V\) are the acyclic graph's vertices with two additional vertices \(v_-,v_+\) as least and greatest elements, \(\preceq_t\) is the transitive closure of the acyclic graph's arc relation and the \(Q_a\) are unary predicates true on vertices labeled by \(a\). NEWLINENEWLINENEWLINE This paper shows that a subset of \(M(A,I)\) is rational if and only if it is the set of models of some formula in the logic chain + FO. This logic is formed of the formulas of the form \(\exists C.\varphi\), where \(\varphi\) is a first-order formula in the language of the above structure, while \(C\) is a second-order variable representing a chain of anti-chains in the acyclic graph. Roughly speaking, such a \(C\) is a sequence \(c_1,\ldots,c_n\) of anti-chains of the acyclic graph such that, for any \(e\in c_i\), there exists an \(e'\in c_{i+1}\) with \(e\preceq_t e'\).