Model-Checking for Ability-Based Logics with Constrained Plans

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.

Authors

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

Keywords

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