Abstract | ||
---|---|---|
Robots are increasingly being used in industry and starting their way in our homes as well, particularly cleaning robots. The common techniques to analyze cleaning robots are based on simulations or statistical experiments made from filming robots' movements. In this work, we propose an alternative way of performing such an analysis by using Probabilistic Model Checking with the language and tool PRISM. We propose a PRISM characterization for robot motion algorithms that can be used as the input for simulations as well as check exhaustively whether an algorithm satisfies specific Probabilistic Temporal formulas. The proposed PRISM model allows measuring energy consumption and time to complete missions; such metrics are helpful to compare different algorithms considering specific environments. Furthermore, to ease the use of our work, we hide the PRISM syntax by proposing an imperative style DSL used to specify the algorithms. We illustrate those ideas with motion planning algorithms for home cleaning robots. |
Year | DOI | Venue |
---|---|---|
2017 | 10.1109/IRI.2017.61 | 2017 IEEE International Conference on Information Reuse and Integration (IRI) |
Keywords | Field | DocType |
prism,dsl,probabilistic model checking | Motion planning,Data mining,Algorithm design,Digital subscriber line,Computer science,Probabilistic analysis of algorithms,Artificial intelligence,Probabilistic logic,Robot,Energy consumption,Syntax,Machine learning | Conference |
ISBN | Citations | PageRank |
978-1-5386-1563-8 | 0 | 0.34 |
References | Authors | |
6 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Rafael Pereira de Araujo | 1 | 0 | 0.34 |
Alexandre Mota | 2 | 72 | 11.09 |
Sidney Nogueira | 3 | 49 | 5.69 |