0
$\begingroup$

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?

$\endgroup$

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.