VERIFYING IDENTICAL COMMUNICATING PROCESSES IS UNDECIDABLE

We prove that boundedness and reachability tree finiteness are undecid able for systems of two identical automata communicating via two perfe ct unbounded one-way FIFO channels and constructed solely from cycles about their initial states. Using a form of mutual exclusion for such systems, we prove further that undecidability holds even when the iden tical automata are totally indistinguishable in the sense that their i nitial states are identical and both channels are initially empty.