# Logic: Kripke structures timed with inequality constraints.

I'm having trouble 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 a clock $$c$$.
I want to define a single atomic proposition. $$p$$ that the labels indicate where the clock is not 0 ($$c neq 0$$).

However, I am struggling to define states and transitions.
My intuition is to create two states. $$s$$, such that $$p notin L (s)$$ Y $$p in L (s & # 39;)$$.
The two states are then connected by a transition of $$(s, epsilon, s & # 39;) in rightarrow$$, such that $$epsilon .

However, when reading publications such as Lepri et.al., it seems that they do not need any $$epsilon$$.

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