# Generalized Fair Reachability Analysis for Cyclic Protocols

 dc.contributor.author Liu, Hong en_US dc.contributor.author Miller, Raymond E. en_US dc.date.accessioned 2004-05-31T21:02:58Z dc.date.available 2004-05-31T21:02:58Z dc.date.created 1995-02 en_US dc.date.issued 1998-10-15 en_US dc.identifier.uri http://hdl.handle.net/1903/423 dc.description.abstract In this paper, the notion of fair reachability is generalized to cyclic protocols with $n\geq 2$ machines. Substantial state reduction can be achieved via fair progress state exploration. It is shown that the fair reachable state space is exactly the set of reachable states with equal channel length. As a result, deadlock detection is decidable for ${\cal P}$, the class of cyclic protocols whose fair reachable state spaces are finite. The concept of simultaneous unboundedness is defined and the lack of it is shown to be a necessary and sufficient condition for a protocol to be in ${\cal P}$. Through finite extension of the fair reachable state space, it is also shown that detection of unspecified receptions, unboundedness, and nonexecutable transitions are all decidable for ${\cal P}$. Furthermore, it is shown that any protocol ${\cal P}$ is logically correct if and only if there is no logical error in its fair reachable state space. This study shows that for the class ${\cal P}$, our generalized fair reachability analysis technique not only achieves substantial state reduction but also maintains very competitive logical error coverage. Therefore, it is a very useful technique to prove logical correctness for a wide variety of cyclic protocols. en_US dc.format.extent 329275 bytes dc.format.mimetype application/postscript dc.language.iso en_US dc.relation.ispartofseries UM Computer Science Department; CS-TR-3421 en_US dc.title Generalized Fair Reachability Analysis for Cyclic Protocols en_US dc.type Technical Report en_US dc.relation.isAvailableAt Digital Repository at the University of Maryland en_US dc.relation.isAvailableAt University of Maryland (College Park, Md.) en_US dc.relation.isAvailableAt Tech Reports in Computer Science and Engineering en_US dc.relation.isAvailableAt Computer Science Department Technical Reports en_US
﻿