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.
BibTeX
@article{Luo_2023, title={Automated Verification of Propositional Agent Abstraction for Classical Planning via CTLK Model Checking}, volume={37}, url={https://ojs.aaai.org/index.php/AAAI/article/view/25796}, DOI={10.1609/aaai.v37i5.25796}, abstractNote={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.}, number={5}, journal={Proceedings of the AAAI Conference on Artificial Intelligence}, author={Luo, Kailun}, year={2023}, month={Jun.}, pages={6475-6482} }