Vol-3194/paper37
Jump to navigation
Jump to search
Paper
| Paper | |
|---|---|
 edit
| |
| description | |
| id | Vol-3194/paper37 |
| wikidataid | →Q117344946 |
| title | Reasoning about Smart Contracts via LTL Encoding |
| pdfUrl | https://ceur-ws.org/Vol-3194/paper37.pdf |
| dblpUrl | https://dblp.org/rec/conf/sebd/FiondaGM22 |
| volume | Vol-3194→Vol-3194 |
| session | → |
Reasoning about Smart Contracts via LTL Encoding
Reasoning about Smart Contracts via LTL Encoding
Valeria Fionda1 , Gianluigi Greco1 and Marco Antonio Mastratisi1
1
DeMaCS, University of Calabria, Italy
Abstract
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.
Keywords
Smart Contracts, Linear Temporal Logic, Reasoning
1. Introduction
Distributed Ledger Technologies (DLT) [1] offers an infrastructure for the synchronized and shared
management of data regulated via consensus algorithms. The blockchain is a particular type of DLT
in which values of data are stored in a “chain of blocks”. Examples of implementations of blockchain
are Bitcoin [5] and Ethereum [6] (exchange of cryptocurrency). DLTs allow for the deployment and
execution of smart contracts [7]: programs stored within the distributed register, that are automatically
executed when certain conditions occur. The effect of the execution of a smart contract may be the
alteration of the state of the register or the activation of other contracts. Some examples of smart contract
application include banking functions (e.g. Savings), decentralized markets (e.g. EtherMarket), prediction
markets (e.g., Augur,), distribution of music royalties (e.g., Ujo) and encoding of virtual property (e.g.,
a‘Ascribe).
Smart contracts in blockchains are typically programmed in a procedural language specific of the host
DLT platform, such as Solidity[8] for Ethereum, or general purpose such as Javascript, Java, Golang,
and Python. Some initiatives exist in the literature for the formalization of smart contracts using a logic
declarative language (e.g., [2, 3, 4]). However, they only enable the formal checking of the correctness
and some other properties of a single smart contract independently from the other smart contracts
running on the same blockchain and the state of the blockchain itself.
We try to fill this gap by focusing on the application of linear temporal logic on finite traces (LTL𝑓 )
[17], with past operators, as a high-level logical tool for the formalization, validation and resolution
of any conflicts in the execution of smart contracts running on the same blockchain infrastructure. In
our framework, called SCRea, each smart contract is characterized by a set of preconditions and an
effect, where effects are visible on the blockchain when the smart contract is activated or, at most, at
SEBD 2022: The 30th Italian Symposium on Advanced Database Systems, June 19-22, 2022, Tirrenia (PI), Italy
" fionda@mat.unical.it (V. Fionda); greco@mat.unical.it (G. Greco); mastratisi@mat.unical.it (M. A. Mastratisi)
� 0000-0002-7018-1324 (V. Fionda); 0000-0002-5799-6828 (G. Greco)
© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073
CEUR Workshop Proceedings (CEUR-WS.org)
�the subsequent time instant. SCRea will enable, given a set of smart contracts, to verify whether the
execution of each of them is compatible with the execution of the others. If so, the framework also allows
to establish a particular order of execution that ensures that the preconditions of each smart contract are
verified before its execution.
We also studied the applicability of SCRea for the identification of conflict situations at runtime by
dealing with one execution trace. In the domain of smart contracts, the term trace denotes a sequence
of events executed by a blockchain or a sequence of function or event invocations issued by one or
more smart contracts. The availability of information at runtime helps dynamic verification techniques
to mitigate one of the main obstacles in the analysis of smart contracts: the need to model a complex
blockchain execution environment.
The rest of the paper is organized as follows. In Section 2 we introduce some preliminary definitions.
The encoding of smart contracts in linear temporal logic is discussed in Section 3 while Section 4 reports
about reasoning problems that are enabled by our encoding. The SCRea framework is described in
Section 5 and Section 6 will conclude the paper.
2. Linear Temporal Logic on Finite Traces with Past Operators
Linear temporal logic, denoted by LTL, is a modal logic introduced in the 1970s [9, 10]. Since then, it has
found applications in several fields of artificial intelligence and computer science, including planning [11],
robotics and control theory [12], the management of business processes [13] and temporal querying of
data [14]. LTL is a modal logic whose modalities are temporal operators related to events that occur at
particular time instants on an ordered timeline. Classically, LTL formulas are interpreted on infinite
traces, but there are some applications where is more appropriate to focus on interpretations on finite
traces [16]. Indeed, a liner temporal logic endowed with this semantics, denoted by LTL𝑓 , has been
recently studied [15, 17, 18].
Syntax. Let’s 𝑉 be a set of propositional variables. An LTL𝑓 formula 𝜙 is built on variables in 𝑉 using
boolean connectives ∧, ∨, ¬ as well as a number of time operators of two categories: future and past
temporal operators. For our purposes we will focus on a specific fragment of LTL𝑓 which includes the
future operator X (next) and the past operators Y (previous), H (always in the past), P (in the past), S
(since). Moreover, we assume that the negation is atomic in 𝜙 in the sense that it is applied directly
only to propositional variables. More formally, the formula 𝜙 is constructed according to the following
grammar, where 𝑥 is any variable in 𝑉 :
𝜙 ::= 𝑥 | ¬𝑥 | (𝜙 ∧ 𝜙) | (𝜙 ∨ 𝜙) | 𝑋(𝜙) | 𝑌 (𝜙) | 𝐻(𝜙) | 𝑃 (𝜙) | (𝜙 𝑆 𝜙)
Semantics. A finite trace defined on the variables in 𝑉 is a sequence 𝜋 = 𝜋0 , 𝜋1 , ...𝜋𝑛−1 that associates
with each 𝑖 ∈ {0, 1, ...𝑛−1} a state 𝜋𝑖 ⊆ 𝑉 consisting of all propositional variables that are assumed to be
true in the time instant 𝑖. The length of 𝜋 (its number of time instants) is denoted by 𝑙𝑒𝑛(𝜋). Given a finite
trace 𝜋, we define that an LTL𝑓 formula 𝜙 evaluate true in 𝜋 at the time instant 𝑖 ∈ {0, 1, ...𝑙𝑒𝑛(𝜋)-1}
inductively as follows:
∙ 𝜋, 𝑖| = 𝑥 if and only if 𝑥 ∈ 𝜋𝑖 ;
∙ 𝜋, 𝑖| = ¬𝑥 if and only if 𝑥 ∈ / 𝜋𝑖 ;
∙ 𝜋, 𝑖| = (𝜙1 ∧ 𝜙2 ) if and only if 𝜋, 𝑖| = 𝜙1 and 𝜋, 𝑖| = 𝜙2 ;
∙ 𝜋, 𝑖| = (𝜙1 ∨ 𝜙2 ) if and only if 𝜋, 𝑖| = 𝜙1 or 𝜋, 𝑖| = 𝜙2 ;
∙ 𝜋, 𝑖| = 𝑋(𝜙′ ) if and only if 𝑖 < 𝑙𝑒𝑛(𝜋) − 1 and 𝜋, 𝑖 + 1| = 𝜙′ ;
∙ 𝜋, 𝑖| = 𝑌 (𝜙′ ) if and only if 𝑖 > 0 and 𝜋, 𝑖 − 1| = 𝜙′ ;
∙ 𝜋, 𝑖| = 𝐻(𝜙′ ) if and only if for each 𝑗 such that 0 ≤ 𝑗 ≤ 𝑖 it’s true that 𝜋, 𝑗| = 𝜙′ ;
∙ 𝜋, 𝑖| = 𝑃 (𝜙′ ) if and only if exists 𝑗 such that 0 ≤ 𝑗 ≤ 𝑖 and 𝜋, 𝑗| = 𝜙′ ;
�Table 1
Interpretation of temporal operators in the context of smart contracts and blockchains.
𝑥∈𝑉 the condition/action 𝑥 occurs
¬𝑥 | 𝑥 ∈ 𝑉 the condition/action 𝑥 does not occurs
(𝑥1 ∧ 𝑥2 ) the conditions/actions 𝑥1 and 𝑥2 occurs
(𝑥1 ∨ 𝑥2 ) the conditions/actions 𝑥1 or 𝑥2 occurs
𝑋(𝑥′ ) in the next step the condition/action 𝑥′ must apply/be executed
in the previous step the condition/action 𝑥′ must be valid/have
𝑌 (𝑥′ )
been executed
in the past there must be an instant in which the condition/action
𝑃 (𝑥′ )
𝑥′ was valid/was performed
in the past the condition/action 𝑥′ has been verified/has always
𝐻(𝑥′ )
been performed
in the past there is an instant in which 𝑥2 has been verified/
(𝑥1 𝑆 𝑥2 ) executed, and from that moment the condition/action 𝑥1 has
always been verified/executed
∙ 𝜋, 𝑖| = (𝜙1 𝑆 𝜙2 ) if and only if exists 𝑗 such that 0 ≤ 𝑗 ≤ 𝑖 and 𝜋, 𝑗| = 𝜙2 and for any k such
that 𝑗 ≤ 𝑘 ≤ 𝑖 it’s true that 𝜋, 𝑘| = 𝜙1 .
When 𝜋, 𝑛-1 |= 𝜙 we say that 𝜋 is a model of 𝜙 and 𝜙 is satisfiable.
3. Encoding Smart Contracts in Linear Temporal Logic
Our goal is to use the fragment of linear time logic on finite traces with past operators described in
the Section 2 to reason on smart contracts. From this perspective, the time operators are interpreted as
reported in Table 1. In our encoding, each smart contract is a pair ⟨𝑝, 𝑒⟩, where: (i) 𝑝 are the preconditions,
i.e. an LTL𝑓 formula using past operators only; (ii) 𝑒 is the effect, i.e. a propositional formula or an LTL𝑓
formula using future operators only. Since 𝑝 are the preconditions that activate the smart contract and 𝑒
the effect of its execution, the smart contract will be expressed by the LTL𝑓 formula 𝜙 = 𝐻(𝑝 → 𝑒), i.e.,
every time the preconditions 𝑝 occurs then the smart contract must be executed and, thus, its effect 𝑒
must be visible. In the smart contracts domain, a trace 𝜋 denotes a sequence of events executed by a
blockchain platform or a sequence of function or event invocations issued by one or more smart contracts.
If a trace 𝜋 satisfies a smart contract ⟨𝑝, 𝑒⟩ it means that it satisfies the LTL𝑓 formula 𝜙 = 𝐻(𝑝 → 𝑒)
encoding it.
Example 1. Let’s consider a simple smart contract within the sharing economy context to access
multimedia contents. The contract consists of the following clause: if a user requests a content for which
he has previously paid, that content must be transferred to him. The propositional variables encoding
events are: 𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡 (he user requests the content), 𝑝𝑎𝑦𝐶𝑜𝑛𝑡𝑒𝑛𝑡 (the user pays for the content)
and 𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡 (the content is transmitted to the user). The precondition of the smart contract
is 𝑝 = 𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡 ∧ 𝑃 (𝑝𝑎𝑦𝐶𝑜𝑛𝑡𝑒𝑛𝑡), that is when the user requires a content it must be checked
that he already payed for it. The effect is the transmission of the content to the user which is considered
to be made in the time instant immediately following the request: 𝑒 = 𝑋(𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡). The smart
contract will then be codified by the following formula: 𝜙 = 𝐻((𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡∧𝑃 (𝑝𝑎𝑦𝐶𝑜𝑛𝑡𝑒𝑛𝑡)) →
𝑋(𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡)).
�4. Reasoning about Smart Contracts
Using LTL𝑓 to encode smart contracts allows to reason over (group of) smart contracts by exploiting its
reasoning capabilities. In this section we will discuss several reasoning problems on smart contracts.
4.1. Reasoning Problems on a Single Smart Contract
In this section we discuss three reasoning problems that can be defined if considering a single smart
contract.
Model checking. A major issue when dealing with a smart contract is model verification or model
checking. The goal is to verify if a given trace 𝜋, encoding the events registered by a blockchain, is a
model of a given smart contract ⟨𝑝, 𝑒⟩ encoded by the formula LTL𝑓 𝜙 = 𝐻(𝑝 → 𝑒). This corresponds
to check whether the smart contract has been executed (i.e., the effects of its execution are visible on the
blockchain) every time its preconditions have been satisfyied. Checking if a trace is a model of a smart
contract can be done in polynomial time w.r.t the length of the formula 𝜙 [15].
Example 2. Let’s consider the smart contract discussed in Example 1 consisting in the LTL𝑓 for-
mula 𝜙 = 𝐻((𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡 ∧ 𝑃 (𝑝𝑎𝑦𝐶𝑜𝑛𝑡𝑒𝑛𝑡)) → 𝑋(𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡)) and the trace 𝜋1 =
{𝑝𝑎𝑦𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡}. It’s easy to see that 𝜋1 is a model of 𝜙. In-
stead, the trace 𝜋2 = {𝑝𝑎𝑦𝐶𝑜𝑛𝑡𝑒𝑛𝑡, 𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡} is not a model of 𝜙 since the precondition of the
smart contract is satisfied but the content is not transmitted to the user.
Satisfiability. Satisfiability is the problem of establishing whether a smart contract ⟨𝑝, 𝑒⟩ encoded by
the LTL𝑓 formula 𝜙 = 𝐻(𝑝 → 𝑒) admits a satisfying trace 𝜋 in which it has been executed at least once.
This corresponds to check whether the LTL𝑓 formula 𝑃 (𝑝) ∧ 𝐻(𝑝 → 𝑒) admits a model.
Example 3. The smart contract discussed in Example 1 is satisfiable, and examples of traces that satisfy
it are:
𝜋1 ={𝑝𝑎𝑦𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡}
𝜋2 ={𝑝𝑎𝑦𝐶𝑜𝑛𝑡𝑒𝑛𝑡, 𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡}
𝜋3 ={𝑝𝑎𝑦𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡}.
Satisfiability at runtime. Satisfiability at runtime is the problem of verifying whether a smart contract
⟨𝑝, 𝑒⟩ (encoded by the LTL𝑓 formula 𝜙 = 𝐻(𝑝 → 𝑒)) is satisfiable given a partial trace 𝜋𝑝 . In particular,
it is the problem of verifying whether there exists a completion 𝜋 = 𝜋𝑝 𝜋𝑡 of 𝜋𝑝 (obtained by adding to
𝜋𝑝 a subtrace 𝜋𝑡 consisting of a certain number of states) such that the trace 𝜋 obtained is a model of the
formula 𝑃 (𝑝) ∧ 𝐻(𝑝 → 𝑒).
Example 4. Consider again the smart contract discussed in Example 1 and the partial trace 𝜋𝑝 =
{𝑝𝑎𝑦𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡}. This smart contract can be satisfied at runtime starting from 𝜋𝑝 ,
and examples of completions of 𝜋𝑝 are:
𝜋1 ={𝑝𝑎𝑦𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡}
𝜋2 ={𝑝𝑎𝑦𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡}
4.2. Reasoning Problems on a Set of Smart Contracts
The previous section considered reasoning problems defined on individual smart contracts. It is also
interesting in the context of blockchains to consider problems defined on a set of smart contracts, which
are supposed to operate and interact in the same blockchain infrastructure.
Model checking. Given a set of smart contracts {⟨𝑝1 , 𝑒1 ⟩, ⟨𝑝2 , 𝑒2 ⟩, ..., ⟨𝑝𝑛 , 𝑒𝑛 ⟩} encoded by the LTL𝑓
formulas 𝜙1 = 𝐻(𝑝1 → 𝑒1 ), 𝜙2 = 𝐻(𝑝2 → 𝑒2 ),... , 𝜙𝑛 = 𝐻(𝑝𝑛 → 𝑒𝑛 ), the goal is to verify if a
given trace 𝜋 is a model of 𝜙1 , 𝜙2 , ..., 𝜙𝑛 . To this end, we can use the same approach used for the
model checking of a single smart contract, but defining appropriately the LTL𝑓 formula encoding the
�set. In particular, since no smart contracts must be violated by the trace, we can consider the formula
𝜙 = 𝜙1 ∧ 𝜙2 ∧ ... ∧ 𝜙𝑛 .
Example 5. Consider the smart contract consisting of the following clause: if a user shares a content that
has been previously transmitted to him, thus violating contractual terms, that user will be deleted from the
system. The propositional variables used for the encoding are: 𝑠ℎ𝑎𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡 (the user shares the con-
tent), 𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡 (the content is transmitted to the user) and 𝑑𝑒𝑙𝑒𝑡𝑒𝑈 𝑠𝑒𝑟 (the user is deleted from
the system). The precondition of the smart contract is 𝑝 = 𝑠ℎ𝑎𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡 ∧ 𝑃 (𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡). The
effect is the deletion of the user from the system which is considered to be made in the time instant immedi-
ately following the sharing 𝑒 = 𝑋(𝑑𝑒𝑙𝑒𝑡𝑒𝑈 𝑠𝑒𝑟). The smart contract is encoded by the following formula:
𝜙2 = 𝐻((𝑠ℎ𝑎𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡 ∧ 𝑃 (𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡)) → 𝑋(𝑑𝑒𝑙𝑒𝑡𝑒𝑈 𝑠𝑒𝑟)). If we consider that 𝜙2 and the
smart contract discussed in Example 1 (consisting of the LTL𝑓 formula 𝜙1 = 𝐻((𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡 ∧
𝑃 (𝑝𝑎𝑦𝐶𝑜𝑛𝑡𝑒𝑛𝑡)) → 𝑋(𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡))) are running on the same blockchain; we can perform
model checking by considering the LTL𝑓 formula 𝜙 = 𝜙1 ∧ 𝜙2 . Let’s consider the following trace: 𝜋 =
{𝑝𝑎𝑦𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡,
𝑠ℎ𝑎𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑑𝑒𝑙𝑒𝑡𝑒𝑈 𝑠𝑒𝑟}. It is easy to verify that 𝜋 satisfies 𝜙 and it’s compliant with the two
smart contracts formalized by it.
Consistency of a set of smart contracts. If we consider a set of smart contracts running on the
same blockchain, another relevant problem is to verify their consistency, i.e. if it is possible that all
smart contracts can sooner or later be executed or if they are incompatible with each other, meaning
that the execution of one of them makes another smart contract never executable. The goal is to
check if there is a trace 𝜋 in which all the smart contracts in the set have been executed at least
once. Let’s consider a set of smart contracts {⟨𝑝1 , 𝑒1 ⟩, ..., ⟨𝑝𝑛 , 𝑒𝑛 ⟩} encoded by the LTL𝑓 formulas
𝜙1 =𝐻(𝑝1 → 𝑒1 ), . . . , 𝜙𝑛 =𝐻(𝑝𝑛 → 𝑒𝑛 ). Then, the LTL𝑓 formula for consistency checking is 𝜙 =
𝑖∈{1,...,𝑛} (𝐻(𝑝𝑖 → 𝑒𝑖 ) ∧ 𝑃 (𝑝𝑖 )), that is, the conjunction of the formulas encoding the individual smart
⋀︀
contracts plus the check that the preconditions of each smart contract have been satisfied at least once
(using the 𝑃 (𝑝𝑖 ) subformulas).
Example 6. Consider the set of smart contracts discussed in Example 5. This set
of smart contracts is consistent, in fact we found a trace satisfying this set. Let:
𝜙′′1 =((𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝑠𝐶𝑜𝑛𝑡𝑒𝑛𝑡 ∧ 𝑃 (𝑝𝑎𝑦𝑠𝐶𝑜𝑛𝑡𝑒𝑛𝑡))→𝑋(𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝑠𝐶𝑜𝑛𝑡𝑒𝑛𝑡) and 𝜙′′2 =((𝑠ℎ𝑎𝑟𝑒𝑠𝐶𝑜𝑛𝑡𝑒𝑛𝑡 ∧
𝑃 (𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡)) → 𝑋(𝑑𝑒𝑙𝑒𝑡𝑒𝑈 𝑠𝑒𝑟). The LTL𝑓 formula allowing to check the con-
sistency of the set is: 𝜙 = 𝐻(𝜙′′1 ) ∧ 𝐻(𝜙′′2 ) ∧ 𝑃 (𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝑠𝐶𝑜𝑛𝑡𝑒𝑛𝑡 ∧ 𝑃 (𝑝𝑎𝑦𝑠𝐶𝑜𝑛𝑡𝑒𝑛𝑡)) ∧
𝑃 (𝑠ℎ𝑎𝑟𝑒𝑠𝐶𝑜𝑛𝑡𝑒𝑛𝑡 ∧ 𝑃 (𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡)). A trace that satisfies 𝜙 is the following: 𝜋 =
{𝑝𝑎𝑦𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑟𝑒𝑞𝑢𝑒𝑠𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑟𝑒𝑞𝑢𝑒𝑠𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡,
𝑠ℎ𝑎𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡} {𝑑𝑒𝑙𝑒𝑡𝑒𝑈 𝑠𝑒𝑟}.
Example 7. Consider the two smart contracts within the sharing economy environment
⟨𝑝1 =(𝑟𝑒𝑞𝑢𝑒𝑠𝑡𝐷𝑒𝑙𝑒𝑡𝑖𝑜𝑛 ∧ 𝐻(¬𝑛𝑜𝑡𝐷𝑒𝑙𝑒𝑡𝑎𝑏𝑙𝑒)), 𝑒1 =𝑑𝑒𝑙𝑒𝑡𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡⟩ and ⟨𝑝2 = (𝑟𝑒𝑞𝑢𝑒𝑠𝑡𝑃 𝑒𝑟𝑚𝑎𝑛𝑒𝑛𝑐𝑒 ∧
𝐻(¬𝑑𝑒𝑙𝑒𝑡𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡)), 𝑒2 =𝑛𝑜𝑡𝐷𝑒𝑙𝑒𝑡𝑎𝑏𝑙𝑒). The smart contract ⟨𝑝1 , 𝑒1 ⟩ establishes that if the owner of
a content ask for its deletion (𝑟𝑒𝑞𝑢𝑒𝑠𝑡𝐷𝑒𝑙𝑒𝑡𝑖𝑜𝑛) and previously such content has not been declared
not deletable (𝐻(¬𝑛𝑜𝑡𝐷𝑒𝑙𝑒𝑡𝑎𝑏𝑙𝑒)), the content is deleted from the system. Instead, the smart contract
⟨𝑝2 , 𝑒2 ⟩ states that if a content is requested to be made permanent in the system (𝑟𝑒𝑞𝑢𝑒𝑠𝑡𝑃 𝑒𝑟𝑚𝑎𝑛𝑒𝑛𝑐𝑒)
and has not been previously deleted (𝐻(¬𝑑𝑒𝑙𝑒𝑡𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡)) then it is marked as not deletable. It is easy
to see that this set of smart contracts is not consistent since the execution of one smart contract prevents
the precondition of the other to be ever satisfied.
Consistency at runtime. Consistency at runtime is the problem of checking if a set of smart contracts
{⟨𝑝1 , 𝑒1 ⟩, ..., ⟨𝑝𝑛 , 𝑒𝑛 ⟩} can be satisfied starting from a partial trace 𝜋𝑝 , that is to verify whether there
exists a completion 𝜋=𝜋𝑝 𝜋𝑡 of 𝜋𝑝 (obtained by adding to 𝜋𝑝 a subtrace 𝜋𝑡 ) such that all smart contracts
in the set are executed at least once. To solve such a problem the encoding of the set of smart contracts
in LTL𝑓 is the same as discussed for the standard consistency checking. However, the partial trace 𝜋𝑝
�Figure 1: SCRea conceptual architecture
must be completed by adding indicator variables 𝑓𝑖 to register the satisfaction of preconditions.
Example 8. Consider again the set of smart contracts discussed in Example 6 and the partial trace
𝜋𝑝 ={𝑝𝑎𝑦𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡}. The completion of 𝜋𝑝 corresponds to the addition of the indica-
tor variable 𝑓1 in the last state, i.e., 𝜋𝑝 ={𝑝𝑎𝑦𝐶𝑜𝑛𝑡𝑒𝑛𝑡}{𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡, 𝑓1 }. The set of smart contracts
is consistent at runtime starting from 𝜋𝑝 , and examples of completions of 𝜋𝑝 are:
𝜋1 ={𝑝𝑎𝑦𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡, 𝑓1 }, {𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡, 𝑠ℎ𝑎𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡, 𝑓2 }, {𝑑𝑒𝑙𝑒𝑡𝑒𝑈 𝑠𝑒𝑟}
𝜋2 ={𝑝𝑎𝑦𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡, 𝑓1 }, {𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡}, {𝑟𝑒𝑞𝑢𝑖𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡, , 𝑠ℎ𝑎𝑟𝑒𝐶𝑜𝑛𝑡𝑒𝑛𝑡,
𝑓1 , 𝑓2 }, {𝑡𝑟𝑎𝑛𝑠𝑚𝑖𝑡𝐶𝑜𝑛𝑡𝑒𝑛𝑡, 𝑑𝑒𝑙𝑒𝑡𝑒𝑈 𝑠𝑒𝑟}
5. SCRea: Smart Contracts Reasoner
In this section we introduce the Smart Contracts Reasoner (SCRea) that works on smart contracts
encoded in LTL𝑓 and exploits boolean satisfiability for solving the reasoning tasks introduced in the
previous section. The proposed reasoner is based on a SAT (boolean satisfiability) rewrite technique
that recalls the approach followed by (incremental) model checking methods for bounded LTL [19]. The
conceptual architecture of SCRea is shown in Figure 1. The input to the system is the LTL𝑓 formula
encoding a single smart contract or a group of smart contracts (see, Section 4).
The first component is the Parser which constructs the parse tree 𝑝𝑡(𝜙) associated with the input
formula 𝜙. Starting from the parse tree, the SAT rewriting technique rewrites 𝜙 into an equivalent
propositional formula Φ𝜙,𝑚 which is satisfiable if, and only if, 𝜙 can be satisfied by a model of maximum
length 𝑚. To verify if Φ𝜙,𝑚 is satisfiable, the reasoner can use any existing SAT solver (e.g., Glucose
[20]). In particular, 𝑝𝑡(𝜙) is given as input to the Encoder module which produces a SAT translation of
the formula by initially considering a model length 𝑚=1. Then, whenever no model of Φ𝜙 is found, 𝑚 is
doubled and the process is repeated until 𝑚 exceeds the upper limit 𝑛 given as input to the Encoder. If
the SAT solver finds a model 𝜎 for a SAT formula Φ𝜙,𝑚 , the Decoder module translates 𝜎 into a trace 𝜋
(having length at most 𝑚) which satisfies 𝜙. Note that 𝑛 is set by the user and could be less than the
minimum length of any model of 𝜙, so the reasoner acts as a correct, although not complete, solver.
5.1. Encoder and Decoder Modules
Given an LTL𝑓 formula representing one or a set of smart contracts, for its SAT encoding a crucial
role is played by the parse tree of a formula 𝑝𝑡(𝜙) = (𝑉, 𝐸, 𝜆) that is a tree (𝑉, 𝐸) with a node labeling
function 𝜆 : 𝑉 → {∧, ∨, 𝑋, 𝑌, 𝑃, 𝐻, 𝑆} ∪ {𝑥, ¬𝑥|𝑥 ∈ 𝑉𝜙 } inductively defined as follows:
∙ For any literal 𝑙 ∈ {𝑥, ¬𝑥} with 𝑥 ∈ 𝑉𝜙 , 𝑝𝑡(𝑙) = ({𝑟}, ∅, 𝜆) and 𝜆(𝑟) = 𝑙.
∙ If 𝑝𝑡(𝜙𝑖 )=(𝑉𝑖 , 𝐸𝑖 , 𝜆𝑖 ), with 𝑖 ∈ {1, 2}, it is an analysis tree having as root the vertex 𝑟𝑖 ∈ 𝑉𝑖 and if
𝑂 ∈ ∧, ∨ is a boolean connective or 𝑂 = 𝑆 then 𝑝𝑡(𝜙1 𝑂𝜙2 ) = ({𝑟} ∪ 𝑉1 ∪ 𝑉2 , {(𝑟, 𝑟1 ), (𝑟, 𝑟2 )} ∪
� 𝐸1 ∪ 𝐸2 , 𝜆) is the analysis tree which has as roots the new node 𝑟, with 𝑟1 and 𝑟2 as its two
children, and where 𝜆 is such that 𝜆(𝑟) = 𝑂 and its restriction on 𝑉𝑖 coincides with 𝜆𝑖 .
∙ If 𝑝𝑡(𝜙′ )=(𝑉 ′ , 𝐸 ′ , 𝜆′ ) is an analysis tree having the root 𝑟′ and if 𝑂 ∈ {𝑋, 𝑌, 𝑃, 𝐻} is a time
operator, then 𝑝𝑡(𝑂(𝜙′ ))=({𝑟} ∪ 𝑉 ′ , {(𝑟, 𝑟′ )} ∪ 𝐸 ′ , 𝜆) is the tree rooted in the new node 𝑟 whose
only child is 𝑟′ and where 𝜆 is such that 𝜆(𝑟)=𝑂 and its restriction on 𝑉 ′ coincides with 𝜆.
To explain the encoding approach used by the reasoner to construct Φ𝜙,𝑚 , let us first note that, given
a trace 𝜋, each node 𝑣 ∈ 𝑉 of the parse tree 𝑝𝑡(𝜙) = (𝑉, 𝐸, 𝜆) can easily be equipped with a set 𝑠𝑎𝑡(𝑣, 𝜋)
of all time instants in which the sub-formula 𝜙𝑣 associated with vertex 𝑣 holds in 𝜋. In particular,
such sets can be computed by structural induction on the parse tree according to the semantics of the
different temporal operators. Then, the basic idea we use to construct the formula Φ𝜙,𝑚 is to imitate
the construction of the sets 𝑠𝑎𝑡(𝑣, 𝜋). Formally, we first define the variables 𝑙[0], ..., 𝑙[𝑚 − 1] that will
be used to encode the last time instant of the model. Intuitively, Φ𝜙,𝑚 will be defined in such a way
that there exists an index 𝑖 ∈ {0, ..., 𝑚 − 1}, such that 𝑙[𝑗] evaluates true (respectively, false) whenever
𝑗 ≥ 𝑖 (respectively, 𝑗 < 𝑖). The instant 𝑖 indicates the last time instant of a model of 𝜙 – more formally,
whenever Φ𝜙,𝑚 is satisfiable, there exists a model of 𝜙 of length 𝑖 ≤ 𝑚. Then, we associate the variables
𝑠𝑣[0], ..., 𝑠𝑣[𝑚 − 1] to each node 𝑣 of 𝑝𝑡(𝜙). Intuitively, 𝑠𝑣[𝑖] is meant to check if the formula encoded in
the parse tree rooted at node 𝑣 is satisfied at instant 𝑖. In the following expressions, we use two additional
variables 𝑠𝑣[−1] and 𝑠𝑣[𝑚], whose value will actually be a constant that will be fixed depending on the
type of node 𝑣. ⋀︀𝑚−2
Then, the SAT encoding is the formula Φ𝜙,𝑚 = 𝑣∈𝑉 (Φ𝑣 ∧ 𝑠𝑟𝑜𝑜𝑡[𝑚-1] ∧ 𝑙[𝑚-1]) ∧ 𝑖=0 (𝑙[𝑖] →
⋀︀
⋀︀𝑚−2 𝑚−1
𝑙[𝑖 + 1]) ∧ 𝑖=0 (𝑙[𝑖] → 𝑣 (𝑠𝑣[𝑖] ↔ 𝑠𝑣[𝑖 + 1])) and, for all 𝑣 ∈ 𝑉 , Φ𝑣 = 𝑠𝑣[0] ↔ Φ0𝑣 𝑖=1 (¬𝑙[𝑖-1] →
⋀︀ ⋀︀
(𝑠𝑣[𝑖] ↔ Φ𝑣 )), where:
𝑖
∙ if 𝜆(𝑣) ∈ {𝑥, ¬𝑥}, then Φ𝑖𝑣 = 𝑣′ ∈𝑉,𝜆(𝑣′ )≡¬𝜆(𝑣) ¬𝑠𝑣 ′ [𝑖] ∧ 𝑣′ ∈𝑉,𝜆(𝑣′ )≡𝜆(𝑣) 𝑠𝑣 ′ [𝑖];
⋀︀ ⋀︀
∙ if 𝜆(𝑣)=∧ or 𝜆(𝑣)=∨, then Φ𝑖𝑣 =𝑠𝑣1 [𝑖]𝜆(𝑣)𝑠𝑣2 [𝑖], where 𝑣1 and 𝑣2 are the right/left children of 𝑣;
∙ if 𝜆(𝑣)=𝑋, then Φ𝑖𝑣 =𝑠𝑣 ′ [𝑖 + 1] ∧ ¬𝑙[𝑖], where 𝑣 ′ is the child of 𝑣 and 𝑠𝑣[𝑚] is the constant false;
∙ if 𝜆(𝑣)=𝑌 , then Φ𝑖𝑣 =𝑠𝑣 ′ [𝑖 − 1], where 𝑣 ′ is the child of 𝑣 and 𝑠𝑣[−1] is the constant false;
∙ if 𝜆(𝑣)=𝑃 , then Φ𝑖𝑣 =𝑠𝑣 ′ [𝑖] ∨ 𝑠𝑣[𝑖 − 1], where 𝑣 ′ is the child of 𝑣 and 𝑠𝑣[−1] is the constant false;
∙ if 𝜆(𝑣)=𝐻, then Φ𝑖𝑣 =𝑠𝑣 ′ [𝑖] ∧ 𝑠𝑣[𝑖 − 1], where 𝑣 ′ is the child of 𝑣 and 𝑠𝑣[−1] is the constant true;
∙ if 𝜆(𝑣)=𝑆, then Φ𝑖𝑣 =(𝑠𝑣2 [𝑖] ∧ 𝑠𝑣1 [𝑖]) ∨ (𝑠𝑣1 [𝑖] ∧ 𝑠𝑣[𝑖 − 1]), where 𝑣1 and 𝑣2 are the left and right
children of 𝑣 and 𝑠𝑣[−1] is the constant false.
We note, for the sake of completeness, that Φ𝜙,𝑚 is rewritten (in polynomial time) in conjunctive normal
form, before being passed to the solver. Moreover, by construction, it is possible to establish that Φ𝜙,𝑚 is
satisfiable if, and only if, 𝜙 can be satisfied by a model 𝜋 with 𝑙𝑒𝑛(𝜋) ≤ 𝑚. When SCRea finds a model
𝜎 for a SAT formula Φ𝜙,𝑚 , the decoder module is responsible for the building of the trace 𝜋 that satisfies
the smart contract 𝜙. In particular, starting from 𝜎 it is possible to construct the trace 𝜋 satisfying 𝜙 by
implementing the following steps: (i) If 𝑙[𝑖] ∈ 𝜎 and there is no 𝑙[𝑗] ∈ 𝜎 with 𝑗 < 𝑖 then the decoder
constructs a trace 𝜋 with 𝑖 states; (ii) For every 𝑣 such that 𝜆(𝑣) = 𝑥 and every 𝑖 such that 𝑠𝑣[𝑖] ∈ 𝜎
then the decoder adds 𝑥 to 𝜋[𝑖].
5.2. SCRea at runtime
In this section we will discuss how the reasoner can be applied to solve reasoning problems at runtime.
To work at runtime it is necessary to slightly modify the architecture of SCRea. In particular, the
Encoder module must also receive in input the partial trace 𝜋𝑝 which contains the events recorded on
the blockchain up to the current time instant. In this case, the parameter 𝑚 concerns the additional
number of states (i.e., sets of events) that can happen after those already present in 𝜋𝑝 . Moreover, if
SCRea is meant to work on a set of smart contracts 𝜋𝑝 must be preprocessed to add indicator variables.
�6. Concluding remarks
In this paper we proposed a framework, based on the encoding of smart contracts in Linear Temporal
Logic on finite traces, that enables various reasoning tasks on a single and on a set of smart contracts
running on the same blockchain. The proposed framework, called SCRea, is the first tool developed with
the aim of checking the consistency of a set of smart contracts that are supposed to cooperate in same
blockchain infrastructure and it is able to work at runtime on a running blockchain system. As a first line
for future research, we are planning to implement our framework on an existing blockchain infrastructure
to test its effectiveness on a real system. As a limitation of the proposed framework we want to point out
that LTL is based on a propositional logic and, thus, has some limitations in expressiveness. Therefor, a
second line for future research regards the extension of the proposed framework with a more powerful
logic such as first-order temporal logic that will increase SCRea’s expressive power.
References
[1] Douglis, F., Stavrou, A. (2020). Distributed Ledger Technologies. IEEE Internet Comput., 24(3).
[2] Idelberger, F., Governatori, G., Riveret, R., Sartor, G. (2016). Evaluation of Logic-Based Smart Contracts
for Blockchain Systems. In Proc. of RuleML, pp. 167–183.
[3] Hu, J., Zhong, Y. (2018). A Method of Logic-Based Smart Contracts for Blockchain System. In Proc.
of ICDPA, pp. 58–61.
[4] Stancu, A., Dragan, M. (2020). Logic-Based Smart Contracts. In Proc. of WorldCIST, pp. 387–394.
[5] Nakamoto, S. (2008). Bitcoin: A peer-to-peer electronic cash system.
[6] Wood, G. (2014). Ethereum: A secure decentralised generalised transaction ledger. Ethereum project
yellow paper, 151(2014), 1-32.
[7] Szabo, N. (1997). The idea of smart contracts. Nick Szabo’s Papers and Concise Tutorials, 6.
[8] Dannen, C. (2017). Introducing Ethereum and Solidity (p. 185). Berkeley: Apress.
[9] Pnueli, A. (1977). The Temporal Logic of Programs. In Proc. of FOCS, pp. 46–57.
[10] Pnueli, A. (1981). The Temporal Semantics of Concurrent Programs. Theoretical Computer Science,
13, 45–60.
[11] Calvanese, D., De Giacomo, G., Vardi, M. Y. (2002). Reasoning about actions and planning in ltl
action theories. In Proc. of KR, pp. 593–602.
[12] Ding, X., Smith, S., Belta, C., Rus, D. (2014). Optimal Control of Markov Decision Processes With
Linear Temporal Logic Constraints. IEEE Transactions on Automatic Control, 59(5), 1244–1257.
[13] Fionda, V., Guzzo, A. (2020). Control-Flow Modeling with Declare: Behavioral Properties, Computa-
tional Complexity, and Tools. IEEE Trans. Knowl. Data Eng., 32(5), pp. 898–911.
[14] Chekol, M.W., Fionda, V., Pirrò, G. (2017). Time Travel Queries in RDF Archives. In Proc. of MEPDaW,
pp. 28–42.
[15] Fionda, V., Greco, G. (2018). LTL on Finite and Process Traces: Complexity Results and a Practical
Reasoner. J. Artif. Intell. Res., 63, pp. 557–623.
[16] Pesic, M., Bosnacki, D., Van der Aalst, W. (2010). Enacting Declarative Languages Using LTL:
Avoiding Errors and Improving Performance. In Proc. of SPIN, pp. 146–161.
[17] De Giacomo, G., Vardi, M. Y. (2013). Linear Temporal Logic and Linear Dynamic Logic on Finite
Traces. In Proc. of IJCAI, pp. 854–860.
[18] Li, J., Zhang, L., Pu, G., Vardi, M. Y., He, J. (2014). LTLf satisfiability checking. In Proc. of ECAI, pp.
513–518.
[19] Biere, A., Heljanko, K., Junttila, T., Latvala, T., and Schuppan, V. (2006). Linear Encodings of Bounded
LTL Model Checking. Logical Methods in Computer Science, 2(5), 1–64.
[20] Audemard, G., and Simon, L. (2009). Predicting Learnt Clauses Quality in Modern SAT Solvers. In
Proc. of IJCAI, pp. 399–404.
�