Testing for unboundedness of fifo channels

AbstractUndecidability of the unboundedness problem for specification models allowing fifo channels was proved a few years ago by Brand and Zafiropulo. The paper investigates a testing approach of that problem. Dealing with the general framework of systems communicating through fifo channels, we find a sufficient condition for unboundedness based on a relation between the nodes of the reachability tree. The construction of the resulting reduced tree can then be applied as well to communicating finite-state machines as to fifo nets. Moreover, the test extends existing decidability results. As a matter of fact, it becomes a decision procedure for a class of systems strictly including linear and monogeneous systems, which are the two essential classes in which decidability is already known. In order to conclude our study on a practical view, we show that a few modifications of the relation make the test available for Estelle specifications