I want to prove something but I am not sure if it is the right way to do it.

I have two LTS that define different semantics. A=($Q_a,Λ,\to)$, and B=$(Q_b,Λ\cup\{\beta\},\leadsto)$, where $\beta$ is a silent transition. So if I am understanding correctly, to prove that A simulates B through a relation $R_1$,i.e, $AR_1B$ I need to prove that: $\forall (p,q)\in R_1,\forall\sigma\inΛ$ such that $q\overset{\beta^*\sigma\beta^*}{\leadsto}q',\exists p'$ such that $p\overset{\sigma}{\to} p'$and $(p',q')\in R_1$,
and to prove that B simulates A through a relation $R_2$,i.e, $BR_2A$ I need to prove that: $\forall (p,q)\in R_2,\forall\sigma\inΛ$ such that $p\overset{\sigma}{\to}p',\exists q'$ such that $q\overset{\sigma}{\leadsto} q'$ and $(p',q')\in R_1$.

What is confusing me is that the unobservebale actions ($\beta$) appears in one sens and not in the other and I am not sure on which sens I should put them.

Any help would be great.


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.