13.11.2017 - Seminarium Instytutowe - godz. 13:00, Damian Kurpiewski (IPI PAN)
Wystąpienie dotyczyć będzie weryfikacji modelowej zdolności strategicznych przy niepełnej informacji, specyfikowanej w logice ATLir. Jest to trudny problem, którego złożoność rozciąga się od NP-zupełności do nierozstrzygalności, w zależności od szczegółów specyfikacji. Dodatkowo, dla niepełnej informacji nie zachodzą zależności stałopunktowe, co znacząco utrudnia syntezę strategii wygrywających. W wystąpieniu zaprezentuję translację z ATLir do formuł stałopunktowych, zapewniające dolną i górną aproksymację weryfikacji. Rozpocznę od pokazania, dlaczego pierwsze, naiwne podejście nie działa. Następnie zaprezentuję, w jaki sposób może ono zostać zmodyfikowane do osiągnięcia gwarantowanego dolnego ograniczenia. Opowiem także o zmodyfikowanym operatorze następnego kroku, który używany jest w operacjach stałopunktowych. Na sam koniec pokazane zostaną wyniki eksperymentalne.