Smart contracts have been proposed as executable implementations enforcing real-life contracts. Unfortunately, the semantic gap between these allows for the smart contract to diverge from its intended deontic behaviour. In this paper we show how a deontic contract can be used for real-time monitoring of smart contracts specifically and request-based interactive systems in general, allowing for the identification of any violations. The deontic logic of actions we present takes into account the possibility of action failure (which we can observe in smart contracts), allowing us to consider novel monitorable semantics for deontic norms. For example, taking a rights-based view of permissions allows us to detect the violation of a permission when a permitted action is not allowed to succeed. A case study is presented showing this approach in action for Ethereum smart contracts.

This article describes several performance improvements that allowed FormaLex, a tool developed to model check legal documents to find coherence problems, to process a real case study of the Argentinian Customer Protection Act. The described truth-preserving techniques reduce the model checking state space by improving the representation of actions and filtering language constructs that are used to encode the law.

Defining and characterising conditional permissions has never been easy. Part of the problem, we believe, comes from the fact that there is not one but a whole family of possible deontic operators, all of them distinct and reasonable, that can be labelled as conditional permissions. In this article, rather than disputing the correct interpretation, we revisit a number of different interpretations the term has received in the literature, and propose appropriate formalisations for these interpretations within the context of contract automata.

Chatbots have been used in different scenarios for getting people interested in CS for decades. However, their potential for teaching basic concepts and their engaging effect has not been measured. In this paper we present a software platform called Chatbot designed to foster engagement while teaching basic CS concepts such as variables, conditionals and finite state automata, among others. We carried out two experiences using Chatbot and the well known platform Alice: 1) an online nation-wide competition, and 2) an in-class 15-lesson pilot course in 2 high schools. Data shows that retention and girl interest are higher with Chatbot than with Alice, indicating student engagement.

Although contract reparations have been extensively studied in the context of deontic logics, there is not much literature using reparations in automata-based deontic approaches. Contract automata is a recent approach to modelling the notion of contract-based interaction between different parties using synchronous composition. However, it lacks the notion of reparations for contract violations. In this article we look into, and contrast different ways reparation can be added to an automaton- and state-based contract approach, extending contract automata with two forms of such clauses: catch-all reparations for violation and reparations for specific violations.

In regulated interactive systems, one party's behaviour may impose restrictions on how others may behave when interacting with it. These restrictions may be seen as implicit contracts which the affected party has to conform to and may thus be considered inappropriate or excessive if they overregulate one of the parties. In this paper we characterise such implicit contracts and present an algorithmic way of synthesising them using a formalism based on contract automata to regulate interactive action-based systems.

We present a formalization of Kanger's types of rights in the context of interacting two-party systems, such as contracts. We show that in this setting basic rights such as claim, freedom, power and immunity can be expressed in terms of (possibly negated) permissions and obligations over presence or absense of actions. Another way of saying this is that, at least in the context of contracts, neither claim, nor power, nor freedom nor immunity are foundational modalities, as they can be defined in terms of others. We also show that the set of atomic type rights is different from Kanger's original proposal.

Despite the fact that contracts are, by definition, an agreement between two or more parties, most formal studies limit themselves to contracts regulating only a single party or the parties independently of each other, without looking into how permissions, obligations or prohibitions of one party affect the other. This article deals with the analysis of what different types of permissions mean in the context of contracts. To give formal semantics we use an automata based formalism allowing to model for one party agreeing, delaying or plain refusing on performing certain actions that the other is attempting. This approach also yields a natural notion of contract strictness analysis for each party.

This article presents the FormaLex toolset, an approach to legislative drafting that, based on the similarities between software specifications and some types of regulations, uses off-the-shelf LTL model checkers to perform automatic analysis on normative systems.

Research in Model-Checking is focused on increasing the size of the problems tools can deal with. The ultimate wave has been the use of Distributed-Computing, where a cluster of computers work together to solve the problem [8, 3, 9].In our work we present a distributed model-checker that evolves from the tool Kronos [5] and can handle backwards computation of TCTL-reachability formulae [1] over timed-automata [2]. Our proposal, including the arguments of its correctness, is based on software architectures, using a notation adapted from [6]. We find such an approach a natural and general way to address the development of complex tools that need to incorporate new features and optimizations as they evolve.We introduce some interesting features such as a priori graph partitioning (using METIS [7], a standard library for graph partitioning), a sophisticated machinery to reach optimum performance (communication piggybacking and delayed messaging) and dead-time utilization, where every processor uses time intervals of inactivity to perform auxiliary, time-consuming tasks that will later speed up the rest of the computation.The correctness proof strategy combines an architecture evolution with the theoretical results about fix point calculation developed by Patrick Cousot in 1978 [4].