Introduction

Distributed ledger technologies (for example, blockchains) provide the foundation and core infrastructure for decentralised finance (DeFi), a type of finance that does not rely on intermediaries like exchanges, banks or brokers [1]. DeFi applications are built by utilising smart contracts, which are executable code that facilitates the process of executing and enforcing the terms of an agreement between (untrusted) parties [2].

While agreements naturally follow a human-readable format (e.g., see Example 1.1), today's usual way of writing such smart contracts is by encoding rules in an objectoriented programming language such as Solidity for the Ethereum platform. The procedural style of these languages requires to define what and how certain conditions should be handled, which is an error-prone and cumbersome process and hard to verify by non-experts whether the intention is reflected in code.

Example 1.1. I lend you ten Bitcoins with an interest rate of 3% per year for three years. The interest payment is monthly.

In an attempt to tackle this issue, researchers suggest the use of logic-based smart contract languages, which allow to better represent and reason upon the conditions of a smart contract [2,3]. Different suggested solutions include the use of Prolog [4,5], domainspecific languages [6], finite state machines [7], Active-U-Datalog [8], or formal contract logic [3].

Let us consider Example 1.1 again. By carefully studying this example, one notices that it contains multiple temporal specifications (e.g., per month, per three years, or per year). While temporal reasoning has been used for the verification of smart contracts [9], current solutions for logic-based smart contracts, to the best of our knowledge, do not consider temporal properties at all or in a sub-optimal way, e.g., by arithmetic or by the introduction of predicates with a special temporal meaning. This is an enormous drawback, as many DeFi applications require some sort of temporal processing 1 .

Requirements. In the following, we suggest what we think are the most essential temporal requirements a logic-based smart contract language has to support to provide a minimum amount of useful reasoning capabilities for DeFi applications.

1. Validity Interval. It is necessary to represent intervals, i.e., when a specific kind of operation is valid, not only punctual points. This is necessary for example in voting contracts, where votes are exactly allowed between the start and the end of an interval. 2. Periodicity. It is necessary to specify periodic patterns that encode repeating agreements. This is necessary for example to encode that the salary is paid per month. 3. One Time Event/Delay. It is necessary to encode single future events. This is necessary for example for shopping contracts, where a payment reminder has to be sent in case the money has not been paid. 4. Negation. While only indirectly related to the temporal domain, it is necessary to support negation. This is necessary to encode that something has not happened in a specific interval as the previous example highlights. 5. Verification. It is necessary to verify whether a given model is satisfied for a given set of rules. This helps for the verification of certain proper-ties and is in line with the work of using temporal logic for verification of smart contracts.

DatalogMTL.

A typical language that supports all of these requirements is DatalogMTL. Organization. The remainder of this paper is organized as follows: In Section 2 we introduce DatalogMTL and provide a brief overview on Smart Contracts. In Section 3 we discuss related work in the area of logic-based smart contracts. We discuss the usage of DatalogMTL as a modelling language for Smart Contracts in Section 5 and conclude the work in Section 6.

Preliminaries

In this section, we briefly introduce smart contracts and present the syntax and semantic of DatalogMTL with stratified negation over the integer timeline.

Distributed Ledgers and Smart Contracts

A distributed ledger technology (DLT) is a decentralized, immutable, and append-only database across different nodes that is managed by multiple participants. At the core of the DLT is a consensus mechanism which contains procedures and rules on how transactions are validated by the nodes [11].

A blockchain is a form of DLT, where transactions are recorded and grouped into blocks, where each block includes a hash of the previous block. Other forms of DLTs are Tangle [12], built on top of a directed acyclic graph, or Corda [13], a leading DLT for regulated industries where the ledger stores per node only the facts the node is aware of.

Smart Contracts are programs stored on the distributed ledger technology that run when certain conditions are satisfied. Usually, smart contracts manage an agreement (i.e., rules) between multiple parties per code without requiring a third party. They reduce risk due to the tamperproof property of DLTs and provide transparency to the process. Typical smart contract applications include voting, supply chains, mortgage, copyright protection, or employment arrangements [14].

DatalogMTL

DatalogMTL extends Datalog with metric temporal logic. In this section, we briefly recap the syntax and semantic of DatalogMTL over the integer timeline [15] with stratified negation [16].

Intervals. An interval is of the form ⟨𝑡1, 𝑡2⟩, where the left (right) bracket is either ( or [ () or ]) and 𝑡1, 𝑡2 ∈ Z ∪ {−∞, ∞}, such that 𝑡1 ≤ 𝑡2. An interval is positive if 𝑡1 > 0 and punctual if 𝑡1 = 𝑡2, which we write as 𝑡 instead of [𝑡, 𝑡]. Syntax. We assume a disjoint set of variables and constants. An atom is an expression of the form 𝑃 (𝜏 ), where 𝑃 is a predicate of arity 𝑛 and 𝜏 is a tuple of constants and variables matching the arity. A literal 𝑀 is an expression given by the following grammar:

𝑀 ::= ⊤ | ⊥ | 𝑃 (𝜏 ) | ⊟𝜚𝑀 | ⊞𝜚𝑀 | 𝜚 𝑀 | 𝜚 𝑀 | 𝑀 𝒮𝜚 𝑀 | 𝑀 𝒰𝜚 𝑀

where 𝑃 (𝜏 ) is an atom and 𝜚 is a positive interval. A rule is an expression of the form

𝑀1 ∧ • • • ∧ 𝑀𝑘 ∧ not 𝑀𝑘+1 ∧ • • • ∧ not 𝑀𝑘+𝑚 → 𝑀 ′

for 𝑘, 𝑚 ≥ 0 and where each 𝑀𝑖 is a literal and 𝑀 ′ is a literal restricted to the following grammar:

𝑀 ′ ::= ⊥ | 𝑃 (𝜏 ) | ⊟𝜚𝑀 ′ | ⊞𝜚𝑀 ′

The conjunction of 𝑀𝑖 is the body and 𝑀 ′ is the head of the rule. The literals 𝑀1, . . . , 𝑀 𝑘 are positive body literals of the rule, and 𝑀 𝑘+1 , . . . , 𝑀 𝑘+𝑚 are the negated ones. A rule is safe, if all variables occur in positive body literals of the rule, and positive if it contains no negative body literal. A DatalogMTL program is a finite set of safe rules. A program Π is stratifiable if there exists a stratification of a program Π. A stratification of Π is given as a function 𝜎 that maps each predicate in Π to positive integers such that for each rule it holds that 𝜎(𝑃 + ) ≤ 𝜎(𝑃 ) and 𝜎(𝑃 − ) < 𝜎(𝑃 ) for 𝑃 + a positive body literal, 𝑃 − a negated body literal and 𝑃 the head of the rule. We say that an expression is ground if it contains no variables. A fact is an expression of the form 𝑃 (𝜏 )@𝜚, where 𝑃 (𝜏 ) is ground and 𝜚 a non-empty interval. A dataset is a finite set of facts.

Semantics. An interpretation M specifies for each time point 𝑡 ∈ Z and for each ground atom 𝑃 (𝑎) whether 𝑃 (𝑎) is satisfied at 𝑡, in which case we write M, 𝑡 |= 𝑃 (𝑎). This notion extends to ground literals as follows:

M, 𝑡 |= ⊤ for each 𝑡 ∈ Z M, 𝑡 |= ⊥ for no 𝑡 ∈ Z M, 𝑡 |= ⊟𝜚𝐴 iff M, 𝑠 |= 𝐴 for all 𝑠 with 𝑡 − 𝑠 ∈ 𝜚 M, 𝑡 |= ⊞𝜚𝐴 iff M, 𝑠 |= 𝐴 for all 𝑠 with 𝑠 − 𝑡 ∈ 𝜚 M, 𝑡 |= 𝐴 𝒮𝜚 𝐴 ′ iff M, 𝑠 |= 𝐴 ′ for some 𝑠 with 𝑡 − 𝑠 ∈ 𝜚 ∧ M, 𝑟 |= 𝐴 for all 𝑟 ∈ (𝑠, 𝑡) M, 𝑡 |= 𝐴 𝒰𝜚 𝐴 ′ iff M, 𝑠 |= 𝐴 ′ for some 𝑠 with 𝑠 − 𝑡 ∈ 𝜚 ∧ M, 𝑟 |= 𝐴 for all 𝑟 ∈ (𝑡, 𝑠) M, 𝑡 |= 𝜚 𝐴 iff M, 𝑠 |= 𝐴 for some 𝑠 with 𝑡 − 𝑠 ∈ 𝜚 M, 𝑡 |= 𝜚 𝐴 iff M,

Related Work

Idelberger et al. [3] suggest the formulation via formal contract logic, a (deontic) defeasible logic. They suggest specifying a default state and use superiority relations to overwrite the state in case a specific event is triggered. This logic always only derives a single state based on current triggers that are valid at the current time. They have not discussed temporal properties at all. Similarly, Frantz and Nowostawski [6] decompose institutions into rule-based statements, which are constructed from 5 different components (attributes (A), deontic (D), aim (I), conditions (C), or else (O)). An example is "people (A) must (D) vote (I) every four years (C), or else they face a fine (O)" and suggest a mapping of the components to Solidity smart contracts using a domainspecific language which creates a template that has to be completed manually.

Stancu and Dragan [5] suggested a Python-to-Prolog interface on top of BigchainDB and Tendermint to forward Prolog clauses to a Prolog process to verify the contract.

Suvorov and Ulyantsev [7] suggest to use a LTL specification and test scenario to create a finite state machine, which is combined with state and action definitions to generate a Solidity smart contract. They use LTL to express possible state transitions in a finite state machine, but again no temporal properties are explored such as a duration of a voting period.

Hu and Zhang [8] propose Logic-SC, a smart contract model based on Active-U-Datalog with temporal extensions. Active-U-Datalog extends Datalog rules with update atoms, which can add or remove relations from the dataset. The temporal extension is provided by a pair ⟨[𝑏𝑒𝑔𝑖𝑛, 𝑒𝑛𝑑], 𝑃 ⟩, where 𝑃 is a periodic expression and [𝑏𝑒𝑔𝑖𝑛, 𝑒𝑛𝑑] denotes the lower and upper bounds for the intervals in 𝑃 . An example of a periodic expression is all .Years + {3, 7}.Months ◁ 2.Months, representing intervals starting as third and seven month of every year and having a duration of 2 months. A rule for counting the total working hours is given as follows totalhours(𝑡1), 𝑡2 = 𝑡1 + 1, +Hour (𝑡), 𝑡 ∈ workingTime → −totalhours(𝑡1), +totalhours(𝑡2), where workingTime is a periodic expression. Critically, this approach deletes elements which are not valid at the current time point and adds new elements, and hence simulates the behaviour of procedural implementations which also add or remove elements. In comparison, our approach works per time point and assumes a single action per time point. Hence, we explore the concept of append-only data structures and create a new status for each new time point.

Ciatto et al. [4] suggest a new language called Tenderfone, that is based on Prolog. It offers several entry points and built-in functions which manage the interaction with smart contracts. These functions include init(args), which gets executed once when the smart contract is deployed, receive(Msg, Sender) to invoke the smart contract and send (Msg, Recipient) to call some other contract. In addition, they offer several temporal predicates. This includes now (T) to get the current timestamp, when(T, Msg) to trigger a receive of the smart contract at time 𝑇 , delay(DT, Msg) which is equal to when(T + DT, Msg), now (T) and the fact that periodically(P, Msg), which triggers receive every 𝑃 time units. This suggestion is close to our solution, as it is the only solution that considers temporal properties. However, they only consider single time units and do not cover intervals.

To summarize, related work focused on the formulation of logic-based smart contracts as well as on the generation of efficient code. This paper will focus only on the formulation aspect and keeps the generation open for future work. The solution of Hu and Zhang provide through the flexibility of Datalog, the possibility to model certain temporal properties, and the solution of Ciatto et al. is the only work that actively considers temporal properties in their proposal. To the best of our knowledge, intervals have not been considered so far in the study of logic-based smart contract languages.

DatalogMTL Smart Contracts

In this section, we formally specify smart contracts with DatalogMTL. While the introduced program would allow one to specify the rules of the contract, possible interaction points with different parties and smart contracts as well as an initial state have to be specified.

Definition 4.1.

A smart contract is a quadruple (𝑁, Π, 𝐷, 𝐴) where:

• 𝑁 is a unique name of the contract and can be seen as a namespace for the contract. • Π is the DatalogMTL program encoding the rules of the smart contract • 𝐷 is the initial dataset encoding the initial state of the smart contract.

• 𝐴 is the set of activators. This set contains atoms that expect input from others and act as interaction points, which other smart contracts or parties may invoke. Per time point, it is only allowed to fire one activator.

While Π and 𝐷 map directly to the definition of Dat-alogMTL, 𝑁 and 𝐴 are in addition required for smart contracts. The namespace provides the possibility to call other smart contracts by generating an atom, which is prefixed with a namespace, or accessing data from other smart contracts. For example, consider a will that manages the transfer of money in case of death, then one can write a rule of the form PersonDied(𝑌 ), Token.balance(𝑌, 𝑋), Heritage(𝑌, 𝑍)

→ Token.transfer (𝑌, 𝑍, 𝑋)

to specify that the whole balance of 𝑌 (accessed from the token) is transferred (by calling the token) to 𝑌 's heir 𝑍, in case 𝑌 died. The activators 𝐴 provide input interfaces to the smart contract. The set contains all atoms in the rules, which can only be provided by external parties. Only one such activator is allowed to be fired per time point to ensure consistency with the rule (i.e., one time point exactly matches to one state of the contract). This is without loss of generality, as in case multiple activators are required, they can be combined by introducing an additional activator and creating auxiliary atoms for internal use. Note, in the following examples we use directly the activators in rule heads for readability, instead of instantiating some additional atom, i.e., we write rules of the form 𝑃 → 𝑄, where 𝑄 is an activator, instead of introducing an auxiliary atom 𝑅 and map the activator to the auxiliary atom 𝑄 → 𝑅 which is used in the rules as head 𝑃 → 𝑅. We still ensure that only one external activator is used per state transition.

Example 4.1.

A smart contract in DatalogMTL with the rule given in Example 1.1 is given as a quadruple (𝑁, Π, 𝐷, 𝐴), where 𝑁 is some unique identifier such as BitcoinLending, the dataset 𝐷 contains the information regarding the monthly interest payment 𝐼𝑛𝑡𝑒𝑟𝑒𝑠𝑡(0.0025)@[0, ∞), the activator 𝐴 is the atom Borrow which is called when the lending starts and fixes the start time point, and the program Π is given as follows:

Borrow (𝐴, 𝐵) → ⊞[0,3𝑦]BorrowDur (𝐴, 𝐵) (1) Borrow (𝐴, 𝐵) → ⊞[1𝑚,1𝑚]PayTime(𝐴, 𝐵) (2) PayTime(𝐴, 𝐵) → ⊞[1𝑚,1𝑚]PayTime(𝐴, 𝐵) (3) Interest(𝑋),

PayTime(𝐴, 𝐵), BorrowDur (𝐴, 𝐵) → Token.transfer (𝐴, 𝐵, 𝑋) (4) where Borrow (𝐴, 𝐵) specifies that 𝐴 borrows the money from 𝐵, BorrowDur (𝐴, 𝐵) defines the duration of the borrow contract between 𝐴 and 𝐵, PayTime(𝐴, 𝐵) specifies the time points when 𝐴 has to pay interest to 𝐵, Interest(𝑋) specifies the interest amount which has to be paid and Token.transfer is a call to an external smart contract, for example a smart contract such as given in Section 5.2, where 𝐴 pays 𝐵 the amount 𝑋.

In detail, Rule (1) specifies the duration of the agreement with three years beginning at the time point where Borrow gets called. Rules ( 2) and ( 3) define the payment time points. In detail, Rule (2) specifies the first interest payment as the first month after the time point where Borrow (𝐴, 𝐵) was activated by some party or smart contract, and Rule (3) extends this to follow-up payments recursively. Rule (4) executes the token transfer of the interest amount in case it is payment time and it is valid (i.e., during the BorrowDur ) by executing the activator of a different smart contract.

We visualized in Figure 1 the use of activators and namespaces to access the data of another smart contract of Example 4.1, where we assume that 𝐴 is Alice, 𝐵 is Bob and there is some additional rule that requires access to the balance of 𝐴 (for example, to check whether 𝐴 is creditworthy or not) to visualize the read direction and a third party, which could either be Alice, Bob or some smart contract that start the borrowing transaction at some time point which gets added as fact to the contract (marked as blue) and derives all other facts given in the box according to the rules of the program.

Case Study

In the previous section, we introduced DatalogMTL smart contracts with a simple example. In this section, we study the use of DatalogMTL together with two real-world examples. We first consider a widely discussed example in the area of logic-based smart contracts, and then we discuss on how to utilize DatalogMTL for writing a smart contract for a crypto token.

License Agreement

In this case study, we focus on the specification of a license agreement [7,3,8]. In this section, we want to explore how such a contract can be written in DatalogMTL.

Example 5.1. Let us consider the following clauses for the right to evaluate and publish the evaluation results of a product [3]:

1. The Licensor grants the Licensee a license to evaluate the Product. 2. The Licensee must not publish the results of the evaluation of the Product without the approval of the Licensor; the approval must be obtained before the publication. If the Licensee publishes results of the evaluation of the Product without approval from the Licensor, the Licensee has 24h to remove the material. 3. The Licensee must not publish comments on the evaluation of the Product, unless the Licensee is permitted to publish the results of the evaluation. 4. If the Licensee is commissioned to perform an independent evaluation of the Product, then the Licensee has the obligation to publish the evaluation results. 5. This license will terminate automatically if the Licensee breaches this agreement.

Apart from the fact that contracts are of natural interest to the economic sector, changing the stakeholders and adapting a few sentences directly leads to an economic example, namely, the golden power check for company takeovers [17]. In this case, the licensor is the government (which has veto/approval power for acquisitions), the licensee is the "acquiring" company, and the product is the target company.

We use the atom GrantX (𝐴, 𝐵, 𝑃 ) to specify that Licensor 𝐴 has granted Licensee 𝐵 the right to do 𝑋 for product 𝑃 , where 𝑋 is either Use to grant the right to evaluate, Commission to grant the right to publish results without approval, Appr to grant the right to publish the results. We further use Publish(𝐵, 𝑃 ) to specify that 𝐵 has published the results of product 𝑃 and Comment(𝐵, 𝑃 ) to specify that 𝐵 has made a comment on the evaluation of product 𝑃 , Remove(𝐵, 𝑃 ) to specify that 𝐵 has removed the content and Violation(𝐵, 𝑃 ) to specify that 𝐵 has violated the license for product 𝑃 and OblRemove(𝐵, 𝑃 ) to specify that 𝐵 is obliged to remove the license. The smart contract is then defined as a quadruple (𝑁, Π, 𝐷, 𝐴), where 𝑁 is some unique identifier such as LicenseAgreement, the dataset 𝐷 is empty, the activators are given by the set of atoms {Publish, Comment, GrantAppr , GrantCommission, GrantUse, Remove} and the program Π is given by the following rules, where we omit the terms in the rules for readability:

GrantAppr → ⊞[0,∞)GrantAppr (1)

Publish, ¬GrantAppr → OblRemove GrantUse, ¬Violation → ⊞[1,1]GrantUse (7) Rule (1) specifies that an approval holds forever. Rules 2-4 match clause (2). Rule 2 states that if the results are published, but they are not approved, then the licensee is obliged to remove the results. Rule (3) specifies the duration of the obligation, which is bounded to 24 hours and extended to the next time point in case no removal has happened. Note that this rule uses an extended form of stratified negation, namely, temporal stratified negation. In this form, the negated facts in recursion only propagate information from the past to the future. Rule (4) then triggers a violation in case the maximum time of 24 hours has been reached. For comments, there is no exception and hence any comment without approval is marked as a violation by Rule (5) which matches clause (3) of the agreement. Rule (6) handles independent evaluations. In case this right is given, then it is also approved. Rule (7) manages the extension of the license, in case no violation occurred. Discussion. From the example, we can see that Dat-alogMTL allows to express complex contracts without the need of formulating rules with any form of explicit time-handling by only using temporal operators. By comparing the example with the established requirements from Section 1, this example gives evidence for requirement (1) by rule (1) or (4), requirement (3) by rule (4), requirement (4) by rules (2), (3), ( 5) and (7). We do not cover requirement (2) here, but (2) has been covered in Section 4. Requirement (5) is usually not part of the contract itself but used to verify that a contract does not reach a certain state. For example, it can be used to state that only one activator is fired at most once per time point or to state that it is not possible to publish a result without having the license to use the program, as the program cannot be evaluated. The latter case can be formulated by a rule of the following form:

Publish, ¬ [0,∞) GrantUse → ⊥

ERC20 Token

In this case study, we analyse how an Ethereum ERC20 token contract [18] can be formalized in DatalogMTL. The standard provides some read-only functions, such as what is the current balance of a user, which we do not consider in the example, as just the atoms of the program have to be accessed. In the following, we focus on the functions, which change the state of the contract. The goal of these functions is to specify when a transfer of tokens between two parties is allowed and how a transfer affects the balance of the parties. The smart contract is then defined as a quadruple (𝑁, Π, 𝐷, 𝐴), where the namespace 𝑁 is some unique identifier such as Token, the dataset 𝐷 contains the initial balance, which is assigned to one or more people, in this case 2000 tokens are assigned to Alice, Bal (𝐴𝑙𝑖𝑐𝑒, 2000), the activators are given by the set of atoms {Tran, App, TranF } and the program Π is given by the following rules Rule (1) verifies whether the balance of party 𝐴 is enough for the transfer. Rules (2) and (3) apply a verified transfer by reducing and increasing the balance of the participating parties. Rule (4) applies the third-party transfer by checking whether the party is allowed to transfer the amount from party 𝐴. In such a case, a usual transfer is emitted, which is handled by rules (1) to (3). Rule (5) updates the approval amount in case such a transaction is successful. Rules ( 6)-( 8) are the housekeeping rules, which copy the current balance and the approved value to the next unit, in case nothing changed. Arithmetic Expressions. In this example, we have used arithmetic expressions in the rules, which have not been formally defined in DatalogMTL. We want to point out that the use of arithmetic in recursion without any restrictions yields undecidability in general [19], however in this case the arithmetic expression is bounded by activators. A formal definition of arithmetic in DatalogMTL has not been considered yet and is future work. The arithmetic operations of this example follow the default notion of addition and subtraction.

Conclusion

In this paper, we introduced DatalogMTL as an option to model smart contracts. We first derived the essential requirements for the necessary features in smart contracts, and then introduced DatalogMTL as a basis for a smart contract language. We explored our language by discussing two real-world examples. In the first one, we introduced a widely discussed existing example and highlighted the advantages of using DatalogMTL, while in the second one we discussed how to model tokens with DatalogMTL. Thereby, we identified the need to have a formally proved arithmetic extension of DatalogMTL to support DeFi applications which require arithmetic operations, which we will consider studying in the future. In addition, we want to focus on compiling DatalogMTL smart contracts to existing procedural smart contract languages such as Solidity to support well-established blockchains such as Ethereum.