Eliminating message counters in synchronous threshold automata

DOI10.1007/978-3-030-67067-2_10MaRDI QIDQ2234072zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Eliminating Message Counters in Threshold Automata
• Complexity of Verification and Synthesis of Threshold Automata
• SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms
• \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
• Synthesis of distributed algorithms with parameterized threshold guards

Cites work

• scientific article; zbMATH DE number 996442 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• scientific article; zbMATH DE number 3408928 (Why is no real title available?)
• scientific article; zbMATH DE number 7649941 (Why is no real title available?)
• A Reduction Theorem for the Verification of Round-Based Distributed Algorithms
• A logic-based framework for verifying consensus algorithms
• A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
• Communication-closed asynchronous protocols
• Cutoff bounds for consensus algorithms
• Impossibility of distributed consensus with one faulty process
• Linear quantifier elimination as an abstract decision procedure
• On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
• On the completeness of verifying message passing programs under bounded asynchrony
• Parameterized model checking of synchronous distributed algorithms by abstraction
• Reachability in parameterized systems: all flavors of threshold automata
• Synchronizing the asynchronous
• Synchronous consensus under hybrid process and link failures

Cited in

(5)

• Higher-order quantifier elimination, counter simulations and fault-tolerant systems
• Complexity of Verification and Synthesis of Threshold Automata
• Eliminating Message Counters in Threshold Automata
• Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
• Verification of threshold-based distributed algorithms by decomposition to decidable logics

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

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