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.

翻译：LNT是一种用于并发系统形式描述的现代语言。它通过融入具有变量直接赋值的命令式编程风格、对称顺序组合以及显式循环运算符等特性，对传统进程演算进行了推广并克服了其已知局限性。本文探讨如何利用这些特性获得尽可能简洁易读的LNT模型。研究以Algorand区块链的共识协议作为连续案例进行说明，该协议的形式化模型近期由乌尔比诺大学开发。研究表明，通过选用恰当的转换方法，LNT代码行数可缩减至三分之一，同时提升可读性。此外，通过可视化检查、等价性检查及模型检查，对形式化模型的多项属性进行了表达与验证。