4.01.2006

Modularne systemy interpretowane

O modelach Kripkego twierdzi się, ze nie są "ugruntowane", tzn. odległość pomiędzy modelem a dziedziną problemu jest dość spora. W rezultacie, nie zawsze jest jasne jak taki model miałby wyglądać dla konkretnego, rzeczywistego systemu. Jako alternatywę podaje się zazwyczaj systemy interpretowane Fagina, Halperna i spółki, gdzie przestrzeń globalnych stanów systemu jest zadana w naturalny (i modularny) sposób, jako produkt lokalnych stanów agentów/procesów. Z drugiej strony, tranzycje w systemach interpretowanych są wyłącznie GLOBALNE, co powoduje, ze modularność systemów interpretowanych jest cokolwiek iluzoryczna. Na drugim końcu mamy formalizmy typu programy współbieżne, czy proste moduły reaktywne, które modelują wyłącznie - lub prawie wyłącznie - lokalne tranzycje. Takie podejście z kolei nie pozwala na modelowanie wielu naturalnych zjawisk związanych z interakcja agentów. W pracy, o której chce opowiedzieć, proponujemy klasę reprezentacji opartych na systemach interpretowanych, w których ewolucja systemu i interakcja agentów może być również potraktowana w sposób modularny. Opowiem również o dość zaskakującym wyniku, związanym ze złożonością weryfikacji modelowej dla tej nowej klasy reprezentacji.