Abstract: robotic swarms are usually designed in a bottom-up way, which can make robotic swarms vulnerable to environmental impact. It is particularly true for the widely used control mode of robotic swarms, where it is often the case that neither the correctness of the swarming tasks at the macro level nor the safety of the interaction among agents at the micro level can be guaranteed. To ensure that the behaviors are safe at runtime, it is necessary to take into account the property guard approaches for robotic swarms in uncertain environments. runtime enforcement is an approach which can guarantee the given properties in system execution and has no scalability issue. Although some runtime enforcement methods have been studied and applied in different domains, they cannot effectively solve the problem of property enforcement on robotic swarm tasks at present. In this paper, an enforcement method is proposed on swarms which should satisfy multi-level properties in uncertain environments. We introduce a macro-micro property enforcing framework with the notion of agent shields and a discrete-time enforcing mechanism called D-time enforcing. To realize this method, a domain specification language and the corresponding enforcer synthesis algorithms are developed. We then apply the approach to enforce the properties of the simulated robotic swarm in the robotflocksim platform. We evaluate and show the effectiveness of the method with experiments on specific unmanned aerial vehicle swarm tasks.

机器人集群的去中心化运行时强制方法

[1]Bauer A, Falcone Y, 2016. Decentralised LTL monitoring. Form Meth Syst Des, 48(1-2):46-93.

[2]Bloem R, Chatterjee K, Greimel K, et al., 2014. Synthesizing robust systems. Acta Inform, 51(3-4):193-220.

[3]Brambilla M, Ferrante E, Birattari M, et al., 2013. Swarm robotics: a review from the swarm engineering perspective. Swarm Intell, 7(1):1-41.

[4]Chung SJ, Paranjape AA, Dames P, et al., 2018. A survey on aerial swarm robotics. IEEE Trans Robot, 34(4):837-855.

[5]Dong W, Zhao CZ, Shu SX, et al., 2012. Anticipatory active monitoring for safety- and security-critical software. Sci China Inform Sci, 55(12):2723-2737.

[6]Dreossi T, Fremont DJ, Ghosh S, et al., 2019. VERIFAI: a toolkit for the formal design and analysis of artificial intelligence-based systems. Proc 31^st Int Conf on Computer Aided Verification, p.432-442.

[7]Egerstedt M, Lee SG, Diaz-Mercado Y, et al., 2020. Control of Swarming Robots. US Patent 10 537 996.

[8]Fine BT, Shell DA, 2013. Unifying microscopic flocking motion models for virtual, robotic, and biological flock members. Auton Robot, 35(2-3):195-219.

[9]Floreano D, Wood RJ, 2015. Science, technology and the future of small autonomous drones. Nature, 521(7553):linebreak 460-466.

[10]Gökc ce F, c Sahin E, 2009. To flock or not to flock: the pros and cons of flocking in long-range “migration” of mobile robot swarms. Proc 8^st Int Joint Conf on Autonomous Agents and Multiagent Systems, p.65-72.

[11]Hu C, Dong W, Yang YH, et al., 2020. Runtime verification on hierarchical properties of ROS-based robot swarms. IEEE Trans Reliab, 69(2):674-689.

[12]Khosla P, Brown B, Paredis C, et al., 2002. Millibot Report. Report on Millibot Project, DARPA Contract DABT63-97-1-0003, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA.

[13]Könighofer B, Alshiekh M, Bloem R, et al., 2017. Shield synthesis. Form Meth Syst Des, 51(2):332-361.

[14]Ligatti J, Bauer L, Walker D, 2005. Edit automata: enforcement mechanisms for run-time security policies. Int J Inform Sec, 4(1-2):2-16.

[15]Mondada F, Gambardella LM, Floreano D, et al., 2005. The cooperation of swarm-bots: physical interactions in collective robotics. IEEE Robot Autom Mag, 12(2):21-28.

[16]Nagavalli S, Chien SY, Lewis M, et al., 2015. Bounds of neglect benevolence in input timing for human interaction with robotic swarms. Proc 10^st Annual ACM/linebreak IEEE Int Conf on Human-Robot Interaction, p.197-204.

[17]Parr T, 2013. The Definitive ANTLR 4 Reference. Pragmatic Bookshelf, Dallas, USA, p.21-33.

[18]Pinisetty S, Preoteasa V, Tripakis S, et al., 2017. Predictive runtime enforcement. Form Meth Syst Des, 51(1):154-199.

[19]Pnueli A, 1977. The temporal logic of programs. Proc 18^st Annual Symp Foundations of Computer Science, p.46-57.

[20]Pugh J, Martinoli A, 2006. Multi-robot learning with particle swarm optimization. Proc 5^st Int joint Conf on Autonomous Agents and Multiagent Systems, p.441-448.

[21]Rajkumar R, Lee I, Sha L, et al., 2010. Cyber-physical systems: the next computing revolution. Proc 47^st Design Automation Conf, p.731-736.

[22]Raju D, Bharadwaj S, Topcu U, 2019. Online synthesis for runtime enforcement of safety in multi-agent systems. https://arxiv.org/abs/1910.10380

[23]Rasmussen S, Kingston D, Humphrey L, 2018. A brief introduction to unmanned systems autonomy services (UxAS). Int Conf on Unmanned Aircraft Systems, p.257-268.

[24]Reinbacher T, Rozier KY, Schumann J, 2014. Temporal-logic based runtime observer pairs for system health management of real-time systems. Proc 20^st Int Conf on Tools and Algorithms for the Construction and Analysis of Systems, p.357-372.

[25]Reynolds CW, 1987. Flocks, herds and schools: a distributed behavioral model. ACM SIGGRAPH Comput Graph, 21(4):25-34.

[26]c Sahin E, Girgin S, Bayindir L, et al., 2008. Swarm robotics. In: Blum C, Merkle D (Eds.), Swarm Intelligence. Natural Computing Series. Springer Berlin Heidelberg, p.87-100.

[27]Schwager M, McLurkin J, Rus D, 2006. Distributed coverage control with sensory feedback for networked robots. Proc Robotics: Science and Systems, p.117-132.

[28]Shi H, Dong W, Zhou G, et al., 2017. Monitor synthesis for parametric MTL properties in discrete control software. IEEE Int Conf on Software Quality, Reliability and Security Companion, p.355-362.

[29]Sinhuber M, van der Vaart K, Ouellette NT, 2019. Response of insect swarms to dynamic illumination perturbations. J Roy Soc Interf, 16(150):20180739.

[30]Standley T, Korf R, 2011. Complete algorithms for cooperative pathfinding problems. Proc 22^nd Int Joint Conf on Artificial Intelligence, p.668-673.

[31]Turgut AE, c Celikkanat H, Gökc ce F, et al., 2008. Self-organized flocking in mobile robot swarms. Swarm Intell, 2(2-4):97-120.

[32]Vásárhelyi G, Virágh C, Somorjai G, et al., 2018. Optimized flocking of autonomous drones in confined environments. Sci Robot, 3(20):eaat3536.

[33]Williams K, Burdick JW, 2006. Multi-robot boundary coverage with plan revision. IEEE Int Conf on Robotics and Automation, p.1716-1723.

[34]Wong C, Yang EF, Yan XT, et al., 2017. An overview of robotics and autonomous systems for harsh environments. Proc 23^rd Int Conf on Automation and Computing, p.1-6.

[35]Zhang X, Leucker M, Dong W, 2012. Runtime verification with predictive semantics. Proc 4^th Int Symp on NASA Formal Methods, p.418-432.

[36]Zhang Y, Kim K, Fainekos G, 2014. DisCoF: cooperative pathfinding in distributed systems with limited sensing and communication range. In: Chong NY, Cho YJ (Eds.), Distributed Autonomous Robotic Systems, p.325-340.