Abstract: The Petri net theory has been used to specify many types of
   systems, in particular, concurrent, distributed and non-deterministic.
   A class of high-level, object-based Petri nets, OBJSA nets, is being
   used to model the behaviour of a concurrent system - a priority queue.
   We propose a method of analysing its behaviour by examining its
   structure and its underlying subnet components according to the state
   machine paradigm. This is closely related to the liveness and safeness
   analysis of free-choice Elementary Net systems with simple or
   unstructured tokens in existing literature. By using these existing
   results and applying them to OBJSA nets with structured tokens, we are
   able to determine the liveness property of our priority queue example.