The model-checking problem for Resource Agent Logic is known to be undecidable. We review existing (un)decidability results and identify a significant fragment of the logic for which model checking is decidable. We discuss aspects which makes model checking decidable and prove undecidability of two open fragments over a class of models in which agents always have a choice of doing nothing. We also discuss the effect of structures where each agent always has an option of choosing an action that does not produce or consume resources on the decidability.
|Title of host publication||Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015)|
|Editors||Qiang Yang, Michael Wooldridge|
|Place of Publication||Palo Alto|
|Publisher||AAAI Press / International Joint Conferences on Artificial Intelligence|
|Publication status||Published - 2015|
|Event||International Joint Conference on Artificial Intelligence - Buenos Aires, Argentina|
Duration: 25 Jul 2015 → 31 Jul 2015
|Conference||International Joint Conference on Artificial Intelligence|
|Period||25/07/15 → 31/07/15|
Bibliographical noteThe full text is available from: http://ijcai.org/Proceedings/15/Papers/214.pdf
Alechina, N., Bulling, N., Logan, B., & Nguyen, H. N. (2015). On the Boundary of (Un)decidability: Decidable Model-Checking for a Fragment of Resource Agent Logic. In Q. Yang, & M. Wooldridge (Eds.), Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015) (pp. 1494-1501). Palo Alto: AAAI Press / International Joint Conferences on Artificial Intelligence.