Thiagarajan and Walukiewicz [18] have defined a temporal logic LTrL on Mazurkiewicz traces, patterned on the famous propositional
temporal logic of linear time LTL defined by Pnueli. They have shown that this logic is equal in expressive power to the first
order theory of finite and infinite traces.
The hopes to get an ”easy” decision procedure for LTrL, as it is the case for LTL, vanished very recently due to a result
of Walukiewicz [19] who showed that the decision procedure for LTrL is non-elementary.
However, tools like Mona [8] or Mosel [7] show that it is possible to handle non-elementary logics on significant examples.
Therefore, it appears worthwhile to have a direct decision procedure for LTrL; in this paper we propose such a decision procedure,
in a modular way. Since the logic LTrL is not pure future, our algorithm constructs by induction a finite family of Büchi
automata for each LTrL-formula. As expected by the results of [19], the main difficulty comes from the ”Until” operator.
Topics logic in computer science - automata and formal languages - theory of parallel and distributed computation - model-checking