Planejamento baseado em verificação simbólica de modelos (2018)
- Authors:
- Autor USP: SANTOS, VIVIANE MELLO BONADIA DOS - IME
- Unidade: IME
- Sigla do Departamento: MAC
- DOI: 10.11606/D.45.2018.tde-20230727-113624
- Assunto: INTELIGÊNCIA ARTIFICIAL
- Agências de fomento:
- Language: Português
- Abstract: 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).
- Imprenta:
- Data da defesa: 22.10.2018
- Status:
- Artigo publicado em periódico de acesso aberto (Gold Open Access)
- Versão do Documento:
- Versão publicada (Published version)
- Acessar versão aberta:
-
ABNT
SANTOS, Viviane Bonadia dos. Planejamento baseado em verificação simbólica de modelos. 2018. Dissertação (Mestrado) – Universidade de São Paulo, São Paulo, 2018. Disponível em: https://teses.usp.br/teses/disponiveis/45/45134/tde-20230727-113624/. Acesso em: 07 maio 2026. -
APA
Santos, V. B. dos. (2018). Planejamento baseado em verificação simbólica de modelos (Dissertação (Mestrado). Universidade de São Paulo, São Paulo. Recuperado de https://teses.usp.br/teses/disponiveis/45/45134/tde-20230727-113624/ -
NLM
Santos VB dos. Planejamento baseado em verificação simbólica de modelos [Internet]. 2018 ;[citado 2026 maio 07 ] Available from: https://teses.usp.br/teses/disponiveis/45/45134/tde-20230727-113624/ -
Vancouver
Santos VB dos. Planejamento baseado em verificação simbólica de modelos [Internet]. 2018 ;[citado 2026 maio 07 ] Available from: https://teses.usp.br/teses/disponiveis/45/45134/tde-20230727-113624/
Informações sobre a disponibilidade de versões do artigo em acesso aberto coletadas automaticamente via oaDOI API (Unpaywall).
Por se tratar de integração com serviço externo, podem existir diferentes versões do trabalho (como preprints ou postprints), que podem diferir da versão publicada.
How to cite
A citação é gerada automaticamente e pode não estar totalmente de acordo com as normas
