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
    ARTIFICIAL INTELLIGENCE, 2022, 305
  • [2] A Counter Abstraction Technique for the Verification of Robot Swarms
    Kouvaros, Panagiotis
    Lomuscio, Alessio
    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
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, PROCEEDINGS, 2003, 2620 : 87 - 102
  • [4] Parameterized Verification of Systems with Precise (0,1)-Counter Abstraction
    Eichler, Paul
    Jacobs, Swen
    Weil-Kennedy, Chana
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2025, PT I, 2025, 15529 : 101 - 124
  • [5] Verification and behavior abstraction towards a tractable verification technique for large distributed systems
    Nitsche, U
    JOURNAL OF SYSTEMS AND SOFTWARE, 1996, 33 (03) : 273 - 285
  • [6] Abstraction of probabilistic systems
    Katoen, Joost-Pieter
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, 2007, 4763 : 1 - 3
  • [7] On abstraction of probabilistic systems
    Dehnert, Christian
    Gebler, Daniel
    Volpato, Michele
    Jansen, David N.
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2014, 8453 : 87 - 116
  • [8] Formal Verification of Probabilistic Swarm Behaviours
    Konur, Savas
    Dixon, Clare
    Fisher, Michael
    SWARM INTELLIGENCE, 2010, 6234 : 440 - 447
  • [9] An Abstraction Technique for the Verification of Multi-Agent Systems Against ATL Specifications
    Lomuscio, Alessio
    Michaliszyn, Jakub
    FOURTEENTH INTERNATIONAL CONFERENCE ON THE PRINCIPLES OF KNOWLEDGE REPRESENTATION AND REASONING, 2014, : 428 - 437
  • [10] An abstraction technique for real-time verification
    Clarke, Edmund M.
    Lerda, Flavio
    Talupur, Muralidhar
    NEXT GENERATION DESIGN AND VERIFICATION METHODOLOGIES FOR DISTRIBUTED EMBEDDED CONTROL SYSTEMS, 2007, : 1 - +
12345