Model-Checking for Ability-Based Logics with Constrained Plans
Authors: Stéphane Demri, Raul Fervari
AAAI 2023 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | 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 abilitybased knowing how logic, for which we show that modelchecking 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 ATLlike logics. We show that for the former logic enriched with budgets, the complexity increases to at least Exp Spacehardness, whereas for the latter, the PTime bound is preserved. Other variant logics are discussed along the paper. |
| Researcher Affiliation | Academia | 1Universit e Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire M ethodes Formelles, 91190, Gif-Sur-Yvette, France 2FAMAF, Universidad Nacional de C ordoba & CONICET, Argentina 3Guangdong Technion Israel Institute of Technology, China |
| Pseudocode | No | The paper describes a 'Check SE' procedure but does not present it as a formal pseudocode or algorithm block. |
| Open Source Code | No | The paper does not mention providing open-source code for the described methodology. |
| Open Datasets | No | The paper is theoretical and does not conduct empirical studies with datasets. |
| Dataset Splits | No | The paper is theoretical and does not conduct empirical studies with datasets requiring training/validation/test splits. |
| Hardware Specification | No | The paper is theoretical and does not involve experimental runs requiring hardware specifications. |
| Software Dependencies | No | The paper is theoretical and does not involve experimental runs requiring specific software dependencies. |
| Experiment Setup | No | The paper is theoretical and does not involve experimental runs requiring detailed setup or hyperparameters. |