A formal model for ledger management systems based on contracts and\n temporal logic

Abstract

A key component of blockchain technology is the ledger, viz., a database\nthat, unlike standard databases, keeps in memory the complete history of past\ntransactions as in a notarial archive for the benefit of any future test. In\nsecond-generation blockchains such as Ethereum the ledger is coupled with smart\ncontracts, which enable the automation of transactions associated with\nagreements between the parties of a financial or commercial nature. The\ncoupling of smart contracts and ledgers provides the technological background\nfor very innovative application areas, such as Decentralized Autonomous\nOrganizations (DAOs), Initial Coin Offerings (ICOs) and Decentralized Finance\n(DeFi), which propelled blockchains beyond cryptocurrencies that were the only\nfocus of first generation blockchains such as the Bitcoin. However, the\ncurrently used implementation of smart contracts as arbitrary programming\nconstructs has made them susceptible to dangerous bugs that can be exploited\nmaliciously and has moved their semantics away from that of legal contracts. We\npropose here to recompose the split and recover the reliability of databases by\nformalizing a notion of contract modelled as a finite-state automaton with\nwell-defined computational characteristics derived from an encoding in terms of\nallocations of resources to actors, as an alternative to the approach based on\nprogramming. To complete the work, we use temporal logic as the basis for an\nabstract query language that is effectively suited to the historical nature of\nthe information kept in the ledger.\n