Planejamento baseado em verificação simbólica de modelos

• Ano de defesa: 2018
• Autor(a) principal: Santos, Viviane Bonadia dos
• Tipo de documento: Dissertação
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: Biblioteca Digitais de Teses e Dissertações da USP
• Palavras-chave em Português: Inteligência Artificial
• Link de acesso: https://teses.usp.br/teses/disponiveis/45/45134/tde-20230727-113624/

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).