Testing for unboundedness of fifo channels (Q685434)

From MaRDI portal
scientific article
Language Label Description Also known as
English
Testing for unboundedness of fifo channels
scientific article

    Statements

    Testing for unboundedness of fifo channels (English)
    0 references
    0 references
    0 references
    17 October 1993
    0 references
    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.
    0 references
    unboundedness
    0 references
    fifo channels
    0 references
    decidability
    0 references
    Estelle specifications
    0 references

    Identifiers