Kiedy dwie symulacje nie są bisimulacją?

20

Biorąc pod uwagę oznaczony system przejścia , gdzie jest zbiorem stanów, jest zbiorem etykiet, a jest relacją trójskładnikową. Jak zwykle napisz dla . Oznaczone przejście oznacza, że system w stanie zmienia stan na z etykietą , co oznacza, że to pewne obserwowalne działanie, które powoduje zmianę stanu. $(S,\Lambda,\to)$ $S$ $\Lambda$ $\to\subseteq S\times\Lambda\times S$ $p \stackrel\alpha\rightarrow q$ $(p,\alpha,q)\in\to$ $p\stackrel\alpha\to q$ $p$ $q$ $\alpha$ $\alpha$

Teraz relacja jest nazywana symulacją iff $R \subseteq S \times S$

\forall (p, q) \in R, if p \overset{α}{\to} p^{'} then \exists q^{'}, q \overset{α}{\to} q^{'} and (p^{'}, q^{'}) \in R .

$\forall (p,q)\in R, \text{ if } p \stackrel\alpha\rightarrow p' \text{ then } \exists q', \; q \stackrel\alpha\rightarrow q' \text{ and } (p',q')\in R.$

Mówi się, że jeden LTS symuluje inny, jeśli istnieje między nimi relacja symulacji.

Podobnie relacja jest bisimulacją iff $R \subseteq S \times S$ $\forall (p,q)\in R,$

\begin{array}{l} if p \overset{α}{\to} p^{'} then \exists q^{'}, q \overset{α}{\to} q^{'} and (p^{'}, q^{'}) \in R and \\ if q \overset{α}{\to} q^{'} then \exists p^{'}, p \overset{α}{\to} p^{'} and (p^{'}, q^{'}) \in R . \end{array}

$\begin{array}{l} \text{ if } p \stackrel\alpha\rightarrow p' \text{ then } \exists q', \; q \stackrel\alpha\rightarrow q' \text{ and } (p',q')\in R \text{ and } \\ \text{ if } q \stackrel\alpha\rightarrow q' \text{ then } \exists p', \; p \stackrel\alpha\rightarrow p' \text{ and } (p',q')\in R. \end{array}$

Mówi się, że dwa LTS są bisimilar, jeśli istnieje bisimulacja między ich przestrzeniami stanu.

Oczywiście te dwa pojęcia są dość powiązane, ale nie są takie same.

W jakich warunkach LTS symuluje inny i odwrotnie, ale że oba LTS nie są podobne?

— Dave Clarke
źródło

12

Ponieważ proces CCS jest wart tysiąc pikseli - i łatwo jest zobaczyć leżący u jego podstaw LTS - oto dwa procesy, które symulują się nawzajem, ale nie są podobne:

P = a b + a

$P = ab + a$

Q = a b

$Q = ab$

$\mathcal{R_1}=\{(ab+a, ab), (b, b), (0,b), (0, 0)\}$ to symulacja.

$\mathcal{R_2}=\{(ab, ab+a), (b, b), (0,0)\}$ to symulacja.

$P\ \mathcal R_1\ Q$ i ale i nie są podobne. Dlaczego nie? Ponieważ i jedyne takie, że to ... a nie jest podobne do . $Q\ \mathcal R_2\ P$ $P$ $Q$ $P\stackrel{a}→0$ $Q'$ $Q\stackrel{a}→Q'$ $b$ $0$ $b$

$P$ $Q$ $Q$ $Q$ $P$ $P$ $a$ $Q$ $a$ $\mathcal R$ $\mathcal R$ $\mathcal R^{-1}$

— jmad
źródło

10

$R_1$ $R_2$ $p_1$ $q$ $R_1$ $R_2$

Kanonicznym przykładem są dwa systemy, które mają te same ślady, ale dokonują wyborów inaczej. Rozważmy dwa automaty z napojami: pierwszy (zły) bierze monetę ( c) i niedeterministycznie decyduje, czy podać filiżankę herbaty ( t). Drugi automat (ten dobry) bierze monetę ( c) i podaje filiżankę herbaty ( t).

wczesny i późny wybór

$R_1 = \{(s,s'), (p,p'), (q,q'), (r,p')\}$ $r$ $r$ $p$

$R_2 = \{(s',s),(p',p),(q',q)\}$ $r$ $r$ $s'$ $2$ $s$ $p'$ $s'$ $c$ $p$ $r$ $1$ $p$ $q'$ $q$ $r$

$r$ $r$

Różnica między tymi dwiema maszynami polega na tym, że dobra maszyna jest deterministyczna i (przy założeniu żywotności) zawsze dostarcza herbatę po włożeniu monety, podczas gdy zła maszyna może kapryśnie wziąć monetę, ale utknie, nie mogąc dostarczyć herbaty.

Tego rodzaju różnica pojawia się często w badaniu systemów współbieżnych. Odpowiedź jmada pokazuje proces CCS z tym LTS.

Aby uzyskać więcej informacji na temat bisimulacji, polecam notatki Davide Sangiorgi O początkach bisimulacji i koindukcji . (Jest to ćwiczenie 1, str. 29, a notatki używają tego samego przykładu.)

— Gilles „SO- przestań być zły”
źródło

Fakt, że dwie jednokierunkowe symulacje nie są równe podobieństwu, sugeruje mi, że symulacja nie jest właściwym pomysłem przybliżenia w obecności niedeterminizmu. Czy są jakieś inne pomysły, które zostały wzięte pod uwagę?

— Uday Reddy,

2

$LTS_1$ $LTS_2$ $R$ $LTS_2$ $LTS_1$ $R$ $R$

$LTS_1$ $LTS_2$ $R$ $LTS_2$ $LTS_1$ $R$

— Charles
źródło

Wydaje mi się, że to, co próbuję powiedzieć, to fakt, że zawsze tak jest, że dwa LTS są podobne, więc pytanie dotyczy raczej tego, czy dana relacja jest (bi) symulacją.

— Charles