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 <r, forall r in mathbb {R} ^ {+} $.

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?