Since 1981, we know that the unboundedness is an undecidable problem for systems of finite state machines that communicate exclusively by exchanging messages over unidirectional, FIFO channels. This led some authors to reduce the general model in order to find restricted classes in where the problem becomes decidable. In this paper, we present a new class of systems constituted of two linear Communicating finite state machines. A linear machine is a directed graph where each strongly connected component is reduced to an elementary circuit. We show for this class that the boundedness problem is decidable. Consequently, the decision procedures can be automatized and integrated into the frame of Computer-Aided Systems Technology. Examples will be used to illustrate our purpose.
展开▼
