Guidelines for Producing Concise LNT Models, Illustrated with Formal Models of the Algorand Consensus Protocol
This work provides incremental guidelines for researchers and practitioners in formal methods to improve model efficiency in specific domains like blockchain protocols.
The authors tackled the challenge of creating concise and readable LNT models for concurrent systems, demonstrating that applying specific transformations to a formal model of the Algorand consensus protocol reduced the lines of code by a factor of three while enhancing readability.
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.