Aplicação de Busca Bidirecional em Planejamento como Verificação Simbólica de Modelos

Abstract

Automated Planning is a subarea of Artificial Intelligence that aims to choose actions from an intelligent agent to achieve a goal. One solution to a planning problem is a sequence of actions (plan), which takes the agent from an initial state to a state that satisfies the goal. When there is no plan that achieves a goal state, it is said that this problem has no solution. The search for a plan can be done in three ways: (i) progressive, from the initial state, trying to reach some state that meets the goal; (ii) regressive, from the set of states that satisfy the goal, trying to reach the initial state e; finally, (iii) bidirectional, simultaneously executing the progressive and regressive searches and trying to reach a common point between these searches. The algorithms reasoned about symbolic models and were implemented using Binary Decision Diagrams. This work proposes the implementation and incorporation of the bidirectional symbolic search in the planning framework with symbolic verification of models, and the performance of tests in planning domains of classic track and track unsolvability.