Submitted by Fabio Sobreira Campos da Costa (fabio.sobreira@ufpe.br) on 2017-08-23T12:48:01Z
No. of bitstreams: 2
license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5)
dissertacao_mestrado_rafael_araujo.pdf: 1319314 bytes, checksum: 15854b595d618c609a911b95573a01ad (MD5) / Made available in DSpace on 2017-08-23T12:48:01Z (GMT). No. of bitstreams: 2
license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5)
dissertacao_mestrado_rafael_araujo.pdf: 1319314 bytes, checksum: 15854b595d618c609a911b95573a01ad (MD5)
Previous issue date: 2016-09-15 / Robots are increasingly being used in industry and starting their way to our homes as
well. Nonetheless, the most frequently used techniques to analyze robots motion are based
on simulations or statistical experiments made from filming robots’ movements. In this
work we propose an alternative way of performing such analysis by using Probabilistic
Model Checking with the language and tool PRISM. With PRISM we can perform
simulations as well as check exhaustively whether a robot motion planning satisfies specific
Probabilistic Temporal formulas. Therefore we can measure energy consumption, time to
complete missions, etc., and all of these in terms of specific motion planning algorithms.
As consequence we can also determine if an algorithm is superior to another in certain
metrics. Furthermore, to ease the use of our work, we hide the PRISM syntax by proposing
a more user-friendly DSL. As a consequence, we created a translator from the DSL to
PRISM by implementing the translation rules and also, a preliminary investigation about
its relative completeness by using the grammatical elements generation tool LGen. We
illustrate those ideas with motion planning algorithms for home cleaning robots. / Robôs estão sendo cada vez mais utilizados na indústria e entrando em nossas casas também.
No entanto, as técnicas mais frequentemente utilizadas para analisar a movimentação
dos robôs são baseadas em simulações ou experimentos estatísticos realizados a partir da
filmagem do movimento dos robôs. Neste trabalho, nós propomos uma maneira alternativa
de realizar tais análises com a utilização da técnica de Verificação de Modelos Probabilísticos
com a linguagem e ferramenta PRISM. Com PRISM, podemos, tanto realizar simulações
quanto verificar exaustivamente se um planejamento de movimentação do robô satisfaz
fórmulas Probabilísticas Temporais específicas. Portanto, podemos medir o consumo de
energia, tempo necessário para completar missões, etc. e tudo isso em termos de algoritmos
específicos de planejamento de movimentação. Como consequência, podemos, também,
determinar se um algoritmo é superior a outro em relação a certas métricas. Além disso,
para facilitar o uso do nosso trabalho, escondemos a sintaxe do PRISM propondo uma
DSL amigável ao usuário. Em consequência, criamos um tradutor da DSL em PRISM
através da implementação de regras de tradução bem como fizemos uma investigação
preliminar sobre sua completude relativa usando a ferramenta de geração de elementos
gramaticais LGen. Ilustramos as idéias com algoritmos de planejamento de movimentação
para robôs de limpeza de casas.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufpe.br:123456789/20827 |
| Date | 15 September 2016 |
| Creators | ARAÚJO, Rafael Pereira de |
| Contributors | http://lattes.cnpq.br/2794026545404598, MOTA, Alexandre Cabral, NOGUEIRA, Sidney de Carvalho |
| Publisher | Universidade Federal de Pernambuco, Programa de Pos Graduacao em Ciencia da Computacao, UFPE, Brasil |
| Source Sets | IBICT Brazilian ETDs |
| Language | English |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Source | reponame:Repositório Institucional da UFPE, instname:Universidade Federal de Pernambuco, instacron:UFPE |
| Rights | Attribution-NonCommercial-NoDerivs 3.0 Brazil, http://creativecommons.org/licenses/by-nc-nd/3.0/br/, info:eu-repo/semantics/openAccess |
Page generated in 0.2895 seconds