# Simulation and Bisimulation

gefragt 2017-08-14 18:42:16 +0100

If K1 is over (a,b,c) and K2 is over (a,b).

Suppose there is a state in K1 which has label c (S1), and there is a state in K2 which has label {} (Q2).

We take the intersection of all the state labels from K1 and (a,b){which is K2}.

Suppose we get the result as {} (empty) for this intersection: S1 ∩ {a,b} ({c} ∩ {a,b}).

Now, when we have to do SIM1 for this state, do we consider (S1,Q1) in SIM1?

bearbeiten retag schließen löschen

## 1 Antwort

geantwortet 2017-08-14 20:29:02 +0100

In general, if you want to compute the greatest (bi)simulation relation between two transition systems ${\cal K}_1$ and ${\cal K}_2$ over variables ${\cal V}_1$ and ${\cal V}_2$, respectively, you compute a sequence of relations ${\cal H}_0,{\cal H}_1,\ldots$ that converges towards the desired (bi)simulation relation.

To this end, you start with the greatest relation ${\cal H}_0\subseteq {\cal S}_1\times {\cal S}_2$ such that states $(s_1,s_2)\in{\cal H}_0$ have comparable labels which means that ${\cal H}_0$ contains exactly those pairs of states $(s_1,s_2)\in {\cal S}_1\times {\cal S}_2$ where ${\cal L}_1(s_1)\cap{\cal V}_2 = {\cal L}_2(s_2)\cap{\cal V}_1$ holds. This means that the labels of the states are the same when you only consider the observable variables.

If I understood your example correctly, this means (allow me to rename your state Q2 to $s_2$):

• ${\cal L}_2(s_2)\cap{\cal V}_1 =$ {} $\cap$ {a,b,c} = {}

So, if ${\cal L}_1(s_1)\cap$ {a,b} = {} holds (which is what you assume), then the state pair $(s_1,s_2)$ is contained in ${\cal H}_0$, otherwise, it is not contained there (and thus in none of the other ${\cal H}_i$.

mehr

## Kommentare

So, if there is a state S1 in K1 and labels a,b,c, and there is a state Q1 in K2 with labels a,b. What would happen here? Will (S1, Q1) it be contained in H0?

( 2017-08-14 21:04:40 +0100 )bearbeiten

If the label of S1 in K1 is {c}, and variable c is not known by states in K2 (since K2 is only defined over variables {a,b}), then state Q1 with label {} will be considered (bi)similar to S1 in the initial relation ${\cal H}_0$. So, yes, (S1,Q1) is contained in ${\cal H}_0$ under these conditions.

( 2017-08-14 21:27:02 +0100 )bearbeiten

## Ihre Antwort

Du kannst deinen Eintrag bereits als Gast verfassen. Deine Antwort wird zwischengespeichert, bis du dich eingeloggt oder registriert hast.
Bitte nur konstruktive Antworten auf diese konkrete Frage posten.
Falls du eine Frage stellen willst, dann stelle eine neue Frage.
Für kurze Diskussionen und Nachfragen benutze bitte die Kommentar-Funktion.
Deine Fragen und Antworten kannst du jederzeit nachbearbeiten und verbessern.
Gute Fragen und Antworten kannst du mit einem Upvote oder Downvote bewerten.

Schreibe deine Antwort auf diese Frage

[Vorschau ausblenden]

## Statistik

Gefragt: 2017-08-14 18:42:16 +0100

Gesehen: 49 mal

Letztes Update: Aug 14 '17