Guidelines for Producing Concise LNT Models, Illustrated with Formal Models of the Algorand Consensus Protocol
Fuente:
arXiv
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866914450434424832 |
|---|---|
| author | Garavel, Hubert |
| author_facet | Garavel, Hubert |
| contents | 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.
|
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_05006 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Guidelines for Producing Concise LNT Models, Illustrated with Formal Models of the Algorand Consensus Protocol Garavel, Hubert Programming Languages Logic in Computer Science Software Engineering 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. |
| title | Guidelines for Producing Concise LNT Models, Illustrated with Formal Models of the Algorand Consensus Protocol |
| topic | Programming Languages Logic in Computer Science Software Engineering |
| url | https://arxiv.org/abs/2604.05006 |