Timed Automata Semantics for Visual e-Contracts

TL;DR

This paper introduces a formal semantics for C-O Diagrams, a visual language for electronic contracts, using extended timed automata to accurately model obligations, permissions, prohibitions, penalties, and timing constraints.

Contribution

It provides a novel formal semantics for C-O Diagrams by extending timed automata with state and edge orderings to capture deontic modalities.

Findings

Formal semantics enables precise analysis of electronic contracts.

Timed automata extension captures complex timing and deontic constraints.

Supports automated verification of contract compliance.

Abstract

C-O Diagrams have been introduced as a means to have a more visual representation of electronic contracts, where it is possible to represent the obligations, permissions and prohibitions of the different signatories, as well as what are the penalties in case of not fulfillment of their obligations and prohibitions. In such diagrams we are also able to represent absolute and relative timing constraints. In this paper we present a formal semantics for C-O Diagrams based on timed automata extended with an ordering of states and edges in order to represent different deontic modalities.