A logical characterization of observation equivalence (Q802306)

\textit{S. D. Brookes} and \textit{W. C. Rounds} [Lect. Notes Comput. Sci. 154, 97-108 (1983; Zbl 0536.68042)] showed that a finitary formal language ('regular trace language', or Reg-TL, for short) which allowed a certain kind of quantification using regular subsets of \(\Sigma^*\) was not strong enough to distinguish all pairs of observationally inequivalent synchronization trees. In the present paper this result is extended to show that there is no class C of subsets of \(\Sigma^*\) such that C-TL can distinguish all pairs of observationally inequivalent synchronization trees. Then a characterization of observation equivalence in terms of an infinitary formal language S-TL(\(\omega)\) is given. This language is obtained as an extension of the language S-TL ('singleton trace language') of Hennessy and Milner by the addition of a connective of \(\omega\)-conjunctions of formulas of finite bounded depth.