Towards the formal veri cation of correctness and robustness of robot swarms (Invited talk)

-

We were honoured to have the opportunity to share with the ICTCS and CILC 2017 attendees some of the recent work in our lab on verifying robot swarms. The talk was given by Alessio Lomuscio; the key topics discussed are based on joint work with Dr Panagiotis Kouvaros, previously at Imperial College London. The references below are given for the bene t of those seeking more details on the methods presented during the talk.

Robot swarms are large collections of small robots, typically running lightweight programs, interacting with their neighbours and the environment. In recent years swarm robotics has shown considerable applicability in a wide range of domains, including search and rescue, automatic mining, and plant monitoring.

I began by arguing that swarm systems bene t from logic-based speci cation languages typically used in AI and multi-agent systems that go beyond plain temporal logic, but also concern the knowledge, the intentions, and the strategic abilities of the agents in the system. To motivate this, I drew parallels with the area of multi-agent systems where approaches based on symbolic model checking [ 1 ], also in combination with symmetry reduction [ 2 ], parallel model checking [ 3 ], and SAT [ 4 ], are now common place.

I then started discussing the speci c case of swarms. One of their key feature is that the number of agents is unbounded at design time. I illustrated a semantics based on agent templates and introduced the parameterised model checking problem (PMCP) as the decision problem of establishing whether all in nitely many concrete instances of a swarm design based on agent templates satis es a given temporal-epistemic speci cation. Cut-o procedures from [5{7] solving the PMCP for di erent classes of swarms were presented, together with alternative approaches such as counter-abstraction [ 8 ]. This enabled us to ground the discussion on concrete protocols such as opinion formation [ 9 ] and brie y discuss related topics such as the veri cation of emergence in swarms [ 10 ].

I concluded by exploring the issue of resilience of a swarm against adverse functioning conditions. Again I drew parallels with our previous work on safety analysis in the context of autonomous systems [11{13]. To do this, I introduced the parameterised fault-tolerance problem as the decision problem of establishing whether any concrete system in which the ratio of faulty versus total number of agents is bounded by a parameter, satis es a given temporal-epistemic speci cation. I illustrated how faults can be injected automatically into correct designs so that the resulting mutated models can be automatically analysed and conclusions on the resilience of the original design can be drawn [ 14 ].

References

1. Lomuscio , A. , Qu , H. , Raimondi , F. : MCMAS : A model checker for the veri cation of multi-agent systems . Software Tools for Technology Transfer 19 ( 1 ) ( 2017 ) 9 { 30

2. Cohen , M. , Dam , M. , Lomuscio , A. , Qu , H.: A symmetry reduction technique for model checking temporal-epistemic logic . In: Proceedings of the 21st International Joint Conference on Arti cial Intelligence (IJCAI09) . ( 2009 ) 721 { 726

3. Kwiatkowska , M. , Lomuscio , A. , Qu , H.: Parallel model checking for temporal epistemic logic . In: Proceedings of the 19th European Conference on Arti cial Intelligence (ECAI10) , IOS Press ( 2010 ) 543 { 548

4. Kacprzak , M. , Lomuscio , A. , Penczek , W. : From bounded to unbounded model checking for temporal epistemic logic . Fundamenta Informaticae 63 ( 2-3 ) ( 2004 ) 221 { 240

5. Kouvaros , P. , Lomuscio , A. : Automatic veri cation of parametrised interleaved multi-agent systems . In: Proceedings of the 12th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS13) , IFAAMAS ( 2013 ) 861 { 868

6. Kouvaros , P. , Lomuscio , A. : A cuto technique for the veri cation of parameterised interpreted systems with parameterised environments . In: Proceedings of the 23rd International Joint Conference on Arti cial Intelligence (IJCAI13) , AAAI Press ( 2013 ) 2013 { 2019

7. Kouvaros , P. , Lomuscio , A. : Parameterised veri cation for multi-agent systems . Arti cial Intelligence 234 ( 2016 ) 152 { 189

8. Kouvaros , P. , Lomuscio , A. : A counter abstraction technique for the veri cation of robot swarms . In: Proceedings of the 29th AAAI Conference on Arti cial Intelligence (AAAI15) , AAAI Press ( 2015 ) 2081 { 2088

9. Kouvaros , P. , Lomuscio , A. : Formal veri cation of opinion formation in swarms . In: Proceedings of the 15th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS16) , IFAAMAS ( 2016 ) 1200 { 1209

10. Kouvaros , P. , Lomuscio , A. : Verifying emergent properties of swarms . In: Proceedings of the 24th International Joint Conference on Arti cial Intelligence (IJCAI15) , AAAI Press ( 2015 ) 1083 { 1089

11. Ezekiel , J. , Lomuscio , A. : Combining fault injection and model checking to verify fault tolerance in multi-agent systems . In: Proceedings of the 8th International Conference on Autonomous Agents and Multiagent Systems (AAMAS09) , IFAAMAS Press ( 2009 ) 113 { 120

12. Ezekiel , J. , Lomuscio , A. , Molnar , L. , Veres , S. : Verifying fault tolerance and selfdiagnosability of an autonomous underwater vehicle . In: Proceedings of the 22nd International Joint Conference on Arti cial Intelligence (IJCAI11) , AAAI Press ( 2011 ) 1659 { 1664

13. Ezekiel , J. , Lomuscio , A. : Combining fault injection and model checking to verify fault tolerance, recoverability, and diagnosability in multi-agent systems . Information and Computation 254 ( 2 ) ( 2017 ) 167 { 194

14. Kouvaros , P. , Lomuscio , A. : Verifying fault-tolerance in parameterised multi-agent systems . In: Proceedings of the 26th International Joint Conference on Arti cial Intelligence (IJCAI17) , AAAI Press ( 2017 ) 288 { 294