Automated Verification of Propositional Agent Abstraction for Classical Planning via CTLK Model Checking
Keywords:KRR: Action, Change, and Causality, PRS: Other Foundations of Planning, Routing & Scheduling
AbstractAbstraction 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.
How to Cite
Luo, K. (2023). Automated Verification of Propositional Agent Abstraction for Classical Planning via CTLK Model Checking. Proceedings of the AAAI Conference on Artificial Intelligence, 37(5), 6475-6482. https://doi.org/10.1609/aaai.v37i5.25796
AAAI Technical Track on Knowledge Representation and Reasoning