• JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
 
  Bookmark and Share
 
 
Thèse de Doctorat
DOI
https://doi.org/10.11606/T.45.2007.tde-09042008-105750
Document
Auteur
Nom complet
Silvio do Lago Pereira
Adresse Mail
Unité de l'USP
Domain de Connaissance
Date de Soutenance
Editeur
São Paulo, 2007
Directeur
Jury
Barros, Leliane Nunes de (Président)
Castilho, Marcos Alexandre
Cozman, Fabio Gagliardi
Finger, Marcelo
Wainer, Jacques
Titre en portugais
Planejamento sob incerteza para metas de alcançabilidade estendidas
Mots-clés en portugais
metas de alcançabilidade estendidas
planejamento sob incerteza
verificação de modelos
Resumé en portugais
Planejamento sob incerteza vem sendo cada vez mais requisitado em aplicações práticas de diversas áreas que eequerem soluções confiáveis para metas complexas. Em vista disso, nos últimos anos, algumas abordagens baseadas no uso de métodos formais para síntese automática de planos têm sido propostas na área de Planejamento em Inteligência Artificial. Entre essas abordagens, planejamento baseado em verificação de modelos tem se mostrado uma opção bastante promissora; entretanto, conforme observamos, a maioria dos trabalhos dentro dessa abordagem baseia-se em CTL e trata apenas problemas de planejamento para metas de alcançabilidade simples (como aquelas consideradas no planejamento clássico). Nessa tese, introduzimos uma classe de metas de planejamento mais expressivas (metas de alcançabilidade estendidas) e mostramos que, para essa classe de metas, a semântica de CTL não é adequada para formalizar algoritmos de síntese (ou validação) de planos. Como forma de contornar essa limitação, propomos uma nova versão de CTL, que denominamos alpha-CTL. Então, a partir da semântica dessa nova lógica, implementamos um verificador de modelos (Vactl), com base no qual implementamos também um planejador (Pactl) capaz de resolver problemas de planejamento para metas de alcançabilidade estendidas, em ambientes não-determinísticos com observabilidade completa. Finalmente, discutimos como garantir a qualidade das soluções quando dispomos de um modelo de ambiente onde as probabilidades das transições causadas pela execução das ações são conhecidas.
Titre en anglais
Planning under uncertainty for extended reachability goals
Mots-clés en anglais
extended reachability goals
model checking
planning under uncertainty
Resumé en anglais
Planning under uncertainty has being increasingly demanded for practical applications in several areas that require reliable solutions for complex goals. In sight of this, in the last few years, some approaches based on formal methods for automatic synthesis of plans have been proposed in the area of Planning in Artificial Intelligence. Among these approaches, planning based on model checking seems to be a very attractive one; however, as we observe, the majority of the works in this approach are mainly based on CTL and deals only with planning problems for simple reachability goals (as those considered in classical planning). In this thesis, we introduce a more expressive class of planning goals (extended reachability goals) and show that, for this class of goals, the CTL's semantics is not adequate to formalize algorithms for synthesis (or validation) of plans. As a way to overcome this limitation, we propose a new version of CTL, called alpha-CTL. Then, based on the semantics of this new logic, we implement a model checker (Vactl), based on which we also implement a planner (Pactl) capable of solving planning problems for extended reachability goals, in nondeterministic planning environments with complete observability. Finally, we discuss how to guarantee the quality of the solutions when we have an environment model where the actions transitions probabilities are known.
 
AVERTISSEMENT - Regarde ce document est soumise à votre acceptation des conditions d'utilisation suivantes:
Ce document est uniquement à des fins privées pour la recherche et l'enseignement. Reproduction à des fins commerciales est interdite. Cette droits couvrent l'ensemble des données sur ce document ainsi que son contenu. Toute utilisation ou de copie de ce document, en totalité ou en partie, doit inclure le nom de l'auteur.
tese.pdf (1.45 Mbytes)
Date de Publication
2008-05-08
 
AVERTISSEMENT: Apprenez ce que sont des œvres dérivées cliquant ici.
Tous droits de la thèse/dissertation appartiennent aux auteurs
CeTI-SC/STI
Bibliothèque Numérique de Thèses et Mémoires de l'USP. Copyright © 2001-2024. Tous droits réservés.