Model-Checking for Ability-Based Logics with Constrained Plans


  • Stéphane Demri CNRS, LMF, ENS Paris-Saclay, France
  • Raul Fervari Universidad Nacional de Córdoba and CONICET, Argentina GTIIT, China



KRR: Computational Complexity of Reasoning, KRR: Action, Change, and Causality, KRR: Knowledge Representation Languages, KRR: Other Foundations of Knowledge Representation & Reasoning, KRR: Reasoning with Beliefs


We investigate the complexity of the model-checking problem for a family of modal logics capturing the notion of “knowing how”. We consider the most standard ability-based knowing how logic, for which we show that model-checking is PSpace-complete. By contrast, a multi-agent variant based on an uncertainty relation between plans in which uncertainty is encoded by a regular language, is shown to admit a PTime model-checking problem. We extend with budgets the above-mentioned ability-logics, as done for ATL-like logics. We show that for the former logic enriched with budgets, the complexity increases to at least ExpSpace-hardness, whereas for the latter, the PTime bound is preserved. Other variant logics are discussed along the paper.




How to Cite

Demri, S., & Fervari, R. (2023). Model-Checking for Ability-Based Logics with Constrained Plans. Proceedings of the AAAI Conference on Artificial Intelligence, 37(5), 6305-6312.



AAAI Technical Track on Knowledge Representation and Reasoning