Title :
Deciding boundedness for systems of two communicating finite state machines
Author :
Benslimane, Abderrahim
Author_Institution :
Lab. d´´Inf., UFR des Sci., Besancon, France
Abstract :
Consider a system of two communicating finite state machines that exchange messages over two unbounded, one-directional, FIFO channels. In our main result, we show that the boundedness problem is decidable for the class of such systems, where the two CFSMs are identical and constituted of only initial elementary circuits, and where the two CFSMs are linear. To analyse such systems, we introduce a reduction relation on the words. We then give examples to illustrate our purpose
Keywords :
decidability; finite state machines; formal specification; open systems; protocols; FIFO channels; boundedness; communicating finite state machines; data communication protocols; deadlock; decidability; distributed systems; initial elementary circuits; modelisation; open communications networks; protocols; reachability tree; reduction relation; specification; validation; Automata; Channel capacity; Circuit analysis; Communication networks; Data communication; Protocols; Reachability analysis; System recovery; Tin;
Conference_Titel :
High Performance Distributed Computing, 1994., Proceedings of the Third IEEE International Symposium on
Conference_Location :
San Francisco, CA
Print_ISBN :
0-8186-6395-2
DOI :
10.1109/HPDC.1994.340236
