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

Publications

10 25 50

Studentship Projects

Project Reference Relationship Related To Start End Student Name
EP/N509486/1 01/10/2016 30/09/2021
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/