An Inductive Technique for Parameterised Model Checking of Degenerative Distributed Randomised Protocols

DOI10.1016/j.entcs.2009.08.007zbMath1339.68167OpenAlexW2146735017WikidataQ59675351 ScholiaQ59675351MaRDI QIDQ2810974

Douglas Graham, Muffy Calder, Alice Ann Miller

Publication date: 6 June 2016

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2009.08.007

zbMATH Keywords

probabilistic model checkingPRISMdegenerative systemsparameterised model checking

Mathematics Subject Classification ID

Graph theory (including graph drawing) in computer science (68R10) Specification and verification (program logics, model checking, etc.) (68Q60) Distributed systems (68M14) Network protocols (68M12) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items

A counter abstraction technique for verifying properties of probabilistic swarm systems

Uses Software

• PRISM

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Symmetry breaking in distributed networks
• Using SPIN to analyse the tree identification phase of the IEEE 1394 high-performance serial bus (FireWire) protocol
• Fun with fireWire: A comparative study of formal verification methods applied to the IEEE 1394 root contention protocol
• Fast randomized consensus using shared memory
• Symmetry Reduction for Probabilistic Model Checking Using Generic Representatives
• Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems
• Validation of Stochastic Systems