An inductive technique for parameterised model checking of degenerative distributed randomised protocols

DOI10.1016/J.ENTCS.2009.08.007MaRDI QIDQ2810974zbMATH OpenOpenAlexWikidataFDO

Authors Douglas Graham, M. Calder, Alice 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

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

Recommendations

• Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
• The probabilistic model checking landscape
• High-level modelling and efficient analysis of randomized protocols.
• Theoretical Aspects of Computing - ICTAC 2004
• P^5: planner-less proofs of probabilistic parameterized protocols

Cites work

• scientific article; zbMATH DE number 700091 (Why is no real title available?)
• scientific article; zbMATH DE number 1956507 (Why is no real title available?)
• scientific article; zbMATH DE number 2006656 (Why is no real title available?)
• scientific article; zbMATH DE number 3240812 (Why is no real title available?)
• Fast randomized consensus using shared memory
• Fun with fireWire: A comparative study of formal verification methods applied to the IEEE 1394 root contention protocol
• Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems
• Symmetry Reduction for Probabilistic Model Checking Using Generic Representatives
• Symmetry breaking in distributed networks
• Using SPIN to analyse the tree identification phase of the IEEE 1394 high-performance serial bus (FireWire) protocol
• Validation of Stochastic Systems

Cited in

(2)

• A counter abstraction technique for verifying properties of probabilistic swarm systems
• P^5: planner-less proofs of probabilistic parameterized protocols

Describes a project that uses

Uses Software

• PRISM

This page was built for publication: An inductive technique for parameterised model checking of degenerative distributed randomised protocols

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2810974)