Verification of population protocols

DOI10.1007/s00236-016-0272-3zbMath1364.68081OpenAlexW2424307510MaRDI QIDQ523133

Javier Esparza, Jérôme Leroux, Rupak Majumdar, Pierre Ganty

Publication date: 20 April 2017

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00236-016-0272-3

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Network protocols (68M12)

Related Items

A counter abstraction technique for verifying properties of probabilistic swarm systems, Unnamed Item, Advances in parameterized verification of population protocols, Unnamed Item, Finding Cut-Offs in Leaderless Rendez-Vous Protocols is Easy, Democratic, existential, and consensus-based output conventions in stable computation by chemical reaction networks, Parameterized Analysis of Immediate Observation Petri Nets, Population protocols: beyond runtime analysis, Computational Complexity of Atomic Chemical Reaction Networks, Unnamed Item, Expressive Power of Broadcast Consensus Protocols, Finding cut-offs in leaderless rendez-vous protocols is easy, Directed reachability for infinite-state systems, Automatic Analysis of Expected Termination Time for Population Protocols, Unnamed Item, Unnamed Item, The complexity of verifying population protocols, Robustness of Expressivity in Chemical Reaction Networks, Unnamed Item, A Survey on Analog Models of Computation

Uses Software

• Coq
• PAT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The computational power of population protocols
• Computation in networks of passively mobile finite-state sensors
• Fast computation by population protocols with a leader
• Semigroups, Presburger formulas, and languages
• Rational sets in commutative monoids
• Vector Addition System Reversible Reachability Problem
• Fast Computation by Population Protocols with a Leader
• Demystifying Reachability in Vector Addition Systems
• Vector Addition System Reversible Reachability Problem
• Stably computable predicates are semilinear
• Presburger Vector Addition Systems
• Automated Technology for Verification and Analysis
• Computation in networks of passively mobile finite-state sensors
• Well-structured transition systems everywhere!