This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
teaching:mfe:ia [2012/03/21 16:05] mdorigo Edited projects in swarm robotics 2012-2012 |
teaching:mfe:ia [2012/03/21 16:07] mdorigo [Formal verification of a swarm robotics behavior through statistical model checking] |
||
|---|---|---|---|
| Line 200: | Line 200: | ||
| checking to formally verify properties of a collective behavior of a | checking to formally verify properties of a collective behavior of a | ||
| robot swarm. Verifying that a system behaves as desired in all | robot swarm. Verifying that a system behaves as desired in all | ||
| - | possible situations is necessary when autonomous robots are involved. | + | possible situations is necessary when autonomous robots are involved. |
| This is particularly true in swarm robotics systems, where the | This is particularly true in swarm robotics systems, where the | ||
| interactions of large number of individuals can result in behaviors | interactions of large number of individuals can result in behaviors | ||
| Line 208: | Line 208: | ||
| computationally impossible to analyze. | computationally impossible to analyze. | ||
| - | The goal of this thesis is to apply a novel model checking technique, | + | This thesis is will explore the application of a novel model checking technique, called statistical model checking, to formally verify a swarm robotics system. A collective behavior will be firstly implemented in |
| - | called statistical model checking, to formally verify a swarm robotics | + | |
| - | system. A collective behavior will be firstly implemented in | + | |
| simulation and then analyzed through statistical model checking. | simulation and then analyzed through statistical model checking. | ||