20.05.2010

Weryfikacja systemów perswazyjnych

Zaprezentowane zostaną badania dwóch zespołów badawczych:

PERSEUS (http://perseus.ovh.org/) w składzie Katarzyna Budzyńska (UKSW), Magdalena Kacprzak (PB, PJWSTK), Paweł Rembelski (PJWSTK),

L3G (http://l3g.pl/) w składzie: Paweł Garbacz (KUL), Piotr Kulicki (KUL), Marek Lechniak (KUL), Robert Trypuz (KUL).

Wystąpienie poświęcone będzie problemowi analizowania i testowania wieloagentowych systemów perswazyjnych. Poruszone zostaną dwa zagadnienia: budowania modelu systemu oraz jego weryfikacji modelowej.

W logice standardowym sposobem reprezentacji stanów przekonań agentów oraz ich dynamiki są modele w stylu Kripkego ze zdefiniowaną w nich relacją dostępności epistemicznej (określającej co agent uważa za możliwe) i dynamicznej (określającej jak stan agenta może się zmienić pod wpływem interakcji z otoczeniem). Przy rozpatrywaniu nawet prostych scenariuszy, w których ten model miałby być zastosowany taka struktura staje się, ze względu na swoją złożoność, w praktyce trudna do opisania. W referacie przedstawiony zostanie nieco bardziej zwięzły sposób opisu stanów epistemicznych agentów i ich dynamiki odwołujący się do ontologicznie bardziej podstawowych pojęć sytuacji oraz możliwości epistemicznych. Z opisu rzeczywistości w ramach tego modelu daje się automatycznie wygenerować odpowiednią strukturę Kripkowską. Wydaje się, że takie podejście przybliża możliwość praktycznego zastosowania logiki epistemicznej oraz jej informatycznych implementacji.

Struktury Kripkowskie, opisujące systemy realizujące proces perswazji, badamy za pomocą narzędzia o nazwie Perseus. Analiza odbywa się dwutorowo. Z jednej strony Perseus wykorzystuje metody i techniki weryfikacji modelowej, aby sprawdzić czy formuła opisująca wybraną własność systemu jest spełniona w zadanym stanie modelu. Z drugiej strony wykonuje weryfikację parametryczną, tzn. dla zadanego wyrażenia zawierającego niewiadomą poszukuje jej wartości tak by otrzymana formuła była prawdziwa w wybranym stanie modelu. W trakcie wystąpienia przedstawimy formalną bazę dwóch nowych modułów weryfikatora. Pierwszy moduł pozwala na formalną weryfikację własności perswazyjnych systemów dialogowych. Weryfikacja oparta jest na logice akcji i stopniowanych modalności AGn oraz propozycji formalizacji systemów dialogowych zaproponowanych przez H. Prakkena. Drugi moduł jest zaprojektowany do wnioskowania o strategiach w dialogach perswazyjnych. Podejście to jest inspirowane logiką ATL (Alternating-time Temporal Logic). Podobnie jak w logice ATL definiujemy strategię jako funkcję za zbioru wszystkich skończonych legalnych dialogów w zbiór możliwych ruchów. Rozważamy i definiujemy kilka modalności opisujących strategie i ich skuteczność w osiąganiu celu agentów.