Probabilistic Model Checking Techniques for Drone Swarms

Lead Research Organisation: Imperial College London
Department Name: 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

Studentship Projects

Project Reference Relationship Related To Start End Student Name
EP/N509486/1 30/09/2016 30/03/2022
1979782 Studentship EP/N509486/1 30/09/2017 30/03/2021 Edoardo Pirovano
 
Description This award developed new techniques to verify the behaviour of systems that involve an unknown number of participants. Some examples of such systems include drone swarms, network protocols, and Internet of Things devices. While techniques have previously been developed to verify these, they did not cover the case of probabilistic systems, where the outcome of actions is not fixed but instead follows a probability distribution. In this award, we have created new techniques for addressing the verification of these unbounded probabilistic systems, and implemented them into a software package. We gave some example applications of our toolkit to verify a number of scenarios, with a particular focus on case studies from swarm robotics.
Exploitation Route The software package developed in this award could be used by other researchers and/or people in industry in order to verify further systems. Additionally, the techniques developed could be further expanded with additional research in order to enable the modeling of even richer scenarios.
Sectors Aerospace

Defence and Marine

Digital/Communication/Information Technologies (including Software)

Electronics

Transport
 
Title PSV 
Description PSV provides a toolkit for verifying properties of unbounded probabilistic multi-agent systems. It combines our previous toolkits PSV-BD, PSV-CA, PSV-F, and PSV-S to support all the models and specifications that they did in one unified software package. 
Type Of Technology Software 
Year Produced 2021 
Open Source License? Yes  
Impact This software package was fully explained and evaluated in my PhD thesis, Parameterised Model Checking of Probabilistic Multi-Agent Systems. 
URL https://github.com/edoardopirovano/psv
 
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/
 
Title PSV-F 
Description Probabilistic Swarm Verifier for Faulty systems is a software package for the verification of properties in probabilistic swarm systems that may exhibit faults. Further information can be found in the corresponding paper (published at IJCAI 2020). 
Type Of Technology Software 
Year Produced 2020 
Open Source License? Yes  
Impact A paper covering the theory behind this software and evaluating the toolkit was published at IJCAI 2020. 
URL https://vas.doc.ic.ac.uk/software/probabilistic/
 
Title PSV-S 
Description Probabilistic Swarm Verifier for Strategic properties is a software package for the verification of strategic properties in probabilistic swarm systems. Further information can be found in the corresponding paper (published at AAMAS 2020). 
Type Of Technology Software 
Year Produced 2020 
Open Source License? Yes  
Impact A paper covering the theory behind this toolkit and evaluating its usability was published at AAMAS 2020. 
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/
 
Description Talk at World Logic Day 2021 Event 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Presented my work at Imperial's World Logic Day 2021 event, which was attended by around 50 people.
Year(s) Of Engagement Activity 2021
URL https://sites.google.com/view/imperial-worldlogicday2021/