TESTING FOR UNBOUNDEDNESS OF FIFO CHANNELS

Undecidability of the unboundedness problem for specification models a llowing fifo channels was proved a few years ago by Brand and Zafiropu lo. The paper investigates a testing approach of that problem. Dealing with the general framework of systems communicating through fifo chan nels, we find a sufficient condition for unboundedness based on a rela tion between the nodes of the reachability tree. The construction of t he resulting reduced tree can then be applied as well to communicating finite-state machines as to fifo nets. Moreover, the test extends exi sting decidability results. As a matter of fact, it becomes a decision procedure for a class of systems strictly including linear and monoge neous systems, which are the two essential classes in which decidabili ty is already known. In order to conclude our study on a practical vie w, we show that a few modifications of the relation make the test avai lable for Estelle specifications.