1. Benefits -- provide means for reasoning about the proving properties on the specifications and to assess whether certain desired properties hold or not.

      2. 'good properties' of Petri net are:
       

        a. liveness -- no dead branch in the system.

        b. Boundedness -- the marking of each place never exceeds k tokens,for some k.

        c. Reversibility -- it is always possible to find a sequence of action that will set the system back in its initial state.


      3. Input-based properties -- guarantee that the sequence of events that are requested ( or expected ) are legal with respect to the behaviour of the input devices that produce these events.

      4. Output-based properties

        a. Observability -- all relevant information potentially available to the user.