transition effects . Its *height* is the maximal effect of any prefix and, similarly, its *depth* is the inverse of the minimal effect of any prefix.

An OCN naturally induces an infinite-state labelled transition system in which each *configuration* is a pair $(s,c)\in \states\x\N$ comprising a state and a non-negative integer. We call such a configuration *final*, or *accepting*, if $s\in F$. Every letter $a\in\alphabet$ induces a step relation $\step{a}~\subseteq (Q\x\N)^2$ between configurations where, for every two configurations $(s,c)$ and $(s',c')$, $$(s,c)\step{a}(s',c') \iff (s,a,d,s')\in\transitions
\quad\text{and }
c'=c+d. $$ A *run* on a word $w=a_1a_2\ldots a_k\in\alphabet^*$ is a path in this induced infinite system; that is, a sequence $\rho=(\initialstate,c_0),(s_1,c_1), (s_2,c_2),\ldots (s_k,c_k)$ such that $(s_{i-1},c_{i-1})\step{a_i}(s_i,c_i)$ holds for all $1\le i\le k$. Naturally, a run uniquely describes a path in the underlying finite OCN. Conversely, for every such path and initial counter value $c_0\in\N$, there is at most one corresponding run: A path $\pi$ is *executable from $c_0$* if its depth is at most $c_0$ (that is, we do not allow the counter to become negative). A run as above is called a (simple) *cycle* if its underlying path is a (simple) cycle. It is *accepting* if it ends in an accepting configuration. 