Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms

DOI10.1007/978-3-319-52234-0_19zbMath1484.68321OpenAlexW2568409254MaRDI QIDQ2961576

No author found.

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

Mathematics Subject Classification ID

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

Related Items

Synthesis of distributed algorithms with parameterized threshold guards, Reachability in Parameterized Systems: All Flavors of Threshold Automata, Parameterized model checking of networks of timed automata with Boolean guards

Cites Work

• Unnamed Item
• Unnamed Item
• Reconciling fault-tolerant distributed computing and systems-on-chip
• Verification of consensus algorithms using satisfiability solving
• A theory of timed automata
• SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms
• Model checking of systems with many identical timed processes
• Booting clock synchronization in partially synchronous systems with hybrid process and link failures
• The Theta-Model: achieving synchrony without clocks
• Tight Cutoffs for Guarded Protocols with Fairness
• Counting Constraints in Flat Array Fragments
• All for the Price of Few
• Uncovering Symmetries in Irregular Process Networks
• A Logic-Based Framework for Verifying Consensus Algorithms
• The Theory of Timed I/O Automata, Second Edition
• What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms
• Parameterized Model Checking of Rendezvous Systems
• On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability
• Liveness of Parameterized Timed Networks
• Counterexample-guided abstraction refinement for symbolic model checking
• Bosco: One-Step Byzantine Asynchronous Consensus
• Efficient on-the-fly Algorithm for Checking Alternating Timed Simulation
• Asynchronous consensus and broadcast protocols
• Impossibility of distributed consensus with one faulty process
• Reaching Agreement in the Presence of Faults
• A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
• On Verifying Fault Tolerance of Distributed Protocols
• Analysis of timed systems using time-abstracting bisimulations