Return to search

Verificação formal de planos para agentes autônomos e sistemas multiagentes: um estudo de caso aplicado ao futebol de robôs

Submitted by Kleber Silva (kleberbs@ufba.br) on 2017-02-06T17:13:39Z
No. of bitstreams: 1
Rui Carlos Botelho Almeida da Silva.pdf: 4302637 bytes, checksum: 7c1d3de5fed3e9f33254bdc62e656a3a (MD5) / Approved for entry into archive by Vanessa Reis (vanessa.jamile@ufba.br) on 2017-02-07T12:02:49Z (GMT) No. of bitstreams: 1
Rui Carlos Botelho Almeida da Silva.pdf: 4302637 bytes, checksum: 7c1d3de5fed3e9f33254bdc62e656a3a (MD5) / Made available in DSpace on 2017-02-07T12:02:49Z (GMT). No. of bitstreams: 1
Rui Carlos Botelho Almeida da Silva.pdf: 4302637 bytes, checksum: 7c1d3de5fed3e9f33254bdc62e656a3a (MD5) / Os Agentes Autônomos – AA e os Sistemas Multiagentes – SMA realizam suas tarefas
baseados num planejamento e a sua complexidade vai depender de qual ambiente esteja
envolvido, principalmente quando este ambiente é dinâmico e não determinista.
A verificação de modelos tem sido aplicada para a verificação de propriedades do
planejamento de modo a checar a correção de aplicações baseadas em AAs e SMA’s e tal
verificação apresenta muitos desafios para contornar situações potenciais de explosão de
estados. O futebol de robôs simulados é uma aplicação que apresenta muitas das
características e problemas inerentes aos AA’s e SMA’s como um ambiente não
determinista e dinâmico, fato este que vem tornando esta aplicação um relevante estudo de
caso para a verificação de modelos de SMA’s.
O presente trabalho considera a especificação e verificação de planos de um time de futebol
de robôs simulado, o qual é baseado na arquitetura multicamada de Agentes
Concorrentes(camada cognitiva, camada instintiva, e camada reativa), utilizando o
verificador de modelos UPPAAL.
Para atingir os objetivos do trabalho foi proposta uma abordagem incremental e evolutiva
para modelar e verificar os planos, a qual inclui abstrações e técnicas baseadas em
verificação composicional de modelos (Compositional Model Checking), com o objetivo de
contornar situações de explosão de estados. O método proposto também pode ser utilizado
em aplicações similares, o qual poderia ser suportado por um ambiente computacional
interativo para guiar os analistas no processo de verificação de planos de SMA’s com
arquitetura multicamada, usando a verificação de modelos.

Identiferoai:union.ndltd.org:IBICT/oai:192.168.11:11:ri/21342
Date09 March 2012
CreatorsSilva, Rui Carlos Botelho Almeida da
ContributorsAndrade, Aline Maria Santos, Andrade, Aline Mari aSantos, Silva, Flavio Morais de Assis, Deharbe, David Boris Paul
PublisherInstituto de Matemática, Programa de Pós-graduação em Mecatrônica, UFBA, brasil
Source SetsIBICT Brazilian ETDs
LanguagePortuguese
Detected LanguagePortuguese
Typeinfo:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis
Sourcereponame:Repositório Institucional da UFBA, instname:Universidade Federal da Bahia, instacron:UFBA
Rightsinfo:eu-repo/semantics/openAccess

Page generated in 0.0019 seconds