Literature Review: Smart Contract Semantics <s> Dynamic Logic <s> In this paper we propose a formal language for writing electronic contracts, based on the deontic notions of obligation, permission, and prohibition. We take an ought-to-do approach, where deontic operators are applied to actions instead of state-of-affairs. We propose an extension of the µ-calculus in order to capture the intuitive meaning of the deontic notions and to express concurrent actions. We provide a translation of the contract language into the logic, the semantics of which faithfully captures the meaning of obligation, permission and prohibition. We also show how our language captures most of the intuitive desirable properties of electronic contracts, as well as how it avoids most of the classical paradoxes of deontic logic. We finally show its applicability on a contract example. <s> BIB001 </s> Literature Review: Smart Contract Semantics <s> Dynamic Logic <s> Many software applications are based on collaborating, yet competing, agents or virtual organisations exchanging services. Contracts, expressing obligations, permissions and prohibitions of the different actors, can be used to protect the interests of the organisations engaged in such service exchange. However, the potentially dynamic composition of services with different contracts, and the combination of service contracts with local contracts can give rise to unexpected conflicts, exposing the need for automatic techniques for contract analysis. In this paper we look at automatic analysis techniques for contracts written in the contract language $\mathcal{CL}$. We present a trace semantics of $\mathcal{CL}$ suitable for conflict analysis, and a decision procedure for detecting conflicts (together with its proof of soundness, completeness and termination). We also discuss its implementation and look into the applications of the contract analysis approach we present. These techniques are applied to a small case study of an airline check-in desk. <s> BIB002
Prisacariu and Schneider BIB001 propose a contract language CL. CL is made up of elements of deontic, dynamic and temporal logics. An extension to CL was proposed by Fenech et al. BIB002 Wtih this extension, they are able to specify obligations, permissions and prohibitions with state based constraints, and relative temporal constraints. The system also has support for reparations.