AAAI 2023technical4 citations
Model-Checking for Ability-Based Logics with Constrained Plans
Abstract
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.
BibTeX
@article{Demri_Fervari_2023, title={Model-Checking for Ability-Based Logics with Constrained Plans}, volume={37}, url={https://ojs.aaai.org/index.php/AAAI/article/view/25776}, DOI={10.1609/aaai.v37i5.25776}, abstractNote={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.}, number={5}, journal={Proceedings of the AAAI Conference on Artificial Intelligence}, author={Demri, Stéphane and Fervari, Raul}, year={2023}, month={Jun.}, pages={6305-6312} }