2
$\begingroup$

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.

$\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.