Browsing by Author "Liu, Hong"

Now showing 1 - 3 of 3
  • Thumbnail Image
    Item
    Generalized Fair Reachability Analysis for Cyclic Protocols
    (1998-10-15) Liu, Hong; Miller, Raymond E.
    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.
  • Thumbnail Image
    Item
    Generalized Fair Reachability Analysis for Cyclic Protocols with Nondeterminism and Internal Transitions
    (1998-10-15) Liu, Hong; Miller, Raymond E.
    In this paper, we extend the generalized fair reachability notion to cyclic protocols with nondeterminism and internal transitions. By properly incorporating internal transitions into the formulation of fair progress vectors, we prove that most of the results established for cyclic protocols without nondeterminism and internal transitions still hold even if nondeterminism and internal transitions are allowed. We identify indefiniteness as a new type of logical error resulting from reachable internal execution cycles and show that indefiniteness can also be detected for the class of cyclic protocols with finite fair reachable state spaces with finite extensions.
  • Thumbnail Image
    Item
    On Hybrid Synthesis for Hierarchical Structured Petri Nets
    (1998-10-15) Liu, Hong; Park, Jun-Cheol; Miller, Raymond E.
    We propose a hybrid method for synthesis of hierarchical structured Petri nets. In a top-down manner, we decompose a system into a set of subsystems at each level of abstraction, each of these is specified as a blackbox Petri net that has multiple inputs and outputs. We stipulate that each subsystem satisfies the following I/O constraints: (1) At any instance of time, at most one of the inputs can be activated; and (2) If one input is activated, then the subsystem must consume the input and produce exactly one output within a finite length of time. We give a stepwise refinement procedure which starts from the initial high-level abstraction of the system and expands an internal place of a blackbox Petri net into a more detailed subnet at each step. By enforcing the I/O constraints of each subsystem in each intermediate abstraction, our refinement maintains the sequencing of transitions prescribed by the initial abstraction of the system. Next, for the bottom-up synthesis, we present interconnection rules for sequential, parallel, and loop structures and prove that each rule maintains the I/O constraints. Thus, by incorporating these interconnection rules into our refinement formulation, our approach can be regarded as a hybrid Petri net synthesis technique that employs both top-down and bottom-up methods. The major advantage of the method is that the modeling details can be introduced incrementally and naturally, while the important logical properties of the resulting Petri net are guaranteed.