PRISMisaprobabilisticmodelchecker,atoolforformalmodellingandanal- ysis of systems that exhibit random or probabilistic behaviour. We extend the language in order to model the Bitcoin system. The tool now supports three dynamic data types: block, ledger and list. As consequence, it is now possible to perform simulations and analyse transient probabilities, i.e. probabilities that are dependent on time, for the Bitcoin protocol. It has been used to under- stand how the system changes during the execution and to analyse the probabilities of reaching an inconsistent state in different settings.

Adele Veschetti, C.L. (2020). PRISM+.

PRISM+

Adele Veschetti;Cosimo Laneve
2020

Abstract

PRISMisaprobabilisticmodelchecker,atoolforformalmodellingandanal- ysis of systems that exhibit random or probabilistic behaviour. We extend the language in order to model the Bitcoin system. The tool now supports three dynamic data types: block, ledger and list. As consequence, it is now possible to perform simulations and analyse transient probabilities, i.e. probabilities that are dependent on time, for the Bitcoin protocol. It has been used to under- stand how the system changes during the execution and to analyse the probabilities of reaching an inconsistent state in different settings.
2020
Adele Veschetti, C.L. (2020). PRISM+.
Adele Veschetti, Cosimo Laneve
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/798128
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact