State Machine - Algorand Specifications

Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Algorand Specifications

This specification defines the Algorand agreement protocol as a state machine. The input to the state machine is some serialization of events, which in turn results in some serialization of network transmissions from the state machine.

We can define the operation of the state machine as transitions between different states.

A transition NN maps some initial state S0, a ledger L0, and an event e to an output state S1, an output ledger L1, and a sequence of output network transmissions a=(a1,a2,…,an).

We write this as

N(S0,L0,e)=(S1,L1,a)

If no transmissions are output, we write that a=ϵ.

The state machine receives two types of events as inputs.

  1. message events: A message event is received when a vote, a proposal, or a bundle is received. A message event is simply written as the message that is received.

  2. timeout events: A timeout event is received when a specific amount of time passes after the beginning of a period. A timeout event λ seconds after a period p begins is denoted t(λ,p).

For more details on the way these events may be constructed from an implementation point of view, refer to the Algorand ABFT non-normative section.

The state machine produces a series of network transmissions as output. In each transmission, the player broadcasts a vote, a proposal, or a bundle to the rest of the network.

A player may perform a special broadcast called a relay. In a relay, the data received from another peer is broadcast to all peers except for the sender.

A broadcast action is simply written as the message to be transmitted. A relay action is written as the same message except with an asterisk. For instance, an action to relay a vote is written as Vote∗(r,p,s,v).

For implementation details on relay and broadcasting actions, refer to the Algorand Network non-normative section.