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 acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.