Synchronized tree languages revisited and new applications

Abstract

We present a new formulation for tree-tuple synchronized languages, much simpler than the existing one. This new formulation allows us to prove stronger structural results. As a consequence, synchronized languages give rise to new applications: - to rewriting: given tree languages L1 (synchronized), L2 (regular), Rel(L1) ⊆ L2 is decidable for several rewrite-like relations Rel. - to concurrency: we prove decidability of the logic EF for a process calculus allowing some bounded form of communication. Consequently, the absence of deadlocks is decidable.