More Web Proxy on the site http://driver.im/

research-article

Formal Verification of Opinion Formation in Swarms

Authors:

Panagiotis Kouvaros,

Alessio LomuscioAuthors Info & Claims

AAMAS '16: Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems

Pages 1200 - 1208

Published: 09 May 2016 Publication History

Abstract

We investigate the formal verification of consensus protocols in swarm systems composed of arbitrary many agents. We use templates to define the behaviour of the agents in an opinion dynamics setting and formulate their verification in terms of the associated parameterised model checking problem. We define a finite abstract model that we show to simulate swarms of any size, thereby precisely encoding any concrete instantiation of the swarm. We give an automatic procedure for verifying temporal-epistemic properties of consensus protocols by model checking the associated finite abstract model. We present a toolkit that can be used to generate the abstract model automatically and verify a given protocol by symbolic model checking. We use the toolkit to verify the correctness of majority rule protocols in arbitrary large swarms.

References

[1]

B. Aminof, A. Murano, S. Rubin, and F. Zuleger. Verification of asynchronous mobile-robots in partially-known environments. In PRIMA 2015: Principles and Practice of Multi-Agent Systems, pages 185--200. Springer, 2015.

[2]

K. Apt and D. C. Kozen. Limits for automatic verification of finite-state concurrent systems. Information Processing Letters, 22(6):307--309, 1986.

Digital Library

[3]

E. Bonabeau, M. Dorigo, and G. Theraulaz. Swarm intelligence. Oxford University Press, 1999.

Digital Library

[4]

M. C. Browne, E. M. Clarke, and O. Grumberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59:115--131, 1988.

Digital Library

[5]

E. Clarke, O. Grumberg, and M. Browne. Reasoning about networks with many identical finite state processes. Information and Computation, 81(1):13--31, 1989.

Digital Library

[6]

E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999.

Digital Library

[7]

M. de Oca, E. Ferrante, A. Scheidler, C. C. Pinciroli, M. Birattari, and M. Dorigo. Majority-rule opinion dynamics with differential latency: a mechanism for self-organized collective decision-making. Swarm Intelligence, 5(3--4):305--327, 2011.

[8]

C. Dixon, A. Winfield, M. Fisher, and C. Zeng. Towards temporal verification of swarm robotic systems. Robotics and Autonomous Systems, 60(11):1429--1441, 2012.

Digital Library

[9]

D. Dolev, C. Dwork, and L. Stockmeyer. On the minimal synchronism needed for distributed consensus. Journal of the ACM (JACM), 34(1):77--97, 1987.

Digital Library

[10]

E. A. Emerson and K. S. Namjoshi. Automatic verification of parameterized synchronous systems. In Proceedings of the 8th International Conference one Computer Aided Verification (CAV96), volume 1102 of Lecture Notes in Computer Science, pages 87--98. Springer, 1996.

Digital Library

[11]

R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning about Knowledge. MIT Press, Cambridge, 1995.

Digital Library

[12]

M. Fischer, N. Lynch, and M. Paterson. Impossibility of distributed consensus with one faulty process. Journal of the ACM (JACM), 32(2):374--382, 1985.

Digital Library

[13]

S. Garnier, J. Gautrais, M. Asadpour, C. Jost, and G. Theraulaz. Self-organized aggregation triggers collective decision making in a group of cockroach-like robots. Adaptive Behavior, 17(2):109--133, 2009.

Digital Library

[14]

S. Konur, C. Dixon, and M. Fisher. Analysing robot swarm behaviour via probabilistic model checking. Robotics and Autonomous Systems, 60(2):199--213, 2012.

Digital Library

[15]

P. Kouvaros and A. Lomuscio. A counter abstraction technique for the verification of robot swarms. In Proceedings of the 29th AAAI Conference on Artificial Intelligence (AAAI15), pages 2081--2088. AAAI Press, 2015.

Digital Library

[16]

P. Kouvaros and A. Lomuscio. Verifying emergent properties of swarms. In Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI15), pages 1083--1089. AAAI Press, 2015.

Digital Library

[17]

P. Kouvaros and A. Lomuscio. Parameterised verification for multi-agent systems. Artificial Intelligence, 234:152--189, 2016.

Digital Library

[18]

P. Krapivsky and S. Redner. Dynamics of majority rule in two-state interacting spin systems. Physical Review Letters, 90(23):238701, 2003.

[19]

R. Lambiotte, J. Saramäki, and V. Blondel. Dynamics of latent voters. Physical Review E, 79(4):046107, 2009.

[20]

A. Lomuscio, H. Qu, and F. Raimondi. MCMAS: A model checker for the verification of multi-agent systems. In Proceedings of the 21th International Conference on Computer Aided Verification (CAV09), volume 5643 of Lecture Notes in Computer Science, pages 682--688. Springer, 2009.

Digital Library

[21]

MCMAS-OFP. Model Checking Opinion Formation Protocols http://vas.doc.ic.ac.uk/software/extensions, 2016.

[22]

C. Parker and H. Zhang. Cooperative decision-making in decentralized multiple-robot systems: The best-of-n problem. IEEE/ASME Transactions on Mechatronics, 14(2):240--251, 2009.

[23]

C. Parker and H. Zhang. Collective unary decision-making by decentralized multiple-robot systems applied to the task-sequencing problem. Swarm Intelligence, 4(3):199--220, 2010.

[24]

W. Penczek and A. Lomuscio. Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae, 55(2):167--185, 2003.

Digital Library

[25]

W. Penczek and A. Lomuscio. Verifying epistemic properties of multi-agent systems via bounded model checking. In Proceedings of the 2nd International Joint Conference on Autonomous Agents and Multi-agent systems (AAMAS03), pages 209--216. IFAAMAS, 2003.

Digital Library

[26]

C. R. r, A. Vanderbilt, M. Hinchey, W. Truszkowski, and J. Rash. Properties of a formal method for prediction of emergent behaviors in swarm-based systems. In Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM04), pages 24--33. IEEE, 2004.

Digital Library

[27]

S. Rubin. Parameterised verification of autonomous mobile-agents in static but unknown environments. In Proceedings of the 14th International Conference on Autonomous Agents and Multiagent Systems (AAMAS15), pages 199--208. IFAAMAS, 2015.

Digital Library

[28]

E. Şahin. Swarm robotics: From sources of inspiration to domains of application. In Proceedings of the 2004 international conference on Swarm Robotics (SAB04), volume 3342 of Lecture Notes in Computer Science, pages 10--20. Springer, 2005.

Digital Library

[29]

E. Şahin and A. Winfield. Special issue on swarm robotics. Swarm Intelligence, 2(2):69--72, 2008.

[30]

A. Scheidler. Dynamics of majority rule with differential latencies. Physical Review E, 83(3):031116, 2011.

[31]

G. Valentini, H. Hamann, and M. Dorigo. Self-organized collective decision making: The weighted voter model. In Proceedings of the 14th International Conference on Autonomous Agents and Multiagent Systems, pages 45--52. IFAAMAS Press, 2014.

Digital Library

[32]

G. Valentini, H. Hamann, and M. Dorigo. Efficient decision-making in a self-organizing robot swarm: On the speed versus accuracy trade-off. In Proceedings of the 14th International Conference on Autonomous Agents and Multiagent Systems, pages 1305--1314. IFAAMAS Press, 2015.

Digital Library

[33]

A. Winfield, J. Sa, M. Fernández-Gago, C. Dixon, and M. Fisher. On formal specification of emergent behaviours in swarm robotic systems. International journal of advanced robotic systems, 2(4):363--370, 2005.

Cited By

Kouvaros PElkind E(2023)Towards formal verification of neuro-symbolic multi-agent systemsProceedings of the Thirty-Second International Joint Conference on Artificial Intelligence10.24963/ijcai.2023/800(7014-7019)Online publication date: 19-Aug-2023
https://dl.acm.org/doi/10.24963/ijcai.2023/800
Lomuscio APirovano EElkind EVeloso MAgmon NTaylor M(2019)A Counter Abstraction Technique for the Verification of Probabilistic Swarm SystemsProceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems10.5555/3306127.3331689(161-169)Online publication date: 8-May-2019
https://dl.acm.org/doi/10.5555/3306127.3331689
Kouvaros PLomuscio A(2017)Verifying fault-tolerance in parameterised multi-agent systemsProceedings of the 26th International Joint Conference on Artificial Intelligence10.5555/3171642.3171684(288-294)Online publication date: 19-Aug-2017
https://dl.acm.org/doi/10.5555/3171642.3171684
Show More Cited By

Index Terms

Formal Verification of Opinion Formation in Swarms
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking

Recommendations

A Counter Abstraction Technique for the Verification of Probabilistic Swarm Systems
AAMAS '19: Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems

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 ...
Formal verification of ASMs using MDGs

We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Formal Verification of Open Multi-Agent Systems
AAMAS '19: Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems

We study open multi-agent systems in which countably many agents may leave and join the system at run-time. We introduce a semantics, based on interpreted systems, to capture the openness of the system and show how an indexed variant of temporal-...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

AAMAS '16: Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems

May 2016

1580 pages

ISBN:9781450342391

General Chairs:
Catholijn M. Jonker
TU Delft, Netherlands
,
Stacy Marsella
University of Southern California, USA
,
Program Chairs:
John Thangarajah
RMIT University. Australia
,
Karl Tuyls
University of Liverpool, UK

Sponsors

IFAAMAS

In-Cooperation

SIGAI: ACM Special Interest Group on Artificial Intelligence

Publisher

International Foundation for Autonomous Agents and Multiagent Systems

Richland, SC

Publication History

Published: 09 May 2016

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

EPSRC Doctoral Prize Fellowship
EPSRC Research Project Trusted Autonomous Systems (grant No. EP/I00520X/1)

Conference

AAMAS '16

Sponsor:

AAMAS '16: International Conference on Agents and Multiagent Systems

May 9 - 13, 2016

Singapore, Singapore

Acceptance Rates

AAMAS '16 Paper Acceptance Rate 137 of 550 submissions, 25%;

Overall Acceptance Rate 1,155 of 5,036 submissions, 23%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
88
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 17 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kouvaros PElkind E(2023)Towards formal verification of neuro-symbolic multi-agent systemsProceedings of the Thirty-Second International Joint Conference on Artificial Intelligence10.24963/ijcai.2023/800(7014-7019)Online publication date: 19-Aug-2023
https://dl.acm.org/doi/10.24963/ijcai.2023/800
Lomuscio APirovano EElkind EVeloso MAgmon NTaylor M(2019)A Counter Abstraction Technique for the Verification of Probabilistic Swarm SystemsProceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems10.5555/3306127.3331689(161-169)Online publication date: 8-May-2019
https://dl.acm.org/doi/10.5555/3306127.3331689
Kouvaros PLomuscio A(2017)Verifying fault-tolerance in parameterised multi-agent systemsProceedings of the 26th International Joint Conference on Artificial Intelligence10.5555/3171642.3171684(288-294)Online publication date: 19-Aug-2017
https://dl.acm.org/doi/10.5555/3171642.3171684
Kouvaros PLomuscio A(2016)Parameterised model checking for alternating-time temporal logicProceedings of the Twenty-second European Conference on Artificial Intelligence10.3233/978-1-61499-672-9-1230(1230-1238)Online publication date: 29-Aug-2016
https://dl.acm.org/doi/10.3233/978-1-61499-672-9-1230

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents