The asynchronous stack revisited

Protocols return often to a particular state - no matter what happens. We call such a state a (em ground state). Each action which occurs in the ground state starts a so-called (em round). A round ends when the ground state is reached again. In distributed protocols without global control, rounds are hard to identify.Ground states might be only virtual snapshots and not necessarily observable. When partial order semantics are considered, a round can be clearly identified even in a distributed system. We will discuss the use of rounds for structuring and verifying a system's behavior. As an example a Petri net model for the asynchronous stack is introduced.