Thus we always include the fractional part $0$ in the set $S$ in \[oneclock:abstr\].

We use a special kind of regular expressions over $\Sigma$ to represent coverable sets of TPN markings as follows.

\[expression:def\] A regular expression $E$ over $\Sigma$ represents the downward-closed set of TPN markings covered by one that has an abstraction in the language of $E$: $${[\![E]\!]}{{\overset{\text{\tinydef}}{=}}}\{N\mid \exists M \exists S.~
    M\ge N \land {\mathit{abs}_{S}(M)}\in{{\mathcal{L}}{\mathopen{}\mathclose\bgroup\originalleft}(E{\aftergroup\egroup\originalright})}\}.$$

An expression is *simple* if it is of the form $E = x_0x_1\dots x_{k}$ where for all $i\le k$ either $x_i\in\Sigma$ or $x_i={y_i}^*$ for some $y_i\in\Sigma$. In the latter case we say that $x_i$ *carries a star*. That is, a simple expression is free of Boolean combinators and uses only concatenation and Kleene star. We will write $\hat{x}_i$ to denote the symbol in $\Sigma$ at position $i$: it is $x_i$ if $x_i\in\Sigma$ and $y_i$ otherwise.

Notice that for all simple expressions $\alpha,\beta$ so that ${{\lvert\alpha\rvert}}>0$, we have that ${[\![\alpha\emptyset\beta]\!]} ={[\![\alpha\beta]\!]}$. However, unless $\alpha$ has length $0$ or is of the form $\alpha=\emptyset\alpha'$, we have ${[\![\emptyset\alpha]\!]} \neq{[\![\alpha]\!]}$. This is because a marking $M$ that contains a token $(p,c)$ with ${{\it frac}(c)}=0$ has the property that all abstractions ${\mathit{abs}_{S}(M)}=x_0\dots x_k$ of $M$ have $x_0\neq 