Eliminating message counters in synchronous threshold automata

DOI10.1007/978-3-030-67067-2_10zbMATH Open1472.68094OpenAlexW3120283163MaRDI QIDQ2234072FDOQ2234072

Authors: Yanyan Li 

Publication date: 18 October 2021

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

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (4)

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