DocumentCode
2234527
Title
Deciding boundedness for systems of two communicating finite state machines
Author
Benslimane, Abderrahim
Author_Institution
Lab. d´´Inf., UFR des Sci., Besancon, France
fYear
1994
fDate
2-5 Aug 1994
Firstpage
262
Lastpage
269
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/HPDC.1994.340236
Filename
340236
Link To Document