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

TL;DR

This paper provides guidelines for creating concise, readable LNT models, demonstrated through formal models of the Algorand consensus protocol, achieving significant code reduction and verification of properties.

Contribution

It introduces methods to optimize LNT model conciseness and readability, exemplified by a formal Algorand protocol model with improved efficiency.

Findings

LNT models can be made three times shorter with proper transformations.

Readability of LNT models is significantly improved.

Properties of the Algorand model are verified using multiple formal methods.

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.