sequentially. Then every marking can be abstracted into a string where all the tokens with the $i$-th fractional clock value are encoded in the $i$-th symbol in the string. Since token multiplicities do not matter for existential coverability, the alphabet from which these strings are built is finite. The primary difficulty is that the length of these strings can grow dynamically as the system evolves, i.e., the space of these strings is still infinite for a given TPN. We perform a forward exploration of the space of reachable strings. By using an acceleration technique, we can effectively construct a symbolic representation of the set of reachable strings in terms of finitely many regular expressions. Finally, we can check existential coverability by using this symbolic representation.

Timed Petri Nets
================

We use ${{\mathbb N}}$ and ${{\mathbb R}_{\geq 0}}$ to denote the sets of nonnegative integers and reals, respectively. For $n\in{{\mathbb N}}$ we write ${[{n}]}$ for the set ${{\mathopen{}\mathclose\bgroup\originalleft}\{0,\ldots,n{\aftergroup\egroup\originalright}\}}$.

For a set ${{\it A}}$, we use ${{{{\it A}}}^*}$ to denote the set of words, i.e. finite sequences, over ${{\it A}}$, and write ${\varepsilon}$ for the empty word. If $R$ is a regular expression over ${{\it A}}$ then ${{\mathcal{L}}{\mathopen{}\mathclose\bgroup\originalleft}(R{\aftergroup\egroup\originalright})}\subseteq {{\it A}}^*$ denotes its 