Download como arquivo ICAL
"Planejamento baseado em Veri cação Simbólica de Modelos"
Segunda-feira 22 Outubro 2018, 09:00
Contato: Este endereço de email está sendo protegido de spambots. Você precisa do JavaScript ativado para vê-lo.

Candidata: Viviana Bonadia dos Santos

 

Orientadora: Profa. Dra. Leliane Nunes de Barros

 

Resumo: Planejamento automatizado em Inteligência Arti cial é a área que estuda o processo
de escolha e organização de ações (síntese de plano) com o objetivo de alcançcar metas
preestabelecidas. Planejamento clássico é uma abordagem de planejamento que faz algumas
suposiçõeses restritivas sobre o ambiente em que o agente atua. Esta abordagem lida
com problemas onde o ambiente é completamente observável, nito, estático e não existe
incerteza sob os efeitos das ações executadas pelo agente. Embora esta seja uma das abordagens
mais estudadas em planejamento, muitos problemas de interesse prático não podem
ser resolvidos, dadas suas suposições demasiadamente restritivas. O Planejamento não determiní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. Uma das principais abordagens para resolver
problemas de planejamento não determinístico é a abordagem baseada em veri cação de
modelos. A maioria dos planejadores que utilizam esta abordagem baseia-se na lógica
temporal de tempo rami cado 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çãoes do
agente, foi proposta uma nova logica, a logica -CTL, e um planejador capaz de resolver
problemas de planejamento n~ao determinsticos pertencentes a classe de problemas FOND
(Fully-Observable Non-Deterministic), chamado Pactl. Neste trabalho de mestrado, temos
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 especi cados como fórmulas lógicas e computacionalmente representados por
meio de diagramas de decisão binária (Binary Decision Diagram - BDD).
Palavras-chave: planejamento não determistico, veri cação de modelos, FOND, BDD.

Local Sala 144 - Bloco B - IME-USP