12.01.2006

Na tropie eksplozji. O agentach i złożoności model checkingu

Temporalna logika agentów ATL pozwala wyrazić fakty na temat strategicznych zdolności agentów: formuła «A»φ mówi, że agent (bądź koalicja agentów) A jest w stanie wymusić temporalną własność φ. Na przykład, «jamesbond»F win oznacza, że agent James Bond ma do dyspozycji strategie, która zapewni mu koniec końców zwycięstwo (prawdziwość tej formuły powinna być oczywista dla każdego, kto kiedykolwiek oglądał filmy o agencie 007). Jedna z najczęściej podkreślanych zalet ATL jest liniowa złożoność model checkingu - liniowa względem wielkości modelu i długości formuły. Tkwi w tym jednak pewien haczyk: otóż wielkość modelu jest zdefiniowana jako ilość *tranzycji*, a nie stanów w systemie. W przypadku zwykłych modeli temporalnych nie stanowiłoby to problemu, gdyż ilość strzałek w grafie nigdy nie przekracza kwadratu ilości węzłów. Niestety, tranzycje w modelach ATL są etykietowane krotkami akcji i okazuje się, że w ogólności jest ich eksponencjalnie wiele w stosunku do ilości agentów. Tak więc, po *niewielkiej* zmianie parametrów wejściowych problemu, mamy do czynienia z eksplozja rozmiaru modelu. Czy złożoność samego model checkingu również eksploduje? O tym chciałbym właśnie opowiedzieć w ramach mego wystąpienia.