Undecidable verification problems for programs with unreliable channels

We consider the class of finite-state systems communicating through unbounded but lossy FIFO channels (called lossy channel systems). These systems have infinite state spaces due to the unboundedness of the channels. In an earlier paper, we showed that the problems of checking reachability, safety properties, and eventuality properties are decidable for lossy channel systems. In this paper, we show that the following problems are undecidable: The model checking problem in propositional temporal logics such as propositional linear time temporal logic (PTL) and computation tree logic (CTL). The problem of deciding eventuality properties with fair channels: do all computations eventually reach a given set of states if the unreliable channels satisfy fairness assumptions? The results are obtained through reduction from a variant of the Post correspondence problem. (C) 1996 Academic Press. Inc.