Plan Existence Verification as Symbolic Model Checking
Resumo
Automated Planning is the subarea of AI concerned with the generation of a plan of actions for an agent to achieve its goals. State-of-the-art planning algorithms are based on heuristic search. However, the inexistence of a plan can be a challenge for such planners, since they are not always able to discern the difficulty of finding a solution from its inexistence. The problem of plan existence verification, called planex, is computationally hard. Thus, in 2016, the planning community held for the first time the Unsolvability International Planning Competition (UIPC), which aims to evaluate algorithms on the task of verifying plan existence. The aim of this paper is to propose a new algorithm to solve the planex problem that is based on symbolic model checking approach. The proposed algorithm differs from others based on model checking in two points: (i) it is able to reason about the actions represented in PDDL (Planning Domain Description Language) and; (ii) it is based on the α-CTL logic, whose semantics takes into account the actions responsable for the state transitions. We also evaluate the proposed alorithm over the UIPC planning benchmark problems.
Referências
[Bertoli et al. 2001] Bertoli, P., Cimatti, A., Pistore, M., Roveri, M., and Traverso, P. (2001). Mbp: a model based planner. In Proc. of the IJCAI’01 Workshop on Planning under Uncertainty and Incomplete Information.
[Bryant 1986] Bryant, R. E. (1986). Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput., 35(8):677–691.
[Burch et al. 1992] Burch, J. R., Clarke, E. M., McMillan, K. L., Dill, D. L., and Hwang, L.-J. (1992). Symbolic model checking: 1020 states and beyond. Information and computation, 98(2):142–170.
[Cimatti et al. 2003] Cimatti, A., Pistore, M., Roveri, M., and Traverso, P. (2003). Weak, strong, and strong cyclic planning via symbolic model checking. AI, 147(1-2):35–84.
[Clarke and Emerson 1982] Clarke, E. M. and Emerson, E. A. (1982). Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs, Workshop, pages 52–71, London, UK. Springer-Verlag.
[Edelkamp and Helmert 2001] Edelkamp, S. and Helmert, M. (2001). MIPS: The modelchecking integrated planning system. AI Magazine, 22(3):67.
[Erol et al. 1995] Erol, K., Nau, D. S., and Subrahmanian, V. S. (1995). Complexity, decidability and undecidability results for domain-independent planning. Artificial intelligence, 76(1):75–88.
[Fourman 2000] Fourman, M. P. (2000). Propositional planning. In Proceedings of AIPS-00 Workshop on Model-Theoretic Approaches to Planning, pages 10–17.
[Giunchiglia and Traverso 2000] Giunchiglia, F. and Traverso, P. (2000). Planning as model checking. Recent Advances in AI Planning, pages 1–20.
[Kripke 1963] Kripke, S. (1963). Semantical considerations on modal logic. Acta Philosophica Fennica, 16:83–94.
[McDermott et al. 1998] McDermott, D., Ghallab, M., Howe, A., Knoblock, C., Ram, A., Veloso, M., Weld, D., and Wilkins, D. (1998). Planning domain definition language.
[Menezes 2014] Menezes, M. V. (2014). Mudan¸cas em Problemas de Planejamento sem Solu¸c˜ao. PhD thesis, IME-USP.
[Menezes et al. 2014] Menezes, M. V., Barros, L. N., and Pereira, S. L. (2014). Symbolic regression for non deterministic actions. Learning and Nonlinear Models, pages 98–114.
[Pereira 2007] Pereira, S. L. (2007). Planejamento sob incerteza para metas de alcancabilidade estendidas. PhD thesis, Instituto de Matemática e Estatística da Universidade de S˜ao Paulo.
[Pereira and Barros 2008] Pereira, S. L. and Barros, L. N. (2008). A logic-based agent that plans for extended reachability goals. AAMAS, 16(3):327–344.
[Staalmarck 2003] Staalmarck, G. (2003). Quantified boolean formulas. In Computer Aided Verification International Conference, Trento, Italy, 6-10, 1999, page 23. Springer.
[Torralba 2016] Torralba, A. (2016). Sympa: Symbolic perimeter abstractions for proving unsolvability. Unsolvability IPC: planner abstracts, pages 8–11.
