Reasoning about Smart Contracts via LTL Encoding

Smart contracts are programs that automatically execute on blockchains when some conditions are verified. They encode the legally relevant events needed to satisfy the terms of an agreement and are usually defined by using procedural languages, even if some recent proposals investigated the possibility of using logic formalisms. However, existing logic-based initiatives are rather limited since they only enable the formal checking of properties of a single smart contract, totally neglecting its possible interactions with other smart contracts running on the same blockchain. This paper proposes a framework, called SCRea, that works on a set of smart contracts specified as Linear Temporal Logic (LTL) formulas. SCRea enables to reason about smart contracts considered individually or by considering them as running cooperatively or competitively on the same blockchain.