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?


Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.