Testing for unboundedness of fifo channels (Q685434)

Undecidability of the unboundedness problem for specification models allowing fifo channels was proved a few years ago by \textit{D. Brand} and \textit{P. Zafiropulo} [On communicating finite-state machines, J. Assoc. Comput. Mach. 30, 323-342 (1983; Zbl 0512.68039)]. The paper investigates a testing approach of that problem in the general framework of systems communicating through fifo channels. We find a sufficient condition for unboundedness of fifo channels based on a relation involving the nodes of the reachability tree (labelled with global states) and transition sequences between them. This relation induces a test for unboundedness by the construction of a reduced tree. This construction can then be applied as well to communicating finite state machines as to fifo-nets and essentially allows to detect unboundedness due to regular growing of fifo channels. Moreover, as a side effect, the test extends existing decidability results. Linear and monogeneous systems were the two essential classes in which decidability was already known. Now, when applied in the class of word-linear systems, which strictly includes linear and monogeneous systems, our test becomes a decision procedure. In order to conclude our study on a practical view, we study the applicability of our test in the context of the specification language Estelle. We show that a few modifications of the relation make the test available for Estelle specifications.