Decentralized runtime enforcement for robotic swarms

HU Chi; DONG Wei; YANG Yong-hui; SHI Hao; DENG Fei

doi:10.1631/FITEE.2000203

Your Location：

Home >

Browse articles >

Decentralized runtime enforcement for robotic swarms

Special Section on Model-Driven Software Development for Cyber-Physical Systems | Updated：2022-05-19

- Decentralized runtime enforcement for robotic swarms
- 机器人集群的去中心化运行时强制方法
- Frontiers of Information Technology & Electronic Engineering Vol. 21, Issue 11, Pages: 1591-1606(2020)
- Affiliations：
  
  College of Computer Science, National University of Defense Technology, Changsha 410073, China
  Institute of Computer Application, China Academy of Engineering Physics, Mianyang 621999, China
- Author bio：
  
  [ "Chi HU, E-mail: huchi16@nudt.edu.cn" ]
  Wei DONG, wdong@nudt.edu.cn
  [ "Hao SHI, shihao14@nudt.edu.cn" ]
- Funds：
- DOI：10.1631/FITEE.2000203
  CLC： TP311
- Received：30 April 2020，
  
  Revised：2020-10-10，
  
  Published：2020-11
- Accepted：
Scan QR Code
HU Chi, DONG Wei, YANG Yong-hui, et al. Decentralized runtime enforcement for robotic swarms[J]. Frontiers of Information Technology & Electronic Engineering, 2020, 21(11): 1591-1606.
DOI：

HU Chi, DONG Wei, YANG Yong-hui, et al. Decentralized runtime enforcement for robotic swarms[J]. Frontiers of Information Technology & Electronic Engineering, 2020, 21(11): 1591-1606. DOI： 10.1631/FITEE.2000203.

摘要

机器人系统设计通常是自下而上的，这种开发方式使机器人群体很容易受到环境影响。具体来说，目前广泛使用的集群控制模型不能保证宏观上群体任务的正确性，也不能保证微观上机器人节点间交互的安全性。因此，为确保机器人行为在运行时的安全性，有必要考虑机器人集群系统在不确定环境下的复杂性质。运行时强制技术能确保状态序列始终满足给定性质，并且避免状态爆炸的问题。虽然在其他领域出现了一些运行时强制的工作，但目前还不能解决机器人集群问题。本文通过引入宏观/微观性质强制框架、防护器以及一个离散时间的强制机制（discrete-time enforcement，

-time强制）解决该问题。论述了领域规约语言和强制器合成算法，然后，将此方法应用到一个机器人集群仿真工具robotflocksim中合成强制器。以无人机集群任务为例实现了该方法，并对实验效果进行讨论。

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 $\mathcal{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.

关键词

Keywords

references

A Bauer , , , Y Falcone . . Decentralised LTL monitoring . . Form Meth Syst Des , , 2016 . . 48 ( ( 1-2 ): ): 46 - - 93 . . DOI: 10.1007/s10703-016-0253-8 http://doi.org/10.1007/s10703-016-0253-8 . .

R Bloem , , , K Chatterjee , , , K Greimel , , , 等 . . Synthesizing robust systems . . Acta Inform , , 2014 . . 51 ( ( 3-4 ): ): 193 - - 220 . . DOI: 10.1007/s00236-013-0191-5 http://doi.org/10.1007/s00236-013-0191-5 . .

M Brambilla , , , E Ferrante , , , M Birattari , , , 等 . . Swarm robotics: a review from the swarm engineering perspective . . Swarm Intell , , 2013 . . 7 ( ( 1 ): ): 1 - - 41 . . DOI: 10.1007/s11721-012-0075-2 http://doi.org/10.1007/s11721-012-0075-2 . .

SJ Chung , , , AA Paranjape , , , P Dames , , , 等 . . A survey on aerial swarm robotics . . IEEE Trans Robot , , 2018 . . 34 ( ( 4 ): ): 837 - - 855 . . DOI: 10.1109/TRO.2018.2857475 http://doi.org/10.1109/TRO.2018.2857475 . .

W Dong , , , CZ Zhao , , , SX Shu , , , 等 . . Anticipatory active monitoring for safety- and security-critical software . . Sci China Inform Sci , , 2012 . . 55 ( ( 12 ): ): 2723 - - 2737 . . DOI: 10.1007/s11432-012-4739-8 http://doi.org/10.1007/s11432-012-4739-8 . .

T Dreossi , , , DJ Fremont , , , S Ghosh , , , 等 . . VERIFAI: a toolkit for the formal design and analysis of artificial intelligence-based systems . . Proc $31^{\rm st}$ Int Conf on Computer Aided Verification , , 2019 . . p.432 - - 442 . . DOI: 10.1007/978-3-030-25540-4_25 http://doi.org/10.1007/978-3-030-25540-4_25 . .

M Egerstedt , , , SG Lee , , , Y Diaz-Mercado , , , 等 . . Control of Swarming Robots . . US Patent , , 2020 . . 10 537 996 . .

BT Fine , , , DA Shell . . Unifying microscopic flocking motion models for virtual, robotic, and biological flock members . . Auton Robot , , 2013 . . 35 ( ( 2-3 ): ): 195 - - 219 . . DOI: 10.1007/s10514-013-9338-z http://doi.org/10.1007/s10514-013-9338-z . .

D Floreano , , , RJ Wood . . Science, technology and the future of small autonomous drones . . Nature , , 2015 . . 521 ( ( 7553 ): ): 460 - - 466 . . DOI: 10.1038/nature14542 http://doi.org/10.1038/nature14542 . .

F Gökçe , , , E Şahin . . To flock or not to flock: the pros and cons of flocking in long-range "migration" of mobile robot swarms . . Proc $8^{{\rm th}}$ Int Joint Conf on Autonomous Agents and Multiagent Systems , , 2009 . . p.65 - - 72 . . . .

C Hu , , , W Dong , , , YH Yang , , , 等 . . Runtime verification on hierarchical properties of ROS-based robot swarms . . IEEE Trans Reliab , , 2020 . . 69 ( ( 2 ): ): 674 - - 689 . . DOI: 10.1109/TR.2019.2923681 http://doi.org/10.1109/TR.2019.2923681 . .

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

B Könighofer , , , M Alshiekh , , , R Bloem , , , 等 . . Shield synthesis . . Form Meth Syst Des , , 2017 . . 51 ( ( 2 ): ): 332 - - 361 . . DOI: 10.1007/s10703-017-0276-9 http://doi.org/10.1007/s10703-017-0276-9 . .

J Ligatti , , , L Bauer , , , D Walker . . Edit automata: enforcement mechanisms for run-time security policies . . Int J Inform Sec , , 2005 . . 4 ( ( 1-2 ): ): 2 - - 16 . . DOI: 10.1007/s10207-004-0046-8 http://doi.org/10.1007/s10207-004-0046-8 . .

F Mondada , , , LM Gambardella , , , D Floreano , , , 等 . . The cooperation of swarm-bots: physical interactions in collective robotics . . IEEE Robot Autom Mag , , 2005 . . 12 ( ( 2 ): ): 21 - - 28 . . DOI: 10.1109/MRA.2005.1458313 http://doi.org/10.1109/MRA.2005.1458313 . .

S Nagavalli , , , SY Chien , , , M Lewis , , , 等 . . Bounds of neglect benevolence in input timing for human interaction with robotic swarms . . Proc $10^{\rm th}$ Annual ACM/IEEE Int Conf on Human-Robot Interaction , , 2015 . . p.197 - - 204 . . DOI: 10.1145/2696454.2696470 http://doi.org/10.1145/2696454.2696470 . .

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

S Pinisetty , , , V Preoteasa , , , S Tripakis , , , 等 . . Predictive runtime enforcement . . Form Meth Syst Des , , 2017 . . 51 ( ( 1 ): ): 154 - - 199 . . DOI: 10.1007/s10703-017-0271-1 http://doi.org/10.1007/s10703-017-0271-1 . .

A Pnueli . . The temporal logic of programs . . Proc $18^{\rm th}$ Annual Symp Foundations of Computer Science , , 1977 . . p.46 - - 57 . . DOI: 10.1109/SFCS.1977.32 http://doi.org/10.1109/SFCS.1977.32 . .

J Pugh , , , A Martinoli . . Multi-robot learning with particle swarm optimization . . Proc $8^{\rm th}$ Int joint Conf on Autonomous Agents and Multiagent Systems , , 2006 . . p.441 - - 448 . . DOI: 10.1145/1160633.1160715 http://doi.org/10.1145/1160633.1160715 . .

R Rajkumar , , , I Lee , , , L Sha , , , 等 . . Cyber-physical systems: the next computing revolution . . Proc $47^{\rm th}$ Design Automation Conf , , 2010 . . p.731 - - 736 . . DOI: 10.1145/1837274.1837461 http://doi.org/10.1145/1837274.1837461 . .

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

S Rasmussen , , , D Kingston , , , L Humphrey . . A brief introduction to unmanned systems autonomy services (UxAS) . . Int Conf on Unmanned Aircraft Systems , , 2018 . . p.257 - - 268 . . DOI: 10.1109/icuas.2018.8453287 http://doi.org/10.1109/icuas.2018.8453287 . .

T Reinbacher , , , KY Rozier , , , J Schumann . . Temporal-logic based runtime observer pairs for system health management of real-time systems . . Proc $20^{\rm th}$ Int Conf on Tools and Algorithms for the Construction and Analysis of Systems , , 2014 . . p.357 - - 372 . . DOI: 10.1007/978-3-642-54862-8_24 http://doi.org/10.1007/978-3-642-54862-8_24 . .

CW Reynolds . . Flocks, herds and schools: a distributed behavioral model . . ACM SIGGRAPH Comput Graph , , 1987 . . 21 ( ( 4 ): ): 25 - - 34 . . DOI: 10.1145/37401.37406 http://doi.org/10.1145/37401.37406 . .

E Şahin , , , S Girgin , , , L Bayindir , , , 等 . . Swarm robotics.In: Blum C, Merkle D (Eds.), Swarm Intelligence^ Natural Computing Series . . Springer Berlin Heidelberg , , 2008 . . p.87 - - 100 . . DOI: 10.1007/978-3-540-74089-6_3 http://doi.org/10.1007/978-3-540-74089-6_3 . .

M Schwager , , , J McLurkin , , , D Rus . . Distributed coverage control with sensory feedback for networked robots . . Proc Robotics: Science and Systems , , 2006 . . p.117 - - 132 . . DOI: 10.15607/RSS.2006.II.007 http://doi.org/10.15607/RSS.2006.II.007 . .

H Shi , , , W Dong , , , G Zhou , , , 等 . . Monitor synthesis for parametric MTL properties in discrete control software . . IEEE Int Conf on Software Quality, Reliability and Security Companion , , 2017 . . p.355 - - 362 . . DOI: 10.1109/QRS-C.2017.66 http://doi.org/10.1109/QRS-C.2017.66 . .

M Sinhuber , , , K van der Vaart , , , NT Ouellette . . Response of insect swarms to dynamic illumination perturbations . . J Roy Soc Interf , , 2019 . . 16 ( ( 150 ): ): 20180739 DOI: 10.1098/rsif.2018.0739 http://doi.org/10.1098/rsif.2018.0739 . .

T Standley , , , R Korf . . Complete algorithms for cooperative pathfinding problems . . Proc $22^{\rm nd}$ Int Joint Conf on Artificial Intelligence , , 2011 . . p.668 - - 673 . . DOI: 10.5591/978-1-57735-516-8/IJCAI11-118 http://doi.org/10.5591/978-1-57735-516-8/IJCAI11-118 . .

AE Turgut , , , H Çelikkanat , , , F Gökçe , , , 等 . . Self-organized flocking in mobile robot swarms . . Swarm Intell , , 2008 . . 2 ( ( 2-4 ): ): 97 - - 120 . . DOI: 10.1007/s11721-008-0016-2 http://doi.org/10.1007/s11721-008-0016-2 . .

G Vásárhelyi , , , C Virágh , , , G Somorjai , , , 等 . . Optimized flocking of autonomous drones in confined environments . . Sci Robot , , 2018 . . 3 ( ( 20 ): ): eaat3536 DOI: 10.1126/scirobotics.aat3536 http://doi.org/10.1126/scirobotics.aat3536 . .

K Williams , , , JW Burdick . . Multi-robot boundary coverage with plan revision . . IEEE Int Conf on Robotics and Automation , , 2006 . . p.11716 - - 1723 . . DOI: 10.1109/ROBOT.2006.1641954 http://doi.org/10.1109/ROBOT.2006.1641954 . .

C Wong , , , EF Yang , , , XT Yan , , , 等 . . An overview of robotics and autonomous systems for harsh environments . . Proc $23^{\rm rd}$ Int Conf on Automation and Computing , , 2017 . . p.1 - - 6 . . DOI: 10.23919/IConAC.2017.8082020 http://doi.org/10.23919/IConAC.2017.8082020 . .

X Zhang , , , M Leucker , , , W Dong . . Runtime verification with predictive semantics . . Proc $4^{\rm th}$ Int Symp on NASA Formal Methods , , 2012 . . p.418 - - 432 . . DOI: 10.1007/978-3-642-28891-3_37 http://doi.org/10.1007/978-3-642-28891-3_37 . .

Y Zhang , , , K Kim , , , G Fainekos . . DisCoF: cooperative pathfinding in distributed systems with limited sensing and communication range . . In: Chong NY, Cho YJ (Eds.), Distributed Autonomous Robotic Systems , , 2014 . . p.325 - - 340 . . DOI: 10.1007/978-4-431-55879-8_23 http://doi.org/10.1007/978-4-431-55879-8_23 . .

Views

Downloads

CSCD

Alert me when the article has been cited

Submit

Tools

Publicity Resources

No data

Related Author

No data

Related Institution

No data

Chat

Address：Zhejiang University Press, 148 Tianmushan Road, Hangzhou, China Postal code：310028
Tel：+86-571-88273162 Email：fitee@zju.edu.cn
It is recommended to read the content of this site in Chrome&IE9+. Please switch to extreme mode in browser 360.
Cookies We use cookies to help provide and enhance our service and tailor content. By continuing, you agree to the use of cookies.

⁰