Pa. Abdulla et B. Jonsson, UNDECIDABLE VERIFICATION PROBLEMS FOR PROGRAMS WITH UNRELIABLE CHANNELS, Information and computation, 130(1), 1996, pp. 71-90
Citations number
34
Categorie Soggetti
Information Science & Library Science",Mathematics,"Computer Science Information Systems
We consider the class of finite-state systems communicating through un
bounded but lossy FIFO channels (called lossy channel systems). These
systems have infinite state spaces due to the unboundedness of the cha
nnels. In an earlier paper, we showed that the problems of checking re
achability, safety properties, and eventuality properties are decidabl
e 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 eventualit
y properties with fair channels: do all computations eventually reach
a given set of states if the unreliable channels satisfy fairness assu
mptions? The results are obtained through reduction from a variant of
the Post correspondence problem. (C) 1996 Academic Press. Inc.