A formal semantics for concurrent systems with a priority relation

A formal semantics for the COSY path expressions with a priority relation is proposed. It turns out that in the general case the full aspects of behaviours of systems specified by such expressions cannot be modeled by vector firing sequences (a standard semantics for the case without priorities), although vector firing sequences (but without interpretation as causality relations) can correctly be extended for expressions with priorities, and some (but not all) aspects of behaviours, like deadlockfreeness and adaquacy properties, can be defined in terms of vector firing sequences. To describe the behaviours of the COSY priority path expressions entirely, a new semantics, called the multiple firing sequence semantics, is introduced and some its properties are proved.