Underapproximating ATL with Imperfect Information and Imperfect Recall

• Autorzy: Jamroga W. , Knapik M.

Warianty tytułu

PL

[Dolna Aproksymacja Bezpamięciowego ATL o Niepełnej Informacji]

• Języki publikacji: EN

Abstrakty

EN

We investigate the correspondence between model checking of af-AMCi and ATLir , on the example of reachability. We identify some of the reasons for the fact that these logics are of uncomparable expressivity. These observations form the basis for a novel method for underapproximating ATLir by means of fixed-point calculations. We introduce a special version of the next-step operator, called Persistent Imperfect Next-Step Operator h_iF and show how it can be used to define a new version of reachability that carries to ATLir.

PL

W pracy badane są związki pomiędzy weryfikacją modelową Bezpamięciowej Logiki Temporalnej Czasu Alternującego z Niepełną Informacją ATLir i Epistemicznego Alternującego Mu-Rachunku af-AMCi. Jak pokazano, naturalne uogólnienia pojęcia osiągalności z ATLir -a do af-AMCi nie przynoszą dobrych efektów: osiągalność w af-AMCi nie pociąga za sobą osiągalności w ATLir . Po zidentyfikowaniu części powodów, dla których tak się dzieje, zaproponowano nową wersję operatora następnego kroku, który pozwala na przybliżanie osiągalności w ATLir przy pomocy obliczeń stałopunktowych.

Słowa kluczowe

EN

ATL; model checking; approximation

PL

ATL; weryfikacja; aproksymacja

• Wydawca: Instytut Podstaw Informatyki PAN
• Czasopismo: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
• Rocznik: 2015
• Tom: Nr 1032
• Strony: 1--16
• Opis fizyczny: Bibliogr. 7 poz., rys.

Twórcy

autor

Jamroga W.

• Instytut Podstaw Informatyki PAN, ul. Jana Kazimierza 5, 01-248 Warszawa, Polskamknapi

autor

Knapik M.

• Instytut Podstaw Informatyki PAN, ul. Jana Kazimierza 5, 01-248 Warszawa, Polska

Bibliografia

• [1] R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672-713. 2002.
• [2] R. Bordini, M. Fisher, C. Pardavila, and M. Wooldridge. Model checking agentspeak. In Proc. of the 2nd Int. Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS'03), pages 409-416. ACM, 2003.
• [3] N. Bulling and W. Jamroga. Alternating epistemic mu-calculus. In Proc. of the 22nd Int. Joint Conf. on Artificial Intelligence, IJCAI, pages 109-114. IJCAI/AAAI. 2011.
• [4] R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning About Knowledge. MIT Press, 1995.
• [5] P. Gammie and R. Meyden. MCK: Model checking the logic of knowledge. In Proc. of the 16th Int. Conf. on Computer Aided Verification (CAV'04), volume 3114 of LNCS, pages 479-483. Springer-Verlag, 2004.
• [6] A. Lomuscio. H. Qu. and F. Raimondi. MCMAS: A model checker for the verification of multi-agent systems. In Proc. of 21st International Conference on Computer Aided Verification (CAV'09), volume 5643 of LNCS, pages 682-688. Springer. 2009.
• [7] P. Schobbens. Alternating-time logic with imperfect recall. Electr. Notes Theor. Comput. Sci., 85(2):82-93, 2004.