  The paper deals with the verification of reachability properties in a
commonly used state transition model of communication protocols, which consists
of finite state machines connected by potentially unbounded FIFO channels.
Although simple reachability problems are undecidable for general protocols
with unbounded channels, they are decidable for the protocols with the
recognizable channel property. The decidability question is open for the
protocols with the rational channel property.
