A Counter Abstraction Technique for the Verification of Probabilistic Swarm Systems

被引：0
|
作者：
Lomuscio, Alessio [1 ]
Pirovano, Edoardo [1 ]
机构：
[1] Imperial Coll London, London, England
来源：
AAMAS '19: PROCEEDINGS OF THE 18TH INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS AND MULTIAGENT SYSTEMS | 2019年
关键词：
MODEL CHECKING;
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We introduce a method for formally verifying properties of arbitrarily large swarms whose agents are modelled probabilistically. We define a parameterised probabilistic semantics for modelling swarms and observe that their verification problem against PLTL specifications is undecidable. We develop a partial procedure for verifying arbitrarily large swarms based on counter abstraction and show its correctness. We present an implementation and report the experimental results obtained when verifying a swarm foraging protocol.
引用
收藏
页码：161 / 169
页数：9
相关论文
共 50 条
  • [31] Combining Control and Data Abstraction in the Verification of Hybrid Systems
    Briand, Xavier
    Jeannet, Bertrand
    [J]. IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2010, 29 (10) : 1481 - 1494
  • [32] Verification by abstraction
    Shankar, N
    [J]. FORMAL METHODS AT THE CROSSROADS: FROM PANACEA TO FOUNDATIONAL SUPPORT, 2003, 2757 : 367 - 380
  • [33] Verification of Deployed Artifact Systems via Data Abstraction
    Belardinelli, Francesco
    Lomuscio, Alessio
    Patrizi, Fabio
    [J]. SERVICE-ORIENTED COMPUTING, 2011, 7084 : 142 - 156
  • [34] Abstraction based verification of stability of polyhedral switched systems
    Soto, Miriam Garcia
    Prabhakar, Pavithra
    [J]. NONLINEAR ANALYSIS-HYBRID SYSTEMS, 2020, 36
  • [35] Probabilistic aggregation strategies in swarm robotic systems
    Soysal, O
    Sahin, E
    [J]. 2005 IEEE Swarm Intelligence Symposium, 2005, : 325 - 332
  • [36] Automatic Verification of Counter Systems With Ranking Function
    Encrenaz, Emmanuelle
    Finkel, Alain
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 239 : 85 - 103
  • [37] Counter-example guided predicate abstraction of hybrid systems
    Alur, R
    Dang, T
    Ivancic, F
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2003, 2619 : 208 - 223
  • [38] CSP-based counter abstraction for systems with node identifiers
    Mazur, Tomasz
    Lowe, Gavin
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2014, 81 : 3 - 52
  • [39] Towards temporal verification of swarm robotic systems
    Dixon, Clare
    Winfield, Alan F. T.
    Fisher, Michael
    Zeng, Chengxiu
    [J]. ROBOTICS AND AUTONOMOUS SYSTEMS, 2012, 60 (11) : 1429 - 1441
  • [40] Structural Counter Abstraction
    Bansal, Kshitij
    Koskinen, Eric
    Wies, Thomas
    Zufferey, Damien
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2013, 2013, 7795 : 62 - 77
12345