2003/06/22 by Jan Pachl, Pachl, Jan
Computer Science · #C.2.2 #D.2.4 #F.1.1 #F.3.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Networking and Internet Architecture (cs.NI) #cs.LO #cs.NI
paper · pdf · doi:10.48550/arxiv.cs/0306121
University of Waterloo, Department of Computer Science Research Report; May 1982; 66 pages, 24 figures; formatted for arXiv: June 2003; arXiv v2 (corrected typos): March 2012
arxiv created 2012/03/20 · arxiv updated 2012/03/21
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.