Accuracy of message counting abstraction in fault-tolerant distributed algorithms

DOI10.1007/978-3-319-52234-0_19zbMATH Open1484.68321OpenAlexW2568409254MaRDI QIDQ2961576FDOQ2961576

Authors:

Publication date: 21 February 2017

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

Full work available at URL: http://resolver.obvsg.at/urn:nbn:at:at-ubtuw:3-2936

Recommendations

• Theorem Proving in Higher Order Logics
• Parameterized model checking of synchronous distributed algorithms by abstraction
• A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
• SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms
• Tutorial on parameterized model checking of fault-tolerant distributed algorithms

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Distributed algorithms (68W15)

Cites Work

• A theory of timed automata
• All for the price of few (parameterized verification through view abstraction)
• Counterexample-guided abstraction refinement for symbolic model checking
• Title not available (Why is that?)
• Reconciling fault-tolerant distributed computing and systems-on-chip
• Impossibility of distributed consensus with one faulty process
• Reaching Agreement in the Presence of Faults
• Analysis of timed systems using time-abstracting bisimulations
• Title not available (Why is that?)
• Efficient on-the-fly algorithm for checking alternating timed simulation
• Asynchronous consensus and broadcast protocols
• The Theta-Model: achieving synchrony without clocks
• Booting clock synchronization in partially synchronous systems with hybrid process and link failures
• Parameterized model checking of rendezvous systems
• Bosco: One-Step Byzantine Asynchronous Consensus
• The theory of timed I/O automata
• Verification of consensus algorithms using satisfiability solving
• SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms
• A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
• Model checking of systems with many identical timed processes
• Liveness of parameterized timed networks
• Tight cutoffs for guarded protocols with fairness
• Counting constraints in flat array fragments
• A logic-based framework for verifying consensus algorithms
• What you always wanted to know about model checking of fault-tolerant distributed algorithms
• On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
• On Verifying Fault Tolerance of Distributed Protocols
• Uncovering symmetries in irregular process networks

Cited In (6)

• Ability to Count Messages Is Worth Θ(Δ) Rounds in Distributed Computing
• Reachability in parameterized systems: all flavors of threshold automata
• Counting protocols for reliable end-to-end transmission
• Parameterized model checking of networks of timed automata with Boolean guards
• Scalable eventually consistent counters over unreliable networks
• Synthesis of distributed algorithms with parameterized threshold guards

This page was built for publication: Accuracy of message counting abstraction in fault-tolerant distributed algorithms

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