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.
Cite
Text
Demri and Fervari. "Model-Checking for Ability-Based Logics with Constrained Plans." AAAI Conference on Artificial Intelligence, 2023. doi:10.1609/AAAI.V37I5.25776Markdown
[Demri and Fervari. "Model-Checking for Ability-Based Logics with Constrained Plans." AAAI Conference on Artificial Intelligence, 2023.](https://mlanthology.org/aaai/2023/demri2023aaai-model/) doi:10.1609/AAAI.V37I5.25776BibTeX
@inproceedings{demri2023aaai-model,
title = {{Model-Checking for Ability-Based Logics with Constrained Plans}},
author = {Demri, Stéphane and Fervari, Raul},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2023},
pages = {6305-6312},
doi = {10.1609/AAAI.V37I5.25776},
url = {https://mlanthology.org/aaai/2023/demri2023aaai-model/}
}