Probabilistic Model Checking Techniques for Drone Swarms
Lead Research Organisation:
Imperial College London
Department Name: Dept of Computing
Abstract
We will investigate the use of probabilistic model checking techniques to verify drone swarm systems. This will involve extending these techniques to enable modelling of systems where the size is potentially unbounded and not known at design-time. We will also develop tools that implement these techniques and demonstrate their applicability on protocols from swarm robotics.
Robotics and modelling
Robotics and modelling
People |
ORCID iD |
| Alessio R Lomuscio (Primary Supervisor) | |
| Edoardo Pirovano (Student) |
Studentship Projects
| Project Reference | Relationship | Related To | Start | End | Student Name |
|---|---|---|---|---|---|
| EP/N509486/1 | 01/10/2016 | 31/03/2022 | |||
| 1979782 | Studentship | EP/N509486/1 | 01/10/2017 | 31/03/2021 | Edoardo Pirovano |
| Title | PSV-BD |
| Description | Probabilistic Swarm Verifier for BoundeD time properties is a software package for the verification of emergence of bounded time properties in probabilistic swarm systems. Further information can be found in the corresponding paper (published at IJCAI 2018). |
| Type Of Technology | Software |
| Year Produced | 2018 |
| Open Source License? | Yes |
| Impact | Enables the verification of bounded time properties in probabilistic swarm systems. |
| URL | https://vas.doc.ic.ac.uk/software/probabilistic/ |
| Title | PSV-CA |
| Description | Probabilistic Swarm Verifier using Counter Abstraction is a software package for the verification of properties in probabilistic swarm systems. Further information can be found in the corresponding paper (published at AAMAS 2019). |
| Type Of Technology | Software |
| Year Produced | 2019 |
| Open Source License? | Yes |
| Impact | Enables the verification of broader range of properties of probabilistic swarm systems than was previously possible. |
| URL | https://vas.doc.ic.ac.uk/software/probabilistic/ |
| Description | Presenting work at Highlights of Logic, Games and Automata 2019 |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Postgraduate students |
| Results and Impact | Attended the Highlights of Logic, Games and Automata 2019 conference in Warsaw to present our AAMAS 2019 work on verifying probabilistic drone swarms. The talk was well received and a number of audience members asked for further details on the work afterwards. |
| Year(s) Of Engagement Activity | 2019 |
| URL | http://highlights-conference.org/warsaw/ |