\cup (T \times P)$ is a set of directed arcs, called the flow relation, $R$ is a finite set of labels representing event types, with $\tau \notin R$ is a label representing an invisible action, and $\ell:T\rightarrow R\cup {\tau}$ is a labeling function that assigns a label to each transition.

The state of a Petri net is defined w.r.t. the state that a process instance can be in during its execution. A state of a Petri net is captured by the marking of its places with tokens. In a given state, each place is either empty, or it contains a certain number of tokens. A transition is enabled in a given marking if all places with an outgoing arc to this transitions contain at least one token. Once a transition fires (i.e. is executed), a token is removed from all places with outgoing arcs to the firing transition and a token is put to all places with incoming arcs from the firing transition, leading to a new state.

A marked Petri net is a pair $(N,M)$, where $N=(P,T,F,L,\ell)$ is a labeled Petri net and where $M \in \mathbb{B}(P)$ denotes the marking of $N$. For $n \in (P \cup T)$ we 