${\mathcal{N}} = (P,T, {\mathit{Var}}, G, {\mathit{Pre}},{\mathit{Post}})$ consists of finite sets of *places* $P$, *transitions* $T$ and *variables* ${\mathit{Var}}$, as well as functions $G,{\mathit{Pre}},{\mathit{Post}}$ defining transition *guards*, *pre*– and *postconditions*, as follows.

For every transition $t\in T$, the guard $G(t)$ maps variables to (open, half-open or closed) intervals with endpoints in ${\mathbb{N}}\cup\{\infty\}$, restricting which values variables may take. All numbers are encoded in unary. The precondition ${\mathit{Pre}}(t)$ is a finite multiset over $(P{\times}{\mathit{Var}})$. Let ${\mathit{Var}}(t)\subseteq{\mathit{Var}}$ be the subset of variables appearing positively in ${\mathit{Pre}}(t)$. The postcondition ${\mathit{Post}}(t)$ is then a finite multiset over $(P{\times}(\{0\}\cup{\mathit{Var}}(t)))$, specifying the locations and clock values of produced tokens. Here, the symbolic clock value is either $0$ (demanding a reset to age $0$), or a variable that appeared already in the precondition.

A *marking* is a finite multiset over $P{\times}{{\mathbb R}_{\geq 0}}$.

\[ex-mtpn\] The picture below shows a place/transition representation of an TPN with four places and one transition. ${\mathit{Var}}(t)=\{x,y\}$, ${\mathit{Pre}}(t) = (p,x)^2 + (q,y)$, $G(t)(x)=[0,5]$, $G(t)(y)=]1,2]$ and ${\mathit{Post}}(t)= (r,y)^3 + (s,0)$.

\(t) \[transition, label=above:[$t$]{},align=left\] [$0\le x \le 5$\
$1 < y \le 2$ ]{}; (p) \[above left=of t,place, label=left:[$p$]{}\] ; (q) \[below left=of t,place, label=left:[$q$]{}\] ; (r) \[above right=of t,place, label=right:[$r$]{}\] ; (s) \[below right=of t,place, 