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 条
  • [1] A counter abstraction technique for verifying properties of probabilistic swarm systems
    Lomuscio, Alessio
    Pirovano, Edoardo
    [J]. ARTIFICIAL INTELLIGENCE, 2022, 305
  • [2] A Counter Abstraction Technique for the Verification of Robot Swarms
    Kouvaros, Panagiotis
    Lomuscio, Alessio
    [J]. PROCEEDINGS OF THE TWENTY-NINTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2015, : 2081 - 2088
  • [3] Parameterized verification by probabilistic abstraction
    Arons, T
    Pnueli, A
    Zuck, L
    [J]. FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, PROCEEDINGS, 2003, 2620 : 87 - 102
  • [4] Verification and behavior abstraction towards a tractable verification technique for large distributed systems
    Nitsche, U
    [J]. JOURNAL OF SYSTEMS AND SOFTWARE, 1996, 33 (03) : 273 - 285
  • [5] Abstraction of probabilistic systems
    Katoen, Joost-Pieter
    [J]. FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, 2007, 4763 : 1 - 3
  • [6] Formal Verification of Probabilistic Swarm Behaviours
    Konur, Savas
    Dixon, Clare
    Fisher, Michael
    [J]. SWARM INTELLIGENCE, 2010, 6234 : 440 - 447
  • [7] An Abstraction Technique for the Verification of Multi-Agent Systems Against ATL Specifications
    Lomuscio, Alessio
    Michaliszyn, Jakub
    [J]. FOURTEENTH INTERNATIONAL CONFERENCE ON THE PRINCIPLES OF KNOWLEDGE REPRESENTATION AND REASONING, 2014, : 428 - 437
  • [8] An abstraction technique for real-time verification
    Clarke, Edmund M.
    Lerda, Flavio
    Talupur, Muralidhar
    [J]. NEXT GENERATION DESIGN AND VERIFICATION METHODOLOGIES FOR DISTRIBUTED EMBEDDED CONTROL SYSTEMS, 2007, : 1 - +
  • [9] Automatic Probabilistic Program Verification through Random Variable Abstraction
    Barsotti, Damian
    Wolovick, Nicolas
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2010, (28): : 34 - 47
  • [10] Ordered Counter-Abstraction Refinable Subword Relations for Parameterized Verification
    Ganty, Pierre
    Rezine, Ahmed
    [J]. LANGUAGE AND AUTOMATA THEORY AND APPLICATIONS (LATA 2014), 2014, 8370 : 396 - 408
12345