Eliminating message counters in synchronous threshold automata

DOI10.1007/978-3-030-67067-2_10zbMath1472.68094OpenAlexW3120283163MaRDI QIDQ2234072

Yanyan Li

Publication date: 18 October 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-67067-2_10

Mathematics Subject Classification ID

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

Related Items (1)

Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Synchronous consensus under hybrid process and link failures
• On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
• Cutoff bounds for consensus algorithms
• A Logic-Based Framework for Verifying Consensus Algorithms
• Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction
• A Reduction Theorem for the Verification of Round-Based Distributed Algorithms
• Impossibility of distributed consensus with one faulty process
• Reachability in Parameterized Systems: All Flavors of Threshold Automata
• A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
• Linear Quantifier Elimination as an Abstract Decision Procedure
• On the completeness of verifying message passing programs under bounded asynchrony
• Communication-closed asynchronous protocols

This page was built for publication: Eliminating message counters in synchronous threshold automata