Automated Verification of Propositional Agent Abstraction for Classical Planning via CTLK Model Checking
Abstract
Abstraction has long been an effective mechanism to help find a solution in classical planning. Agent abstraction, based on the situation calculus, is a promising explainable framework for agent planning, yet its automation is still far from being tackled. In this paper, we focus on a propositional version of agent abstraction designed for finite-state systems. We investigate the automated verification of the existence of propositional agent abstraction, given a finite-state system and a mapping indicating an abstraction for it. By formalizing sound, complete and deterministic properties of abstractions in a general framework, we show that the verification task can be reduced to the task of model checking against CTLK specifications. We implemented a prototype system, and validated the viability of our approach through experimentation on several domains from classical planning.
Cite
Text
Luo. "Automated Verification of Propositional Agent Abstraction for Classical Planning via CTLK Model Checking." AAAI Conference on Artificial Intelligence, 2023. doi:10.1609/AAAI.V37I5.25796Markdown
[Luo. "Automated Verification of Propositional Agent Abstraction for Classical Planning via CTLK Model Checking." AAAI Conference on Artificial Intelligence, 2023.](https://mlanthology.org/aaai/2023/luo2023aaai-automated/) doi:10.1609/AAAI.V37I5.25796BibTeX
@inproceedings{luo2023aaai-automated,
title = {{Automated Verification of Propositional Agent Abstraction for Classical Planning via CTLK Model Checking}},
author = {Luo, Kailun},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2023},
pages = {6475-6482},
doi = {10.1609/AAAI.V37I5.25796},
url = {https://mlanthology.org/aaai/2023/luo2023aaai-automated/}
}