Równowa˙zno´s´c modeli CCS

Algebra CCS i jej algebry pochodne dostarczaj ˛a metod do specyfikacji i weryfikacji dy-namiki systemów współbie˙znych. Metody słu˙z ˛ace do oceny równowa˙zno´sci modeli pozwalaj ˛a oceni´c zgodno´s´c modelu traktowanego jako implementacja, z modelem b˛ed ˛acym specyfikacj ˛a rozwa˙zanego systemu współbie˙znego. W przypadku, gdy model jest rozwijany jako ci ˛ag ko-lejnych iteracji, relacje równowa˙zno´sci pozwalaj ˛a na wykazanie równowa˙zno´sci modelu i-tego z modelem i + 1-szym.

Zasadniczym kryterium porównywania agentów w algebrze CCS i algebrach pochodnych jest porównywanie agentów na podstawie ich obserwowalnego zachowania. Istniej ˛a tutaj dwa podstawowe podej´scia. W pierwszym, akcja wewn˛etrzna reprezentowana przez τ jest trakto-wana tak jak ka˙zda inna akcja, w drugim podej´sciu, akcja τ jest traktotrakto-wana jako niewidoczna i porównywane s ˛a tylko akcje obserwowalne z zewn ˛atrz.

Definicja 5. Relacj˛e dwuargumentow ˛a R ⊆ E × E nazywamy siln ˛a bisymulacj ˛a, je˙zeli z tego, ˙ze (E, F ) ∈ R wynika, ˙ze dla wszystkich α ∈ Act, spełnione s ˛a warunki:

(1) E → E^α 0 =⇒ ∃F⁰: F → F^α 0 ∧ (E0, F⁰) ∈ R, (2) F → F^α 0 =⇒ ∃E⁰: E → E^α 0∧ (E0, F⁰) ∈ R.

Powy˙zsza definicja oznacza, ˙ze je˙zeli agent E mo˙ze podj ˛a´c pewn ˛a akcj˛e α, to tak ˛a sam ˛a akcj˛e musi mie´c mo˙zliwo´s´c podj ˛a´c agent F i na odwrót. Ponadto, para wyra˙ze´n otrzymanych

w wyniku wykonania tego samego przej´scia przez oba agenty musi równie˙z nale˙ze´c do rela-cji R. Relacja silnej bisymularela-cji równowa˙zy agenty, które wykazuj ˛a równowa˙zne zachowanie wewn˛etrzne i zewn˛etrzne. Para agentów pozostaj ˛acych w relacji silnej bisymulacji na´sladuje nawzajem swoje zachowanie.

Mo˙zna wykaza´c, ˙ze zło˙zenie i suma dwóch silnych bisymulacji oraz relacja odwrotna do relacji b˛ed ˛acej siln ˛a bisymulacj ˛a, równie˙z s ˛a silnymi bisymulacjami.

Definicja 6. Agenty E i F s ˛a silnie równowa˙zne (E ∼ F ), je˙zeli istnieje silna bisymulacja R taka, ˙ze (E, F ) ∈ R.

Dowodzenie istnienia relacji silnej bisymulacji mi˛edzy dwoma agentami jest realizowane przez analiz˛e ich drzew pochodnych. Rozwa˙zmy agenty A i C zdefiniowane nast˛epuj ˛aco:

A = a.A₁ A1 = c.A B = b.B₁ B₁ = c.B C = a.C₁+ b.C₂ C₁ = b.C₃ C2 = a.C3 C₃ = τ.C (3.23) a a b C3 C1 C2 (A|B)\c a a b (A1|B1)\c (A1|B)\c (A|B1)\c b b C τ τ

Rys. 3.6. Grafy pochodnych dla silnie równowa˙znych agentów

Agenty (A | B)\c i C s ˛a silnie równowa˙zne. Grafy pochodnych dla obu agentów przedsta-wiono na rys. 3.6.

Definicja 7. Relacj˛e R okre´slon ˛a na zbiorze Λ nazywamy kongruencj ˛a, gdy spełnia ona nast˛e-puj ˛ace warunki:

(1) R jest relacj ˛a równowa˙zno´sci;

(2) Je˙zeli E ∈ Λ, E⁰jest podwyra˙zeniem wyra˙zenia E i (E⁰, F⁰) ∈ R, to równie˙z (E, F ) ∈ R, gdzie wyra˙zenie F powstaje z wyra˙zenia E przez podstawienie F⁰ za E⁰.

Twierdzenie 1. Relacja silnej bisymulacji jest relacj ˛a kongruencji.

Z tw. 1 oraz def. 7 wynika, ˙ze po zast ˛apieniu fragmentu wyra˙zenia wyra˙zeniem mu silnie równowa˙znym, otrzymujemy wyra˙zenie silnie równowa˙zne do wyra˙zenia wyj´sciowego.

Niech Act^∗ oznacza zbiór słów nad alfabetem Act i niech t ∈ Act^∗. Symbolem bt ∈ L^∗ (zbiór słów nad alfabetem L) oznaczamy słowo otrzymane z t, z którego usuni˛eto wszystkie wyst ˛apienia symbolu τ . W celu zdefiniowania relacji słabej bisymulacji rozwa˙za si˛e etykieto-wany system przej´s´c:

(E , L^∗, {=⇒ : s ∈ L^{s ∗}}), (3.24) gdzie relacja=⇒ zdefiniowana jest nast˛epuj ˛^s aco:

Definicja 8. Je˙zeli t = α1. . . αn ∈ Act^∗ wówczas E =⇒ E^{t 0}, je´sli: E(−→)^{τ ∗ α}1

−→ (−→)^{τ ∗}. . . (−→)^{τ ∗ α}n

−→ (−→)^{τ ∗}E⁰, (3.25) gdzie (−→)^τ ∗oznacza ci ˛ag (w szczególno´sci pusty) wyst ˛apie´n operacji τ .

Relacje−→,^t =⇒ i^t bt

=⇒, dla t ∈ Act^∗ reprezentuj ˛a pewien ci ˛ag akcji z dokładnie t ˛a sam ˛a obserwowaln ˛a zawarto´sci ˛a jak t, ale z ró˙znymi mo˙zliwo´sciami interwencji akcji τ :

(1) → okre´sla dokładnie ile razy akcja τ pojawia si˛e w t;^t (2) ⇒ okre´sla, ˙ze akcja τ mo˙ze si˛e pojawi´c w t;^t

(3) bt

⇒ nie dostarcza ˙zadnych informacji na temat wyst ˛apie´n akcji τ .

Definicja 9. Relacj˛e dwuargumentow ˛a S ⊆ E ×E nazywamy (słab ˛a) bisymulacj ˛a, je˙zeli z tego, ˙ze (E, F ) ∈ R wynika, ˙ze dla wszystkich α ∈ Act, spełnione s ˛a warunki:

(1) E→ E^α 0 =⇒ ∃F⁰: F αb

⇒ F0 ∧ (E0, F⁰) ∈ S, (2) F → F^α 0 =⇒ ∃E⁰: E αb

⇒ E0∧ (E0, F⁰) ∈ S.

Definicja 10. Agenty E i F s ˛a obserwacyjnie równowa˙zne (E ≈ F ), je˙zeli istnieje bisymulacja S taka, ˙ze (E, F ) ∈ S.

Relacja słabej bisymulacji równowa˙zy agenty, które wykazuj ˛a równowa˙zne zachowanie obserwowalne na zewn ˛atrz. Relacja słabej bisymulacji nie jest relacj ˛a kongruencji.

Rozwa˙zmy agenty C i D zdefiniowane nast˛epuj ˛aco:

C = a.C₁+ b.C₂ C₁ = b.C₃ C₂ = a.C₃ C3 = τ.C D = a.D1+ b.D2 D₁ = b.D D₂ = a.D (3.26) a a b C3 C1 C2 b C τ a D D1 b a D2 b

Rys. 3.7. Grafy pochodnych dla słabo równowa˙znych i obserwacyjnie kongruentnych agentów

Grafy pochodnych dla rozwa˙zanych agentów przedstawiono na rys. 3.7. Agenty C i D s ˛a obserwacyjnie równowa˙zne, ale nie s ˛a silnie równowa˙zne, bo po wykonaniu akcji a i ¯b agent C b˛edzie mógł wykona´c akcj˛e τ , za´s D nie b˛edzie miał takiej mo˙zliwo´sci.

Relacja obserwacyjnej równowa˙zno´sci nie jest relacj ˛a kongruencji co mo˙ze by´c traktowane jako jej wada. Problemem jest tutaj mo˙zliwo´s´c wyst ˛apienia akcji τ jako pierwszej, np agenty a.0 + b.0 i τ.a.0 + b.0 nie s ˛a obserwacyjnie równowa˙zne. Wynika to z faktu, ˙ze po wykonaniu akcji τ drugi z agentów b˛edzie mógł ju˙z wykona´c tylko akcj˛e a, za´s pierwszy ci ˛agle b˛edzie miał wybór mi˛edzy a i b. Dla porównania obserwacyjna równowa˙zno´s´c zachodzi mi˛edzy agentami a.0 + b.0 i a.τ.0 + b.0. Zamiast obserwacyjnej równowa˙zno´sci cz˛esto rozpatruje si˛e relacj˛e obserwacyjnej kongruencji:

Definicja 11. Wyra˙zenia E i F nazywamy obserwowalnie kongruentnymi, E ≈c F , je˙zeli spełnione s ˛a warunki:

(2) E ⇒ E^{τ 0} =⇒ ∃F⁰: F ⇒ F^{τ 0}∧ E⁰ ≈ F⁰, (3) F ⇒ F^τ 0 =⇒ ∃E⁰: E ⇒ E^τ 0∧ E0 ≈ F0.

Twierdzenie 2. Relacja obserwowalnej kongruencji jest relacj ˛a kongruencji.

Ka˙zde dwa agenty, który s ˛a silnie równowa˙zne, s ˛a równie˙z obserwacyjnie kongruentne. Ka˙zde dwa agenty, który s ˛a obserwacyjnie kongruentne, s ˛a równie˙z słabo równowa˙zne. Impli-kacje odwrotne nie s ˛a prawdziwe.

Rozwa˙zane wcze´sniej agenty C i D (zob. (3.26)) s ˛a obserwacyjnie kongruentne. Dla po-równania rozwa˙zny agenty C i D zdefiniowane nast˛epuj ˛aco:

C = a.C₁+ b.C₂ C₁ = b.C₃ C2 = a.C3 C₃ = τ.C D = τ.D1 D₁ = a.D₂+ b.D₃ D2 = b.D D₃ = a.D (3.27) D b a D₂ D₃ D1 a b a a b C3 C1 C2 b C τ τ

Rys. 3.8. Grafy pochodnych dla słabo równowa˙znych agentów

Grafy pochodnych dla rozwa˙zanych agentów przedstawiono na rys. 3.8. Agenty C i D s ˛a słabo równowa˙zne, ale nie s ˛a obserwacyjnie kongruentne.

Warto zwróci´c uwag˛e na jeszcze jeden fakt istotny z punktu widzenia omawianych relacji równowa˙zno´sci. Rozwa˙zmy agenty A i B zdefiniowane nast˛epuj ˛aco:

A = a.A₁ A₁ = b.A₂+ c.A₃ A₂ = 0 A₃ = d.A B = a.B₁+ a.B₃ B₁ = b.B₂ B2 = 0 B₃ = c.B₄ B₄ = d.B (3.28) A a A1 b A2 A3 c d a b d B B1 B2 B4 B3 c a

Rys. 3.9. Grafy pochodnych dla agentów A i B

Grafy pochodnych dla rozwa˙zanych agentów przedstawiono na rys. 3.9. Na przedstawio-ne agenty mo˙zna patrze´c jak na automaty sko´nczoprzedstawio-ne. Z punktu widzenia teorii automatów te dwa automaty s ˛a równowa˙zne, bo akceptuj ˛a ten sam j˛ezyk (opisany wyra˙zeniem regularnym

(acd)^∗ab). Z punktu widzenia omawianych w tym podrozdziale relacji, agenty te nie s ˛a nawet obserwacyjnie równowa˙zne.

Relacje pozwalaj ˛ace porównywa´c agenty definiowane s ˛a równie˙z dla algebry TCCS. Pod-stawowa ró˙znica dotyczy tutaj uwzgl˛ednienie zmian stanu agenta w wyniku upływu czasu, np. relacja czasowej bisymulacji definiowana jest nast˛epuj ˛aco:

Definicja 12. Relacj˛e dwuargumentow ˛a R ⊆ E^T× ET nazywamy czasow ˛a bisymulacj ˛a je˙zeli z tego, ˙ze (E, F ) ∈ R wynika, ˙ze dla wszystkich akcji α i opó´znie´n t, spełnione s ˛a warunki: (1) E→ E^α 0 =⇒ ∃F⁰: F → F^α 0 ∧ (E0, F⁰) ∈ R,

(2) F → F^α 0 =⇒ ∃E⁰: E → E^α 0∧ (E0, F⁰) ∈ R, (3) E E^{t 0} =⇒ ∃F⁰: F F^{t 0} ∧ (E0, F⁰) ∈ R, (4) F F^{t 0} =⇒ ∃E⁰: E E^{t 0}∧ (E0, F⁰) ∈ R.

Przedstawiona definicja okre´sla siln ˛a czasow ˛a bisymulacj˛e. Mo˙zna zdefiniowa´c równie˙z słab ˛a czasow ˛a bisymulacj˛ei czasow ˛a obserwowaln ˛a równowa˙zno´s´c.

Na podstawie formalnych definicji bisymulacji wyprowadzono szereg praw (twierdze´n), które mo˙zna stosowa´c do wykazania, ˙ze dwa ró˙zne modele tego samego systemu s ˛a w rzeczy-wisto´sci równowa˙zne przy okre´slonej relacji równowa˙zno´sci. Wi˛ecej informacji na ten temat mo˙zna znale´z´c w monografiach [26, 57].

W celu przedstawienia przykładu zastosowania omawianych relacji porównywania agen-tów, rozwa˙zny model systemu sygnalizacji ´swietnej dla skrzy˙zowania przedstawionego na rys. 3.10. minor road sensor lights 2 1 1 major road

Rys. 3.10. Model skrzy˙zowania

W systemie tym domy´slnie sygnał zielony jest wy´swietlany dla drogi nr 1. Przeł ˛aczenie stanu sygnalizacji nast˛epuje w wyniku zbudzenia sensora (w modelu jest to reprezentowane przez akcj˛e press). Przyjmijmy nast˛epuj ˛ace oznaczenia akcji: l2Ron – wł ˛aczenie sygnału czerwonego na sygnalizatorze L2, l1Goff – wył ˛aczenie sygnału zielonego na sygnalizatorze L1itd. Traktuj ˛ac system jako cało´s´c, jego specyfikacj˛e mo˙zna przedstawi´c jak na listingu 3.4.

agent Lights1 = start.l2Ron.l1Gon.L;

agent L = press.l1Goff.l1Ron.l2Roff

.l2Gon.l2Goff.l2Ron.l1Roff.l1Gon.L;

Listing 3.4. Model systemu sygnalizacji ´swietlnej dla skrzy˙zowania z Rys. 3.10 – definicje agentów

Z drugiej strony, w systemie tym mo˙zna wyró˙zni´c elementy składowe: sensor i dwa sygna-lizatory. Mo˙zna wi˛ec zdefiniowa´c trzy agenty, a nast˛epnie u˙zy´c operatora zło˙zenia, aby stanowi-ły one jeden system. Uwzgl˛edniaj ˛ac dodatkowe wewn˛etrzne akcje niezb˛edne do synchronizacji poszczególnych agentów, system mo˙zna opisa´c jak na listingu 3.5.

agent StartSensor = reset.Sensor;

agent Sensor = press.’signal.reset.Sensor;

agent StartL1 = start.’synch1.synch2.l1Gon.’reset.L1;

agent L1 = signal.l1Goff.l1Ron.’l1.l2.l1Roff.l1Gon.’reset.L1;

agent StartL2 = synch1.l2Ron.’synch2.L2;

agent L2 = l1.l2Roff.l2Gon.l2Goff.l2Ron.’l2.L2;

set S = {l1, l2, signal, synch1, synch2, reset};

agent Lights2 = (StartL1|StartL2|StartSensor)\S;

Listing 3.5. Model systemu sygnalizacji ´swietlnej dla skrzy˙zowania z Rys. 3.10 – wersja rozbudowana

Stosuj ˛ac przedstawione w tym podrozdziale poj˛ecia mo˙zna wykaza´c, ˙ze agenty Lights1 i Lights2 s ˛a obserwowalnie kongruentne. Modele te nie s ˛a silnie równowa˙zne, gdy˙z wy-kazuj ˛a odmienne zachowanie wewn˛etrzne. Bior ˛ac jednak pod uwag˛e fakt, ˙ze akcje nale˙z ˛ace do zbioru S nie s ˛a widoczne z zewn ˛atrz, oba modele z punktu widzenia ich otoczenia zachowuj ˛a si˛e podobnie. Oba modele przedstawiono w formacie akceptowanym przez CWB, co pozwala na automatyczne sprawdzenie, ˙ze mi˛edzy modelami zachodzi wspomniana relacja. W analogiczny sposób mo˙zna konstruowa´c kolejne iteracje rozwijanego systemu i weryfikowa´c ich zgodno´s´c z modelem z poprzedniego etapu.