16.11.2006

Problem efektywności weryfikacji modelowej dynamiczno-strukturalnych własności mobilnych agentów

W pracy [1] przestawiono pojęcie hipersieci - wizualnego modelu działania mobilnych agentów. Jednym z podstawowych założeń jest, że w hipersieciach agenci zorganizowani są w sposób hierarchiczny: jeden manipuluje drugim, podczas gdy sam może być manipulowany przez trzeciego. Skutkuje to drzewiasta; struktura; podległości. Własności hipersieci opisywać można przy pomocy formuł zaproponowanej w [2] logiki CTL^2.
Jest to logika posiadająca operatory modalne dwojakiego rodzaju: - strukturalne, te wypowiadają się na temat położenia danego agenta w hierarchii - dynamiczne, te opisują możliwe ewolucje danego systemu w czasie. Logika ta ma tak samo złożony problem weryfikacji modelowej jak CTL względem zwykłych modeli Kripkego. W szczególności jest liniowa względem wielkości przestrzeni stanów osiągalnych w hipersieci. Jest to ZŁA wiadomość, bo hipersieć złożona z N agentów moze miec N^N osiągalnych stanów.
W ramach seminarium nie przedstawię gotowych wyników mówiących, że tak źle jednak nie jest. Opowiem raczej o swoich nadziejach na zmniejszenie wielkości tej struktury w oparciu o:
- symetrie między agentami oraz
- odpowiednią adaptację pojęcia bisymulacji.

[1] M. A. Bednarczyk, L. Bernardinello, W. Pawłowski, L. Pomello Modelling mobility with Petri Hypernets J. L. Fiadeiro, et al.~(Eds), Recent Trends in Algebraic Development Techniques, 17th International Workshop, WADT 2004, Barcelona, Spain, March 27-30, 2004, Revised Selected Papers. LNCS, {\bf3423}, 28-44, Springer-Verlag, 2005.
[2] Marek A. Bednarczyk, Wojciech Jamroga, Wiesław Pawłowski Expressing and verifying temporal and structural properties of mobile agents Fundamenta Informaticae, IOS Press, 72, 51-63, 2006.