with an abstraction of TPN markings as words over the alphabet $\Sigma {{\overset{\text{\tinydef}}{=}}}2^{P{\times}{[{{c_\mathit{max}}+1}]}}$. Each symbol $X\in\Sigma$ represents the places and integer ages of tokens for a particular fractional value.

\[oneclock:abstr\] Let $M\subseteq P {\times}{{\mathbb R}_{\geq 0}}$ be a marking and let ${{\it frac}(M)} {{\overset{\text{\tinydef}}{=}}}\{{{\it frac}(c)}\mid (p,c)\in M\}$ be the set of fractional clock values that appear in $M$.

Let $S\subset [0,1[$ be a finite set of real numbers with $0\in S$ and ${{\it frac}(M)}\subseteq S$ and let $f_0,f_1,\dots,f_n$, be an enumeration of $S$ so that $f_{i-1} < f_i$ for all $i\le n$. The *$S$-abstraction* of $M$ is $${\mathit{abs}_{S}(M)} {{\overset{\text{\tinydef}}{=}}}x_0x_1\dots x_n \in \Sigma^*$$ where $x_i {{\overset{\text{\tinydef}}{=}}}\{(p,{{\it int}(c)}) \mid (p,c)\in M \land {{\it frac}(c)}=f_i\}$ for all $i\le n$. We simply write ${\mathit{abs}_{}(M)}$ for the shortest abstraction, i.e. with respect to $S=\{0\}\cup{{\it frac}(M)}$.

The abstraction of marking $M = \{(p,2.1),(q,2.2),(p,5.1),(q,5.1)\}$ is ${\mathit{abs}_{}(M)}=\emptyset~\{(p,2),(p,5),(q,5)\}~\{(q,2)\}$. The first symbol is $\emptyset$, because $M$ contains no token with an integer age (i.e., no token whose age has fractional part $0$). The second and third symbols represent sets of tokens with fractional values $0.1$ and $0.2$, respectively.

Clocks with integer values play a special role in the behavior of TPN, because the constants in the transition guards are integers. 