# Timed Kripke structures with inequality constraints

I am having problems creating a timed Kripke structure $$\mathcal{TK} = \langle S, \mathcal{T}, \rightarrow, L \rangle$$ for a system that I have. My system, a timed automaton system (time base $$\mathcal{T} =\mathbb{R}^+$$) has one clock $$c$$. I want to define one single atomic proposition $$p$$ that labels states where the clock is not 0 ($$c \neq 0$$).

However, I am struggling to define the states and transitions. My intuition is to create two states $$s$$, such that $$p \notin L(s)$$ and $$p \in L(s')$$. The two states are then connected using a transition of $$(s, \epsilon, s') \in \rightarrow$$, such that $$\epsilon < r, \forall r \in \mathbb{R}^{+}$$.

However, when reading publications such as Lepri et.al., they don't seem to have the need for any $$\epsilon$$.

Can somebody explain why they do not need such transitions, or is it impossible for them to express such structures?