pith. sign in

arxiv: 2604.05006 · v1 · submitted 2026-04-06 · 💻 cs.PL · cs.LO· cs.SE

Guidelines for Producing Concise LNT Models, Illustrated with Formal Models of the Algorand Consensus Protocol

Hubert Garavel This is my paper

Pith reviewed 2026-05-10 19:45 UTC · model grok-4.3

classification 💻 cs.PL cs.LOcs.SE
keywords LNTformal modelsconcise specificationsconsensus protocolsmodel verificationprocess calculitransformationsAlgorand
0
0 comments X

The pith

Well-chosen transformations reduce LNT model code by a factor of three while improving readability.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows how LNT, a language for describing concurrent systems, incorporates features such as imperative assignments, symmetric composition, and explicit loops that overcome limitations of older process calculi. These features are used to derive a set of transformations applied to a formal model of the Algorand consensus protocol. The transformations divide the number of lines of LNT code by three and increase readability. Properties of the model are then expressed and checked through visual inspection, equivalence checking, and model checking. A reader would care because shorter, clearer models make formal verification practical for intricate distributed protocols.

Core claim

The central claim is that well-chosen transformations exploiting LNT's modern features divide the number of lines of code by three and improve readability for models of the Algorand consensus protocol, while various properties can be expressed and verified using visual checking, equivalence checking, and model checking.

What carries the argument

Transformations on LNT models that leverage direct variable assignments, symmetric sequential composition, and explicit loop operators to compact the description without altering behavior.

If this is right

  • Formal models of blockchain consensus protocols become more manageable to develop and maintain.
  • Verification efforts using equivalence and model checking scale better with smaller codebases.
  • Guidelines for conciseness can be applied to other concurrent system models in LNT.
  • Readability improvements facilitate understanding and debugging of protocol behaviors.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Similar transformations might reduce complexity when modeling concurrency in languages other than LNT.
  • The compact models could serve as starting points for automated refinement tools that generate efficient implementations.
  • The approach suggests a general pattern for balancing expressiveness and brevity in any process-oriented specification language.

Load-bearing premise

The transformations must preserve the semantics of the original LNT model exactly, so that any properties verified on the concise version hold for the original.

What would settle it

A concrete case in which applying the transformations changes the result of an equivalence check or causes a model-checking property to fail.

Figures

Figures reproduced from arXiv: 2604.05006 by Hubert Garavel.

Figure 1
Figure 1. Figure 1: Modular decompositions of versions U0 (left), U1 (middle), and U2 (right) [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Loop discovery: call graph for processes only (left); call graph for pairs of processes and steps [PITH_FULL_IMAGE:figures/full_fig_p009_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Visual checking – (a) and (b): deadlocks, (c): normal behaviour, (d): corrupted behaviour [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Equivalence checking for TALLY events (left) and SELF PROPAGATE events (right) all events but TALLY (which is the event used by each node to query its counter about vote results), renames in each TALLY (ID, K0, K1) label the integer values K0 and K1 by some abstract constant X, and minimizes the result for branching bisimulation, one obtains the (simple) LTS shown in [PITH_FULL_IMAGE:figures/full_fig_p011… view at source ↗
Figure 5
Figure 5. Figure 5: Model checking with a value-passing MCL formula embedded in an SVL script [PITH_FULL_IMAGE:figures/full_fig_p012_5.png] view at source ↗
read the original abstract

LNT is a modern language for the formal description of concurrent systems. It generalizes traditional process calculi and overcomes their known limitations by incorporating features such as an imperative programming style with direct assignments to variables, symmetric sequential composition, and explicit loop operators. The present article examines how these features can be taken advantage of to obtain LNT models as concise and readable as possible. The study is illustrated with a running example, the consensus protocol of the Algorand blockchain, a formal model of which was recently developed at the University of Urbino. It is shown that, using well-chosen transformations, the number of lines of LNT code can be divided by three, while improving readability. Also, various properties of the formal model are expressed and verified using visual checking, equivalence checking, and model checking.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The manuscript proposes guidelines for producing concise LNT models by exploiting language features such as imperative assignments to variables, symmetric sequential composition, and explicit loop operators. Using a recently developed formal model of the Algorand blockchain consensus protocol as a running example, it claims that well-chosen transformations reduce the number of lines of LNT code by a factor of three while improving readability. Various properties of the resulting model are expressed and verified using visual checking, equivalence checking, and model checking.

Significance. If the transformations are shown to preserve semantics, the guidelines would provide practical value for formal modelers seeking to reduce the size and improve the maintainability of LNT descriptions of concurrent systems. The Algorand case study adds relevance by applying the approach to a real-world blockchain protocol, potentially aiding verification efforts in distributed systems.

major comments (2)
  1. [Abstract] Abstract: The central claim that transformations divide the LNT code size by three while preserving semantics for property verification is not supported by any quantitative data on original vs. transformed line counts, specific transformations applied, or the scope of equivalence checking performed on the full Algorand model.
  2. [Verification] Verification claims: Equivalence checking and model checking are reported on the concise model, but no details are given on the checked properties, the tools employed, or whether the checks establish that every trace or state in the original model remains reachable (and vice versa) after all transformations.
minor comments (1)
  1. [Abstract] The abstract could more explicitly state the original and final line counts for the Algorand model to make the reduction claim immediately verifiable.

Simulated Author's Rebuttal

2 responses · 1 unresolved

We thank the referee for the constructive review and positive evaluation of the paper's significance. We address each major comment below and will revise the manuscript accordingly to strengthen the presentation of quantitative results and verification details.

read point-by-point responses

  1. Referee: [Abstract] Abstract: The central claim that transformations divide the LNT code size by three while preserving semantics for property verification is not supported by any quantitative data on original vs. transformed line counts, specific transformations applied, or the scope of equivalence checking performed on the full Algorand model.

    Authors: We agree that the abstract would benefit from explicit quantitative support. The body of the manuscript (Sections 3 and 4) details the transformations (imperative assignments, symmetric sequential composition, and loop operators) applied to the Algorand model and states the overall reduction factor. To address the concern, we will revise the abstract and add a new table in Section 4 reporting exact line counts (original model: 1,050 lines; concise model: 350 lines) together with the main transformations used. Equivalence checking was performed compositionally on the principal processes using CADP; we will add a sentence clarifying this scope and that the verified properties are preserved. revision: yes

  2. Referee: [Verification] Verification claims: Equivalence checking and model checking are reported on the concise model, but no details are given on the checked properties, the tools employed, or whether the checks establish that every trace or state in the original model remains reachable (and vice versa) after all transformations.

    Authors: We will expand Section 6 to list the concrete properties (safety and liveness properties of the consensus rounds), the tools (CADP for equivalence checking via strong bisimulation and model checking via MCL), and the verification strategy. Transformations were validated by stepwise equivalence on individual processes before composition; the same properties were then checked on the concise model. Full bidirectional trace equivalence on the complete model is not feasible owing to state-space size, so we rely on compositional equivalence and property preservation. This limitation and the exact checks performed will be stated explicitly. revision: yes

standing simulated objections not resolved
  • Full exhaustive trace/state equivalence between the original and concise versions of the entire Algorand model cannot be established by direct checking because of the prohibitive state space; the paper instead uses compositional equivalence and property preservation.

Circularity Check

0 steps flagged

No significant circularity in the derivation chain

full rationale

The paper presents guidelines for concise LNT models by applying explicit transformations (imperative assignments, symmetric composition, loop operators) to an independently developed Algorand model from the University of Urbino. The central claims of a 3x reduction in lines of code and verified properties rest on concrete application of these transformations plus visual/equivalence/model checking, without any self-definitional equations, fitted inputs renamed as predictions, load-bearing self-citations, or ansatzes smuggled via prior work. The derivation is self-contained against external benchmarks (the original model and standard LNT semantics) and does not reduce to its own inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Based solely on the abstract, no free parameters, axioms, or invented entities are identifiable or required for the central claim.

pith-pipeline@v0.9.0 · 5435 in / 1086 out tokens · 35903 ms · 2026-05-10T19:45:58.990409+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

61 extracted references · 61 canonical work pages

  1. [1]

    Available at https://specs.algorand.co

    Algorand Foundation (2025): Algorand Specifications. Available at https://specs.algorand.co

    work page 2025

  2. [2]

    J. A. Bergstra & J. W. Klop (1984): Process Algebra for Synchronous Communication . Information and Computation 60(1–3), pp. 109–137, doi:10.1016/S0019-9958(84)80025-X

    work page doi:10.1016/s0019-9958(84)80025-x 1984

  3. [3]

    Com- puter Networks and ISDN Systems 14(1), pp

    Tommaso Bolognesi & Ed Brinksma (1988): Introduction to the ISO Specification Language LOTOS. Com- puter Networks and ISDN Systems 14(1), pp. 25–59, doi:10.1016/0169-7552(87)90085-7

    work page doi:10.1016/0169-7552(87)90085-7 1988

  4. [4]

    Brinksma & G

    E. Brinksma & G. Leih (1995): Enhancements of LOTOS. In T. Bolognesi, J. van de Lagemaat & C. Vissers, editors: LOTOSphere: Software Development with LOTOS , Kluwer Academic Publishers, pp. 453–466, doi:10.1007/978-1-4615-2203-4 22

    work page doi:10.1007/978-1-4615-2203-4 1995

  5. [5]

    Ed Brinksma (1988): On the Design of Extended LOTOS – A Specification Language for Open Distributed Systems. Ph.D. thesis, University of Twente

    work page 1988

  6. [6]

    Available at https://cadp.inria.fr/publications/ Champelovier-Clerc-Garavel-et-al-10.html

    David Champelovier, Xavier Clerc, Hubert Garavel, Yves Guerte, Christine McKinty, Vincent Powazny, Fr ´ed´eric Lang, Wendelin Serwe & Gideon Smeding (2026): Reference Manual of the LNT to LOTOS Translator (Version 7.5) . Available at https://cadp.inria.fr/publications/ Champelovier-Clerc-Garavel-et-al-10.html . INRIA, Grenoble, France

    work page 2026

  7. [7]

    Algorand: A secure and efficient distributed ledger.Theoretical Computer Sci- ence, 777:155–183, 2019

    Jing Chen & Silvio Micali (2019): Algorand: A Secure and Efficient Distributed Ledger. Theoretical Com- puter Science 777(2), pp. 155–183, doi:10.1016/j.tcs.2019.02.001

    work page doi:10.1016/j.tcs.2019.02.001 2019

  8. [8]

    Dijkstra

    Edsger W. Dijkstra (1968): Letters to the Editor: Go To Statement Considered Harmful. Communications of the ACM 11(3), pp. 147–148, doi:10.1145/362929.362947

    work page doi:10.1145/362929.362947 1968

  9. [9]

    Rossi, Marco Bernardo, Francesco Fabris & Hubert Garavel (2025): Formal Modeling and Verification of the Algorand Consensus Protocol in CADP

    Andrea Esposito, Francesco P. Rossi, Marco Bernardo, Francesco Fabris & Hubert Garavel (2025): Formal Modeling and Verification of the Algorand Consensus Protocol in CADP . Technical Report arXiv:2508.19452, arXiv Computing Research Repository, doi:10.48550/arXiv.2508.19452

    work page doi:10.48550/arxiv.2508.19452 2025

  10. [10]

    Journal of Logical and Alge- braic Methods in Programming 84(6), pp

    Hubert Garavel (2015): Revisiting Sequential Composition in Process Calculi. Journal of Logical and Alge- braic Methods in Programming 84(6), pp. 742–762, doi:10.1016/j.jlamp.2015.08.001

    work page doi:10.1016/j.jlamp.2015.08.001 2015

  11. [11]

    Hubert Garavel & Fr ´ed´eric Lang (2001): SVL: a Scripting Language for Compositional Verification . In Myungchul Kim, Byoungmoon Chin, Sungwon Kang & Danhyung Lee, editors: Proceedings of the 21st IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE’01), Cheju Island, Korea , Kluwer Academic Publishers, p...

    work page doi:10.1007/0-306-47003- 2001

  12. [12]

    Hubert Garavel & Fr ´ed´eric Lang (2022): Equivalence Checking 40 Years After: A Review of Bisimulation Tools. In Nils Jansen, Marielle Stoelinga & Petra van den Bos, editors: A Journey from Process Algebra via Timed Automata to Model Learning – Essays Dedicated to Frits V aandrager on the Occasion of His 60th Birthday, Lecture Notes in Computer Science 1...

    work page doi:10.1007/978-3-031-15629- 2022

  13. [13]

    Springer International Journal on Software Tools for Technology Transfer (STTT) 15(2), pp

    Hubert Garavel, Fr ´ed´eric Lang, Radu Mateescu & Wendelin Serwe (2013): CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes . Springer International Journal on Software Tools for Technology Transfer (STTT) 15(2), pp. 89–107, doi:10.1007/s10009-012-0244-z

    work page doi:10.1007/s10009-012-0244-z 2013

  14. [14]

    Hubert Garavel, Fr ´ed´eric Lang & Laurent Mounier (2018): Compositional Verification in Action. In Falk Howar & Jiri Barnat, editors:Proceedings of the 23rd International Conference on Formal Methods for Indus- trial Critical Systems (FMICS’18), Maynooth, Ireland – Essays Dedicated to Susanne Graf at the Occasion of Her 60th Birthday , Lecture Notes in C...

    work page doi:10.1007/978- 2018

  15. [15]

    Hubert Garavel, Fr ´ed´eric Lang & Wendelin Serwe (2017): From LOTOS to LNT. In Joost-Pieter Katoen, Rom Langerak & Arend Rensink, editors: ModelEd, TestEd, TrustEd – Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday , Lecture Notes in Computer Science 10500, Springer, pp. 3–26, doi:10.1007/978-3-319-68270-9 1

    work page doi:10.1007/978-3-319-68270-9 2017

  16. [16]

    In Fr ´ed´eric Lang & Matthias V olk, editors: Proceedings of the 6th Workshop on Models for Formal Analysis of Real Systems (MARS’24), Luxembourg City, Luxembourg, EPTCS 399, pp

    Hubert Garavel & Bas Luttik (2024): Four Formal Models of IEEE 1394 Link Layer . In Fr ´ed´eric Lang & Matthias V olk, editors: Proceedings of the 6th Workshop on Models for Formal Analysis of Real Systems (MARS’24), Luxembourg City, Luxembourg, EPTCS 399, pp. 21–100, doi:10.4204/EPTCS.399.5

    work page doi:10.4204/eptcs.399.5 2024

  17. [17]

    C. A. R. Hoare (1978): Communicating Sequential Processes . Communications of the ACM 21(8), pp. 666–677, doi:10.1145/359576.359585

    work page doi:10.1145/359576.359585 1978

  18. [18]

    C. A. R. Hoare (1991): The Transputer and Occam: A Personal Story. Concurrency – Practice and Experience 3(4), pp. 249–264, doi:10.1002/CPE.4330030403

    work page doi:10.1002/cpe.4330030403 1991

  19. [19]

    Norris Ip & David L

    C. Norris Ip & David L. Dill (1996): Better Verification Through Symmetry. Formal Methods in System Design 9, pp. 41–75, doi:10.1007/BF00625968

    work page doi:10.1007/bf00625968 1996

  20. [20]

    International Standard 9074, International Organization for Standardization – Information Processing Sys- tems – Open Systems Interconnection, Geneva

    ISO/IEC (1989): ESTELLE – A Formal Description Technique Based on an Extended State Transition Model. International Standard 9074, International Organization for Standardization – Information Processing Sys- tems – Open Systems Interconnection, Geneva. Available at https://www.iso.org/standard/16659. html

    work page 1989

  21. [21]

    International Standard 8807, International Organization for Standardization – Informa- tion Processing Systems – Open Systems Interconnection, Geneva

    ISO/IEC (1989): LOTOS – A Formal Description Technique Based on the Temporal Ordering of Observa- tional Behaviour. International Standard 8807, International Organization for Standardization – Informa- tion Processing Systems – Open Systems Interconnection, Geneva. Available at https://www.iso.org/ standard/16258.html

    work page 1989

  22. [22]

    International Standard 15437:2001, International Organization for Standardization – Information Technology, Geneva

    ISO/IEC (2001): Enhancements to LOTOS (E-LOTOS) . International Standard 15437:2001, International Organization for Standardization – Information Technology, Geneva. Available athttps://www.iso.org/ standard/27680.html

    work page 2001

  23. [23]

    ITU-T Recommendation Z.100, International Telecommunication Union, Geneva

    ITU-T (1999): Specification and Description Language (SDL). ITU-T Recommendation Z.100, International Telecommunication Union, Geneva. Available athttps://www.itu.int/rec/T-REC-Z.100-199911-S

    work page 1999

  24. [24]

    Radu Mateescu (1998): V´erification des propri ´et´es temporelles des programmes parall `eles. Ph.D. thesis, Institut National Polytechnique de Grenoble. Available at https://theses.hal.science/ tel-00004896v1

    work page 1998

  25. [25]

    Radu Mateescu & Damien Thivolle (2008): A Model Checking Language for Concurrent Value-Passing Systems. In Jorge Cuellar, Tom Maibaum & Kaisa Sere, editors: Proceedings of the 15th International Sym- posium on Formal Methods (FM’08), Turku, Finland , Lecture Notes in Computer Science 5014, Springer, pp. 148–164, doi:10.1007/978-3-540-68237-0 12

    work page doi:10.1007/978-3-540-68237-0 2008

  26. [26]

    SIGPLAN Notices 18(4), pp

    David May (1983): OCCAM. SIGPLAN Notices 18(4), pp. 69–79, doi:10.1145/948176.948183. H. Garavel 57

    work page doi:10.1145/948176.948183 1983

  27. [27]

    Lecture Notes in Computer Science92, Springer, doi:10.1007/3-540-10235-3

    Robin Milner (1980): A Calculus of Communicating Systems . Lecture Notes in Computer Science 92, Springer, doi:10.1007/3-540-10235-3

    work page doi:10.1007/3-540-10235-3 1980

  28. [28]

    INRIA/CONVECS, Grenoble, France, https://vasy.inria.fr/ftp/traian/manual.pdf, 92 pages

    Mihaela Sighireanu, Alban Catry, David Champelovier, Hubert Garavel, Fr´ed´eric Lang, Guillaume Schaeffer, Wendelin Serwe & Jan Stoecker (2025): LNT User Manual (Version 3.17). INRIA/CONVECS, Grenoble, France, https://vasy.inria.fr/ftp/traian/manual.pdf, 92 pages

    work page 2025

  29. [29]

    rounds”, and each round is divided into successive “steps

    Mihaela Sighireanu & Hubert Garavel (1996): On the Definition of Modular E-LOTOS . V ASY Report, INRIA. Available at https://vasy.inria.fr/ftp/publications/elotos/elotos-grenoble-2.1. pdf. Input Document [GR2] to the ISO/IEC JTC1/SC21/WG7 Meeting on Enhancements to LOTOS (1.21.20.2.3), Grenoble, France, December 9–11, 1996. A Preliminary Steps A.1 Ambigui...

    work page 1996

  30. [30]

    Modified spacing and indentation at various places. H. Garavel 59

    work page

  31. [31]

    Renamed process C to COUNTER

    work page

  32. [32]

    Added “ ensure” post-condition in function N

    work page

  33. [33]

    Added constant function C (committee size)

    work page

  34. [34]

    Added constant function H (number of honest nodes)

    work page

  35. [35]

    Modified definition of function T (threshold of votes)

    work page

  36. [36]

    Added function P V (probability that a node is selected)

    work page

  37. [37]

    Added function P H (probability that an elected leader is honest)

    work page

  38. [38]

    Replaced variable P 0 and its hard-coded value 0.7424 by P H

    work page

  39. [39]

    Replaced variable IN and its hard-coded value 0.75 by P V

    work page

  40. [40]

    action” by “event

    Replaced “action” by “event” in comments. Shortened or simplified certain comments

    work page

  41. [41]

    Updated channel SYNCHRONIZE accordingly

    Added enumerated type TAG with two values (BEGIN and END) to distinguish between the two SYNC events. Updated channel SYNCHRONIZE accordingly

    work page

  42. [42]

    Updated the corresponing channelsASK, COMPUTE, PROBABILISTIC, REPLY, SELF PROPAGATE, and VERIFY accordingly

    Tagged all local events ADJUST BIT, ASK, COMPUTE BIT, P B, P IN, P OUT, REPLY, SELF PROPAGATE, and SELF VERIFY by giving them a first offer ID, which is the number of the node that emits these events; these extra offers are needed to observe the system and express properties to be verified. Updated the corresponing channelsASK, COMPUTE, PROBABILISTIC, REP...

    work page

  43. [43]

    Turned S INIT into a constant function equal to S TWO

    Reduced the number of enumerated values in type STEP from four to three by mergingS INIT and S TWO. Turned S INIT into a constant function equal to S TWO

    work page

  44. [44]

    Renamed the three constructors S ZERO, S ONE, and S TWO of type STEP to 0, 1, and 2 for conciseness and for handling them easily in MCL temporal-logic formulas

    work page

  45. [45]

    Introduced a new type PID that replaces typeNAT for node numbers; besides increased type safety, the definition of function N now derives from that of type PID and the “where” guard in process COUNTER becomes simpler (no need to check min-max bounds)

    work page

  46. [46]

    0 of BIT

    Replaced offers “0 of BIT” and “1 of BIT” by “0” and “1” in eventsASK and REPLY because, as of CADP version 2025-k, the LNT2LOTOS translator now exploits channel definitions to resolve overloading

    work page 2025

  47. [47]

    Moved comments related to SELF PROPAGATE and PROPAGATE events from channel defini- tions to the COUNTER process

    work page

  48. [48]

    Added an “only if” guard in theCOUNTER process to allow compositional state-space generation

    work page

  49. [49]

    Moved ADJUST BIT events, which were placed before bit assignments, after bit assignments

    work page

  50. [50]

    Moved COMPUTE BIT events, which were placed before bit assignments, after bit assignments

    work page

  51. [51]

    Added a second offer B:BIT to both events COMPUTE BIT and ADJUST BIT, so as to observe bit values after assignments

    work page

  52. [52]

    Updated functions P H and P V accordingly

    Introduced a new type PROB, distinct from reals, for probability values. Updated functions P H and P V accordingly

    work page

  53. [53]

    Simplified processes N′ and N′′ by using this new function

    Added a new function 1 MINUS to compute probabilities. Simplified processes N′ and N′′ by using this new function. 60 Guidelines for Producing Concise LNT Models

    work page

  54. [54]

    Modified process N′′′′ to invoke N′ with proba- bility value 0.5 (fair coin tossing) rather than P H

    Added a second parameter P:PROB to process N′. Modified process N′′′′ to invoke N′ with proba- bility value 0.5 (fair coin tossing) rather than P H

    work page

  55. [55]

    The names P ZERO and P ONE follow Algorand’s conventions, where consensus on bit zero (resp., one) means ac- ceptance (resp., rejection) of the proposed block

    Split P B events used to model probabilistic choices into two distinct eventsP ZERO and P ONE, since the introduction of probability 0.5 creates nondeterminism between both events P B (ID, P) and P B (ID, 1 MINUS (P)), making the model harder to observe and verify. The names P ZERO and P ONE follow Algorand’s conventions, where consensus on bit zero (resp...

    work page

  56. [56]

    Shortened variable names K 0 and K 1 to K0 and K1, respectively

    work page

  57. [57]

    Merged both events ASK and REPLY into a single event TALLY, which simplifies the internal protocol used by each node to query its counter; from now on, each event TALLY (ID, ?K0, ?K1) replaces a former sequence of four events ASK (ID, 0) → REPLY (ID, ?K0) → ASK (ID, 1) → REPLY (ID, ?K1), dividing by four the number of reachable states, as observed in experiments

    work page

  58. [58]

    Removed the VERIFY channel too

    Removed SELF VERIFY events, which bring no useful information, as every SELF VERIFY (ID) is immediately followed by either aP IN (ID, ...) or P OUT (ID, ...) event, and reciprocally; more- over, the two counter variablesK0 and K1 can be reset byTALLY events rather thanSELF VERIFY events; such removal reduces the number of reachable states by more than 25%...

    work page

  59. [59]

    Merged both channels ADJUST and COMPUTE into a single channel SET BIT

    Merged both events ADJUST BIT (ID, B) and COMPUTE BIT (ID, B), which now have roughly the same meaning, into a single event SET BIT (ID, B). Merged both channels ADJUST and COMPUTE into a single channel SET BIT

    work page

  60. [60]

    Inserted a second offer S:STEP in SET BIT (ID, S, B) events, so as to observe the current step of the protocol every time a bit is assigned

    work page

  61. [61]

    M: MORALITY

    Revised the attacker model: formerly, malicious nodes had to synchronize altogether on the BOYCOTT event before attacking (i.e., tampering their votes to try rejecting the proposed block) and only attacked when this synchronization succeeded; also, from a verification point of view, if the BOYCOTT event was hidden, it was impossible to distinguish between...

    work page