C. Baier and J. P. Katoen, Principles of model checking, 2008.

M. Ben-or, Another advantage of free choice: Completely asynchronous agreement protocols (extended abstract), In: PODC. pp, pp.27-30, 1983.
DOI : 10.1145/800221.806707

G. Bracha, Asynchronous byzantine agreement protocols, Inf. Comput, vol.75, issue.2, pp.130-143, 1987.
DOI : 10.1016/0890-5401(87)90054-x
URL : https://doi.org/10.1016/0890-5401(87)90054-x

T. Elrad and N. Francez, Decomposition of distributed programs into communicationclosed layers, Sci. Comput. Program, vol.2, issue.3, pp.155-173, 1982.
DOI : 10.1016/0167-6423(83)90013-8
URL : https://doi.org/10.1016/0167-6423(83)90013-8

M. J. Fischer, N. A. Lynch, and M. S. Paterson, Impossibility of distributed consensus with one faulty process, J. ACM, vol.32, issue.2, pp.374-382, 1985.
DOI : 10.1145/588058.588060
URL : http://theory.lcs.mit.edu/tds/papers/Lynch/pods83-flp.pdf

I. Konnov, M. Lazic, H. Veith, and J. Widder, Para 2 : Parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms, Formal Methods in System Design, vol.51, issue.2, pp.270-307, 2017.
DOI : 10.1007/978-3-319-21690-4_6

I. Konnov, M. Lazi´clazi´c, H. Veith, and J. Widder, A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms, POPL. pp, pp.719-734, 2017.

I. Konnov, H. Veith, and J. Widder, On the completeness of bounded model checking for threshold-based distributed algorithms, Reachability. Information and Computation, vol.252, pp.95-109, 2017.

I. Konnov and J. Widder, Bymc: Byzantine model checker, ISoLA (3), vol.11246, pp.327-342, 2018.
DOI : 10.1007/978-3-030-03424-5_22
URL : https://hal.archives-ouvertes.fr/hal-01909653

M. Z. Kwiatkowska and G. Norman, Verifying randomized byzantine agreement, pp.194-209, 2002.
DOI : 10.1007/3-540-36135-9_13
URL : https://link.springer.com/content/pdf/10.1007%2F3-540-36135-9_13.pdf

M. Z. Kwiatkowska, G. Norman, and D. Parker, PRISM 4.0: Verification of probabilistic real-time systems, CAV. pp, pp.585-591, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00648035

M. Z. Kwiatkowska, G. Norman, and R. Segala, Automated verification of a randomized distributed consensus protocol using cadence SMV and PRISM, CAV. pp, pp.194-206, 2001.
DOI : 10.1007/3-540-44585-4_17

D. J. Lehmann and M. O. Rabin, On the advantages of free choice: A symmetric and fully distributed solution to the dining philosophers problem, POPL. pp, pp.133-138, 1981.

A. Mostéfaoui, H. Moumen, and M. Raynal, Randomized k-set agreement in crashprone and byzantine asynchronous systems, Theor. Comput. Sci, vol.709, pp.80-97, 2018.

U. Nestmann, R. Fuzzati, and M. Merro, Modeling consensus in a process calculus, CONCUR. pp, pp.393-407, 2003.
DOI : 10.1007/978-3-540-45187-7_26
URL : http://lamp.epfl.ch/~uwe/citations/nestmann.fuzzati.merro-concur03.pdf

Y. J. Song and R. Van-renesse, Bosco: One-step Byzantine asynchronous consensus, DISC. LNCS, vol.5218, pp.438-450, 2008.
DOI : 10.1007/978-3-540-87779-0_30
URL : http://www.cs.cornell.edu/projects/quicksilver/public_pdfs/52180438.pdf