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 条
  • [21] A Three-Value Abstraction Technique for the Verification of Epistemic Properties in Multi-agent Systems
    Belardinelli, Francesco
    Lomuscio, Alessio
    LOGICS IN ARTIFICIAL INTELLIGENCE, (JELIA 2016), 2016, 10021 : 112 - 126
  • [22] Informed Swarm Verification of InfiniteState Systems
    Wijs, Anton
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (73): : 19 - 19
  • [23] Safety Verification for Probabilistic Hybrid Systems
    Koutsoukos, Xenofon
    EUROPEAN JOURNAL OF CONTROL, 2012, 18 (06) : 588 - 590
  • [24] Verification of probabilistic systems with faulty communication
    Abdulla, PA
    Bertrand, N
    Rabinovich, A
    Schnoebelen, P
    INFORMATION AND COMPUTATION, 2005, 202 (02) : 141 - 165
  • [25] The verification of probabilistic lossy channel systems
    Schnoebelen, P
    VALIDATION OF STOCHASTIC SYSTEMS: A GUIDE TO CURRENT RESEARCH, 2004, 2925 : 445 - 465
  • [26] Probabilistic Verification of Concurrent Autonomous Systems
    Parker, David
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2021, (339): : 9 - 9
  • [27] Automated Verification Techniques for Probabilistic Systems
    Forejt, Vojtech
    Kwiatkowska, Marta
    Norman, Gethin
    Parker, David
    FORMAL METHODS FOR ETERNAL NETWORKED SOFTWARE SYSTEMS, SFM 2011, 2011, 6659 : 53 - 113
  • [28] On the numerical verification of probabilistic rewriting systems
    Ben Hassen, Jounaidi
    Tahar, Sofiene
    2006 DESIGN AUTOMATION AND TEST IN EUROPE, VOLS 1-3, PROCEEDINGS, 2006, : 1223 - +
  • [29] Verification of probabilistic systems with faulty communication
    Abdulla, PA
    Rabinovich, A
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, PROCEEDINGS, 2003, 2620 : 39 - 53
  • [30] Safety Verification for Probabilistic Hybrid Systems
    Zhang, Lijun
    She, Zhikun
    Ratschan, Stefan
    Hermanns, Holger
    Hahn, Ernst Moritz
    COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2010, 6174 : 196 - 211
12345