Deciding boundedness for systems of two communicating finite state machines
Abderrahim Benslimane · 2002
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.>