Tiziana Cimoli

In her phd thesis, she proposed a new model for events, in the form of a conservative extension of Winskel’s event structures. Event structures (ES) are one of the classical models of concurrent systems. In classical ES, an enabling X |- e represents the fact that the events e can only occur after all the events in the set X have already occurred. In the new model however, the new kind of causality allows enabled events to happen in any order; and this allows to represent circular dependencies .

Using this new kind of causality, a new theory of contracts has been presented. Contracts represent interacting processes with an explicit notion of obligations and objectives. Processes and their obligations are modeled as event structures, by interpreting events as actions promised by some participants. The states of a contract are sequences of events; a participant has a contractual obligation (in a given state) whenever some of its events is enabled in such a state. Contracts are interpreted as multi-player concurrent games: participants take turns to play by firing events to reach their goals, and they eventually win, lose or tie. The notions of agreement and protection are thus formalized using concepts of strategies and violations: a participant agrees on a contract if she has a strategy to reach her objectives (or make another participant chargeable for a violation), whatever the moves of her adversaries; a participant is protected by a contract when she has a strategy to defend herself in all possible contexts, even in those where she has not reached an agreement.

It has been shown that, using classical event structures as a model, agreements and protection mutually exclude each other. However, using the new model with the circular causality, it is possible to write a contract which both assures protection to her owner and results into an agreement with another participant.

Tiziana also studied the relations between this new kind of event structures and a logic called Propositional Contract Logic. PCL is an extension of intuitionistic propositional logic, featuring a new binary connective, called contractual implication. The main result is that provable atoms in the logic correspond to reachable events in the event structures; and also, there is a correspondence between the configurations of this new kind of event structures and the proofs in a fragment of PCL.

The new model for ES has also been compared with a new kind of Petri Nets called Lending Petri Nets. Lending Petri nets are an extension of Petri nets where places may carry a negative number of tokens. This allows for modeling contracts where a participant may promise to give some of her resources under the guarantee that some other resources will eventually be obtained in exchange. LPNs can model contracts which, at the same time, admit an agreement and protect their participants.

Then Tiziana's studies have broadened to another model for contracts, namely binary session types, to establish a relation between the notion of agreement in contracts with that of compliance in session types. It has been shown that compliance in session types corresponds to the existence of an eager winning strategy in game-based contracts.

Although largely used to model contracts, session types cannot faithfully capture a natural and relevant aspect of interaction protocols, i.e., the timing constraints among the communication actions. Hence, she focused extending synchronous binary session types with time constraints. From a theoretical point of view, the objective was to lift to the timed case some decidability results, like those of compliance and subtyping. Some intriguing problems arose: unlike in the untimed case, a timed session type not always admits a compliant; hence, besides deciding if two session types are compliant, it becomes a relevant problem whether a session type has a compliant one. From a more practical perspective, decision procedures for timed session types, like those for compliance and for dynamic verification, enable the implementation of programming tools and infrastructures for the development of safe communication-oriented distributed applications.

Hence, a decidable compliance relation was introduced , which generalises to the timed setting the usual progress-based notion of compliance between untimed session types. A sound and complete technique was given to decide when a timed session type admits a compliant one, and if so, to construct the least session type compliant with a given one, according to the subtyping preorder induced by compliance. Decidability of subtyping follows from these results. Finally, exploiting this theory, a message-oriented middleware was designed and implemented, where distributed modules with compliant protocols can be dynamically composed, and their communications monitored, so to guarantee safe interactions. The middleware allows to reduce the complexity of developing distributed applications, by relieving programmers from the need to explicitly deal with the misbehaviour of external services.

Recently, Tiziana Cimoli has focused on Smart Contracts, and she has began to investigate the two main platforms for decentralized applications: Bitcoin and Ethereum.

As future work, she aims at studying semantics and properties of Smart Contracts, in relation with the other classical models.

Publications