language.

A *multiset* over a set $X$ is a function $M:X\to{\mathbb{N}}$. The set ${{X}^\oplus}$ of all (finitely supported) multisets over $X$ is partially ordered pointwise (by $\le$). The multiset union of $M,M'\in{{X}^\oplus}$ is $(M\oplus M')\in{{X}^\oplus}$ with $(M\oplus M')(\alpha){{\overset{\text{\tinydef}}{=}}}M(\alpha)+M'(\alpha)$ for all $\alpha\in X$. If $M\ge M'$ then the multiset difference $(M\ominus M')$ is the unique $M''\in{{X}^\oplus}$ with $M=M'\oplus M''$. We will use a monomial representation and write for example $(\alpha + \beta^3)$ for the multiset $(\alpha\mapsto1, \beta\mapsto 3)$. For a multiset $M$ and a number $m\in{\mathbb{N}}$ we let $m\cdot M$ denote the $m$-fold multiset sum of $M$. We further lift this to sets of numbers and multisets on the obvious fashion, so that in particular ${\mathbb{N}}\cdot S {{\overset{\text{\tinydef}}{=}}}\{n\cdot M\mid n\in {\mathbb{N}}, M\in S\}$.

\[sec:model\] *Timed Petri nets* are place/transition nets where each token carries a real value, sometimes called its *clock value* or *age*. Transition firing depends on there being sufficiently many tokens whose value is in a specified interval. All tokens produced by a transition either have age $0$, or inherit the age of an input-token of the transition. To model time passing, all token ages can advance simultaneously by the same (real-valued) amount.

\[def:MTPN\] A *timed Petri net* (TPN) 