|
|
|---|
|
|
|
|---|
Definition of the AleoBFT labeled state transition system.
We model the protocol as a labeled state transition system, according to the standard definition of that notion in the literature. We define the possible states of the system, the possible events of the system, the possible initial states, and the possible transitions by which an event takes a state to a new state (the events `label' the transitions between states).