Virtual First-Order Structure

Abstract

The proof of liveness for various new classes of nets is not intuitive and rather hard to understand. We propose to find the maximum class, called non-virtual-net (NV-net) that are live as long as all minimal siphons never get empty of tokens and the maximum class, called virtual-net (V-net) that may be weakly live if all minimal siphons never get empty of tokens. In the future, when a new system is developed, if it is an NV-net, then it is live as long as no siphons ever get empty. We show that weakly liveness is closely related to a structure called Virtual First Order Structure. We show that both Synchronized Choice Net and Extended Synchronized Choice Net belong to non-virtual-net.