Planejamento automatizado em Inteligência Artificial é a área que estuda o processo de escolha e organização de ações (síntese de plano) com o objetivo de alcançar metas preestabelecidas. Planejamento clássico é uma abordagem de planejamento que faz algumas suposições restritivas sobre o ambiente em que o agente atua. Esta abordagem lida com problemas onde o ambiente é completamente observável, finito, estático e não existe incerteza sob os efeitos das ações executadas pelo agente. Embora esta seja urna das abor- dagens mais estudadas em planejarncnto, muitos problemas de interesse prático não podem ser resolvidos, dadas suas suposições demasiadamente restritivas. O Planejarnento não de- terminístico relaxa algumas dessas suposições e considera que pode existir incerteza nos efeitos das ações executadas pelo agente. Isso torna o planejamento não determinístico uma abordagem de maior aplicabilidade prática. Urna das principais abordagens para resolver problemas de planejamento não determinístico é a abordagem baseada em vérificação de modelos. A maioria dos planejadores que utilizam esta abordagem baseia-se na lógica temporal de tempo ramificado CTL. Contudo, esta lógica possui algumas limitações. Para contornar as limitações da lógica CTL, a qual não considera explicitamente as ações do agente, foi proposta uma nova lógica, a lógica a-CTL, e um planejador capaz de resolver problemas de planejamento não determinísticos pertencentes à classe de problemas FOND (Pully-Obseruable Non-Deterministic), chamado PACTL. Neste trabalho de mestrado, te- mos por objetivo estender o planejador PACTL com representações e raciocínio simbólico. Chamamos nosso planejador de PACTL-SYM. No PACTL-SYM, os conjuntos de estados e ações são especificados como fórmulas lógicas e computacionalmente representados por meio de diagramas de decisão binária (Binary Decision Diagram - BDD).

ln Artificial Intelligence automated planning is the area that studies the process of choosing and organizing the actions (plan synthesis) with the objective of achieving pre-established goals. Classical planning is an approach to planning that makes restrictive sup- positions about the environment that the agent works. This approach deals with problems where the environment is completely observable, finite, static and there is no uncertain under the effects of the executed actions by the agent. Even though this is one of the most studied approaches in planning, many problems of practical interest cannot be solved, gi- ven its too restrictive suppositions. The non-deterministic planning relieves some of this suppositions and considers that uncertain can exist in the effects of the actions executed by the agent. It makes non-deterministic planning an approach of higher practical usage. One of the main approaches to solve non-deterministic planning problems is the model checking approach. The majority of the planners that use this approach base itself in the computation tree logic (CTL). This logic has some limitations. To work around the li- mitations of the CTL, that does not explicitly considers the actions of the agent, a new logic was proposed, the a-CTL logic, and a planner capable of solving Fully-Observable Non-Deterministic problems (FOND), called PACTL. This Master Thesis objective is to extend the PACTL planner with representations and symbolic reasoning. Our planner is called PACTL-SYM. ln the PACTL-SYM, the set of states and actions are specified as logical formulas and computationally represented by Binary Decision Diagrams (BDD).