lemmaLemma[section] definitionDefinition[section] exampleExample[section]
observationObservation[section] theoremTheorem[section]
propositionProposition[section] corollaryCorrolary[section]

11institutetext: ISP, University of Lübeck, Germany 11email:
<EMAIL_ADDRESS>
22institutetext: University of Gothenburg, Sweden 22email:
<EMAIL_ADDRESS>
# Synchronous Agents, Verification, and Blame — A Deontic View

Karam Kharraz 11 Shaun Azzopardi  22 Gerardo Schneider  22 Martin Leucker  11

###### Abstract

A question we can ask of multi-agent systems is whether the agents’ collective
interaction satisfies particular goals or specifications, which can be either
individual or collective. When a collaborative goal is not reached, or a
specification is violated, a pertinent question is whether any agent is to
blame. This paper considers a two-agent synchronous setting and a formal
language to specify when agents’ collaboration is required. We take a
_deontic_ approach and use _obligations_ , _permissions_ , and _prohibitions_
to capture notions of non-interference between agents. We also handle
_reparations_ , allowing violations to be corrected or compensated. We give
trace semantics to our logic, and use it to define blame assignment for
violations. We give an automaton construction for the logic, which we use as
the base for model checking and blame analysis. We also further provide
quantitative semantics that is able to compare different interactions in terms
of the required reparations.

##  1 Introduction

Interaction between agents can be adversarial, where each agent pursues its
own set of individual goals, or cooperative where the agents collaborate to
achieve a collective goal. Verification techniques can help us detect whether
such goals may be achieved. Agents may also interfere or not cooperate, at
which point the failure to achieve a goal could be attributed to some agent.
In this paper, we develop a _deontic_ logic allowing us to specify the
anticipated interaction of two agents in the presence of such aspects.

A deontic logic [McNamara2006, von1951deontic] includes norms as first-class
concepts, with _obligations_ , _permissions_ , and _prohibitions_ as basic
norms. These concepts are crucial in legal documents and contractual
relationships, where the agents are the parties to a contract.111We use party
and agent interchangeably throughout. Norms are parameterised by
actions/events or propositions and are used to specify what ought to be, or
the parties ought to do.

In this paper, interaction or cooperation of the agents is modelled as the
interplay of the individual actions performed by each agent, leading to the
concept of cooperative actions. Cooperative actions could be synchronous,
i.e., actions at each time point of each agent are meant to describe the
possible cooperation, or asynchronous, meaning that actions for cooperation
may happen a different time points.222Observe similarities with synchronous
and asynchronous communication. We choose synchrony as an abstraction to
simplify the concept of cooperation and non-interference between parties. We
also study only the setting with two rather than many parties. As such, we are
concerned with two-party synchronous systems, leaving extensions as future
work.

We re-purpose and extend the syntax of a deontic language from literature
[DBLP:conf/jurix/AzzopardiGP16, DBLP:conf/jurix/AzzopardiPS18] into a new
deontic logic with denotational semantics appropriate for this two-party
setting. Our semantics depends on two notions of informative satisfaction or
violation, which talk about the exact point in time a contract is satisfied or
violated. Other features of the logic include the ability to make contracts
trigger on matching a regular language, requiring the satisfaction of a
contract while one is still within the prefix language of a regular language,
and a recursion operator to allow the definition of persistent contracts and
repetition.

We extend the semantics with a notion of blame assignment, to identify which
party is responsible for a certain violation. We further use this to define
quantitative semantics that counts the number of violations caused by a
certain party, which can be used to compare different traces or behaviour of a
party.

We give an exponential automata construction for the logic, transforming a
contract specification into an automaton capable of identifying satisfaction,
and violation as specified in our semantics. We also provide a model checking
algorithm, which is quadratic in the size of the contract automaton, hence
exponential in the size of the contract. We re-use this construction for blame
analysis, but leave analysis for the quantitative semantics for future work.

The paper organisation follows. Section 2 lays out preliminaries, Section 3
presents our logic, and Section 4 presents algorithms for model checking and
blame analysis through automata constructions. Related work is considered in
Section 5, and we conclude in Section 6.

##  2 Preliminaries

We write $\mathbb{N}_{\infty}$ for $\mathbb{N}\cup\\{\infty\\}$. Given a
finite alphabet $\Sigma$, we write $\Sigma_{0}$, and $\Sigma_{1}$ for re-
labellings of $\Sigma$ with party identifiers $0$ and $1$, and $\Sigma_{0,1}$
for $\Sigma_{0}\cup\Sigma_{1}$. We use $P[x/y]$ to refer to the syntactic
replacement of $x$ in $P$ with $y$, where $P$ can be an automaton ($x$ and $y$
are states), or a specification ($x$ and $y$ are syntactic objects in the
language). We write $(*,s)$ to refer to all state pairs with $s$ in the second
position, and similarly for $(s,*)$.
Traces For $i\in\mathbb{N}$, $j\in\mathbb{N}_{\infty}$, and an infinite trace
$w$ over sets of actions from a finite alphabet $\Sigma$, we denote the trace
between positions $i$ and $j$ by $w[i..j]$, including the values at both
positions. If $j<i$ then $w[i..j]$ is the empty trace. When $j=\infty$ then
$w[i..j]$ is the suffix of $w$ from $i$. We write $w[i]$ for $w[i...i]$, and
$w\cdot w^{\prime}$ for concatenation of $w$ and $w^{\prime}$, which is only
defined for a finite word $w$.

Given two traces $w,w^{\prime}$ over $2^{\Sigma}$, we define stepwise
intersection: $(w\sqcap
w^{\prime})[i]\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny def}}}{=}}w[i]\cap
w^{\prime}[i]$, union $(w\sqcup
w^{\prime})[i]\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny def}}}{=}}w[i]\cup
w^{\prime}[i]$, and union with party labelling:
$(w\sqcup^{0}_{1}w^{\prime})[i]\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}w[i]\cup^{0}_{1}w^{\prime}[i]$, where
$E\cup^{0}_{1}E^{\prime}\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\\{a_{0}\mid a\in E\\}\cup\\{a_{1}\mid a\in E^{\prime}\\}$, i.e. the
left actions are labeled by $0$ and the right actions by $1$. This gives a
trace in $\Sigma_{0,1}$. For instance, given
$w=\langle\\{a\\},\\{b\\},\\{c,d\\}\rangle$ and
$w^{\prime}=\langle\\{a\\},\\{e\\},\\{d,e\\}\rangle$, we have that $w[2]\cap
w^{\prime}[2]=\\{c,d\\}\cap\\{d,e\\}=\\{d\\}$ and
$w[2]\sqcup^{0}_{1}w^{\prime}[2]=\\{c,d\\}\sqcup^{0}_{1}\\{d,e\\}=\\{c_{0},d_{0},d_{1},e_{1}\\}$.

Given two traces $w_{0}$ and $w_{1}$, over $2^{\Sigma}$, we write
$\vec{w}_{i}^{j}$ for the pair $(w_{0}[i..j],w_{1}[i..j])$. $\vec{w}_{i}^{j}$
is said to be an interaction, and when $j\in\mathbb{N}$ a finite interaction.
Sometimes we abuse notation and treat $\vec{w}_{i}^{j}$ as a trace in
$\Sigma_{0,1}$, since it can be projected into such a trace through
$\sqcup^{0}_{1}$.

Automata A tuple $A=\langle\Sigma,Q,q_{0},\textit{Rej},\rightarrow\rangle$ is
an automaton, where $\Sigma$ is a finite alphabet, $S$ is a finite set of
states, $s_{0}\in S$ is the initial state, $\textit{Rej}\subseteq S$ is a set
of rejecting states, and $\rightarrow\in S\times
2^{\Sigma}\rightarrow(2^{S}\setminus\emptyset)$ is the transition function
($\rightarrow\in S\times 2^{\Sigma}\rightarrow S$ when the automaton is
deterministic). The language $L(A)$ of automaton $A$ is the set of infinite
traces with no prefix reaching a rejecting state. The rejecting language
$RL(A)$ of automaton $A$ is the set of infinite traces with a prefix reaching
a rejecting state. We write $RL_{s}(A)$ for the rejecting language through a
specific rejecting state $s\in\textit{Rej}$.

The synchronous product of automata $A$ and $B$ over the same alphabet
$\Sigma$, denoted by $A\|B$, is the automaton: $(\Sigma,S_{A}\times
S_{B},(s_{0_{A}},s_{0_{B}}),(Rej_{A}\times S_{B})\cup(S_{A}\times
Rej_{B}),\rightarrow)$ where $\rightarrow$ is the minimal relation such that:
for any $E\subseteq\Sigma$, if $s_{1}\xrightarrow{E}_{A}s^{\prime}_{1}$ and
$s_{2}\xrightarrow{E}_{B}s^{\prime}_{2}$ then
$(s_{1},s_{2})\xrightarrow{E}(s^{\prime}_{1},s^{\prime}_{2})$.

The relaxed synchronous product of automata $A$ and $B$ over the same alphabet
$\Sigma$, denoted by $A\|^{r}B$ includes $A\|B$ but allows moving
independently when there is no match: if
$s_{1}\xrightarrow{E}_{A}s^{\prime}_{1}$ and $\nexists s^{\prime}_{2}\cdot
s_{2}\xrightarrow{E}_{B}s^{\prime}_{2}$, then
$(s_{1},s_{2})\xrightarrow{E}(s^{\prime}_{1},s_{2})$; and symmetrically.

Moore Machines A Moore machine is a 5-tuple
$M=(S,s_{0},\Sigma_{I},\Sigma_{O},\delta,\lambda)$ where $S$ is a finite set
of states, $s_{0}\in S$ is the initial state, $\Sigma_{I}$ and $\Sigma_{O}$
are respectively the finite set of input and output actions, $\delta:S\times
2^{\Sigma_{I}}\rightarrow 2^{S}$ is a transition function that maps each state
and inputs to a next state, and $\lambda:S\rightarrow 2^{\Sigma_{O}}$ is an
output function that maps each state to a set of outputs.

The product of a Moore machine $M_{1}$ over input alphabet $\Sigma_{I}$ and
output alphabet $\Sigma_{O}$, and Moore machine $M_{2}$ with flipped input and
output alphabets is the automaton: $M_{1}\otimes
M_{2}\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}(\Sigma_{I}\cup\Sigma_{O},S_{1}\times
S_{2},(s_{0_{1}},s_{0_{2}}),\emptyset,\rightarrow)$ where $\rightarrow$ is the
minimal relation such that: for any states $s_{1}\in S_{1}$ and $s_{2}\in
S_{2}$, where $s_{1}\xrightarrow{\lambda_{2}(s_{2})}s^{\prime}_{1}$ and
$s_{2}\xrightarrow{\lambda_{1}(s_{1})}s^{\prime}_{2}$ then
$(s_{1},s_{2})\xrightarrow{\lambda_{1}(s_{1})\cup\lambda_{2}(s_{2})}(s^{\prime}_{1},s^{\prime}_{2})$.

Regular Expressions We use standard syntax for regular expressions. We treat
as atomic boolean combinations of actions from $\Sigma_{0,1}$. The operators
are standard: choice, $re+re$ (match either); sequence, $re;re$ (match the
first then the second) and the Kleene plus, $re^{+}$ (match a non-zero finite
amount of times in sequence). The language of a regular expression $re$ is a
set of finite traces: $L(re)\subseteq(2^{\Sigma_{0,1}})^{*}$. We abuse
notation and write $\vec{w}_{i}^{j}\in L(re)$ for
$w_{0}[i...j]\sqcup_{1}^{0}w_{1}[i...j]\in L(re)$.

We restrict attention to the tight language of a regular expression,
containing matching finite traces that have no matching strict prefix:
$TL(re)\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\\{\vec{w}_{i}^{j}\in L(re)\mid\nexists
k:k<j\wedge\vec{w}_{i}^{k}\in L(re)\\}$. The prefix closure of the tight
language is the set of finite prefixes of the tight language up to a match:
$cl(re)\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\\{\vec{w}_{i}^{k}\mid\exists j:\vec{w}_{i}^{j}\in TL(re)\wedge
i\leq k<j\\}$. We define the complement of the prefix closure as the set of
finite traces that do not tightly match the regular expression but whose
maximal strict prefix is in the closure of the expression:
$\overline{cl}(re)\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\\{\vec{w}_{i}^{j}\mid(\vec{w}_{i}^{j-1}\in
cl(re)\wedge\vec{w}_{i}^{j}\not\in cl(re)\wedge\vec{w}_{i}^{j}\not\in
TL(re))\\}$.

We denote by $A(re,s_{0},s_{\checkmark},s_{\times})$ the deterministic finite
automaton corresponding to regular expression $re$, with $s_{0}$, and
$s_{\times}$ respectively as the initial and rejecting states and,
$s_{\checkmark}$ as a sink state, s.t. $\forall\vec{w}_{i}^{j}\in
TL(re):s_{0}\xRightarrow{\vec{w}_{i}^{j}}s_{\checkmark}$,
$\forall\vec{w}_{i}^{j}\in{cl}(re):\exists
s:s_{0}\xRightarrow{\vec{w}_{i}^{j}}s\wedge s\neq s_{\checkmark}\wedge s\neq
s_{\times}$, and
$\forall\vec{w}_{i}^{j}\in\overline{cl}(re):s_{0}\xRightarrow{\vec{w}_{i}^{j}}s_{\times}$.

##  3 A Deontic Logic for Collaboration

In this section, we present the syntax and semantics of $c\mathcal{DL}$, a
deontic logic able to express the extent to which parties should cooperate and
non-interfere.

######  Definition 1 ($c\mathcal{DL}$ Syntax).

A $c\mathcal{DL}$ contract $C$ is given by the following grammar, given an
alphabet $\Sigma$, regular expressions $re$, a set of variables $\mathbb{X}$,
and party labels $p$ from $\\{0,1\\}$:

$\displaystyle a\in$ $\displaystyle~{}\Sigma_{0}\cup\Sigma_{1}$ $\displaystyle
N:=\ $ $\displaystyle~{}O_{p}(a)\mid F_{p}(a)\mid P_{p}(a)\mid\top\mid\perp$
$\displaystyle C:=\ $ $\displaystyle~{}N\mid C\wedge C\mid C;C\mid
C\blacktriangleright C\mid$ $\displaystyle~{}\langle re\rangle C\mid
re\rotatebox[origin={c}]{-90.0}{$\bumpeq$}C\mid\mathbb{X}\mid recX.C$

Our setting is that of two-party systems, with one party indexed with $0$ and
the other with $1$. As the basic atoms of the language, we have _norms_. These
norms are labeled by the party that is the main subject of the norm, and the
action that is normed: $O_{p}(a)$ denotes an obligation for party $p$ to
achieve $a$; $F_{p}(a)$ denotes a prohibition for party $p$ from achieving
$a$, and $P_{p}(a)$ denotes a permission/right for party $p$ to achieve $a$.

We call $c\mathcal{DL}$ specifications contracts. Contracts include norms, the
atomic satisfied ($\top$), and the transgressed ($\perp$) contract. Contracts
can be _conjuncts_ ($\wedge$) and _sequentially composed_ (;). A contract may
repair the violation of another ($C\blacktriangleright C^{\prime}$ means that
$C^{\prime}$ is the _reparation_ applied when $C$ is violated).

Contracts can be triggered when a regular expression matches tightly ($\langle
re\rangle C$). A regular expression can also guard  $\bumpeq$ a contract $C$,
such that an unrecoverable mismatch with it removes the need to continue
complying with $C$ in ($re\rotatebox[origin={c}]{-90.0}{$\bumpeq$}C$).

We allow recursive definitions of contracts ($rec~{}X.C$), where
$X\in\mathbb{X}$, with some restrictions. First, we do not allow a contract to
have two recursive sub-contracts using the same variable name. Secondly, we
have some syntactic restrictions on the contract $C$ appearing inside of the
recursion: $C$’s top-level operator is always a sequence, or a regular
expression trigger contract, with $X$ only appearing once and on the right-
hand side of a sequence, i.e., the expression must be tail recursive. We also
require an additional restriction for recursion with the reparation operator:
the reparation has to either not be the last operation before $X$ or the whole
recursion should be guarded with $re\rotatebox[origin={c}]{-90.0}{$\bumpeq$}$,
the reason behind it is to avoid the procrastination dilemma
[jackson1985semantics]. For example, $rec~{}X.\langle
re\rangle((C\blacktriangleright C^{\prime});X)$ and
$re\rotatebox[origin={c}]{-90.0}{$\bumpeq$}(rec~{}X.C\blacktriangleright X)$
are valid, unlike $rec~{}X.X$, $rec~{}X.C;(C^{\prime}\wedge X)$,
$rec~{}X.\langle re\rangle((C;X);C^{\prime})$, and
$rec~{}X.C\blacktriangleright X$. Moreover, a recursion variable
$X\in\mathbb{X}$ must always be bound when it appears in a contract.

In our setting, we want to be able to talk about collaborative actions
(actions that require both parties to be achieved successfully) and non-
interference between the parties (a party not being allowed to interfere with
the other party carrying out a certain action). We model both of these using a
notion of synchronicity. We will later represent parties as Moore machines;
here we talk just about their traces.

We assume two traces over $2^{\Sigma}$, one for each party: $w_{0}$ and
$w_{1}$. A party’s trace is a record of which actions were enabled (or
attempted) by that party. The step-wise intersection of these traces,
$w_{0}\sqcap w_{1}$, is the trace of successful actions. Restricting attention
to the successful actions misses information about attempts that were not
successful. Instead, we give semantics over pairs of party traces, an
interaction, rather than over $w_{0}\sqcap w_{1}$, allowing us to localise
interference. This setting allows us to model both collaboration and non-
interference between the parties in the same way. If the parties are required
to collaborate on an action, then they must both propose it (obligation). If
instead, the parties should ensure an action is not successful, then at least
one of them must not enable it (prohibition). If a party is required to not
interfere with another party’s action, then they must also enable it
(permission). We refer to actions of one party variously as _proposed_ ,
_attempted_ , or _enabled_ by that party. We consider an example specification
in our language.

######  Example 1.

Consider two possibly distinct robots, 0 and 1, working on a factory floor,
with their main goal being to cooperate in placing incoming packages on
shelves. Each robot has sensors to identify when a new package is in the queue
(detectProd), and they must lift the package together (lift), and place it on
a shelf (putOnShelf). Between iterations of this process, the robots are
individually allowed to go to their charging ports (charge0 or charge1). If a
robot does not help in lifting, it is given another chance:

$\displaystyle\textit{permitCharge}\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}$ $\displaystyle~{}P_{0}(\textit{charge0})\wedge
P_{1}(\textit{charge1})$
$\displaystyle\textit{lift}(p)\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}$ $\displaystyle~{}O_{p}(\textit{lift})\blacktriangleright
O_{p}(\textit{lift})$
$\displaystyle\textit{detect\&Lift}(p)\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}$
$\displaystyle~{}\langle\textit{detectProd}_{p}\rangle\textit{lift}(p)$
$\displaystyle\textit{detect\&Place}\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}$
$\displaystyle~{}(\textit{detect\&Lift}(0)\wedge\textit{detect\&Lift}(1))\,;$
$\displaystyle\,(O_{0}(\textit{putOnShelf})\wedge O_{1}(\textit{putOnShelf}))$
$\displaystyle\textit{collabRobot}\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}$
$\displaystyle~{}rec~{}X.\textit{permitCharge};\textit{detect\&Place};X.$

###  3.1 Informative Semantics

$\begin{array}[]{l<EMAIL_ADDRESS>def}}}{=}}&~{}\ i=j\\\ \vec{w}_{i}^{j}\models_{s}\
\perp&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny def}}}{=}}&~{}\
\textit{false}\\\
\vec{w}_{i}^{j}\models_{s}O_{p}(a)&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&~{}\ i=j\wedge a\in w_{0}[i]\text{ and }a\in w_{1}[i]\\\
\vec{w}_{i}^{j}\models_{s}F_{p}(a)&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&~{}\ i=j\wedge a\not\in w_{p}[i]\text{ or }a\not\in w_{1-p}[i]\\\
\vec{w}_{i}^{j}\models_{s}P_{p}(a)&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&~{}\ i=j\wedge a\in w_{p}[i]\text{ implies }a\in w_{1-p}[i])\\\
\vec{w}_{i}^{j}\models_{v}N&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&~{}\ i=j\wedge\vec{w}_{i}^{j}\not\models_{s}N\\\ \\\
\vec{w}_{i}^{j}\models_{s}\langle re\rangle
C&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny def}}}{=}}&~{}\
\vec{w}_{i}^{j}\in\overline{cl}(re)\text{ or }(\exists k<j:\vec{w}_{i}^{k}\in
TL(re)\text{ and }\vec{w}_{k+1}^{j}\models_{s}C)\\\
\vec{w}_{i}^{j}\models_{v}\langle re\rangle
C&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny def}}}{=}}&~{}\ \exists
k<j:\vec{w}_{i}^{k}\in TL(re)\text{ and }\vec{w}_{k+1}^{j}\models_{v}C\\\
\vec{w}_{i}^{j}\models_{s}re\rotatebox[origin={c}]{-90.0}{$\bumpeq$}C&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&~{}\ (\vec{w}_{i}^{j}\in\overline{cl}(re)\cup TL(re)\text{ and
}\nexists k<j:(\vec{w}_{i}^{k}\models_{v}C))\\\ &&~{}\ \text{ or
}(\vec{w}_{i}^{j}\in cl(re)\text{ and }\vec{w}_{i}^{j}\models_{s}C)\\\
\vec{w}_{i}^{j}\models_{v}re\rotatebox[origin={c}]{-90.0}{$\bumpeq$}C&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&~{}\ \vec{w}_{i}^{j}\in cl(re)\text{ and
}\vec{w}_{i}^{j}\models_{v}C\\\ \vec{w}_{i}^{j}\models_{s}C\wedge
C^{\prime}&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny def}}}{=}}&~{}\
\vec{w}_{i}^{k}\models_{s}C\text{ and
}\vec{w}_{i}^{l}\models_{s}C^{\prime}\text{ and }j=max(k,l)\\\
\vec{w}_{i}^{j}\models_{v}C\wedge
C^{\prime}&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny def}}}{=}}&~{}\
(\vec{w}_{i}^{j}\models_{v}C\text{ or
}\vec{w}_{i}^{j}\models_{v}C^{\prime})\text{ and }\nexists
k<j:\vec{w}_{i}^{k}\models_{v}C\wedge C^{\prime}\\\
\vec{w}_{i}^{j}\models_{s}C;C^{\prime}&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&~{}\ \exists k<j:\vec{w}_{i}^{k}\models_{s}C\text{ and
}\vec{w}_{k+1}^{j}\models_{s}C^{\prime}\\\
\vec{w}_{i}^{j}\models_{v}C;C^{\prime}&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&~{}\ (\exists k<j:\vec{w}_{i}^{k}\models_{s}C\text{ and
}\vec{w}_{k+1}^{j}\models_{v}C^{\prime})\text{ or
}\vec{w}_{i}^{j}\models_{v}C\\\ \vec{w}_{i}^{j}\models_{s}C\blacktriangleright
C^{\prime}&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny def}}}{=}}&~{}\
\vec{w}_{i}^{j}\models_{s}C\text{ or }(\exists
k<j:\vec{w}_{i}^{k}\models_{v}C\text{ and
}\vec{w}_{k+1}^{j}\models_{s}C^{\prime})\\\
\vec{w}_{i}^{j}\models_{v}C\blacktriangleright
C^{\prime}&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny def}}}{=}}&~{}\
\exists k<j:\vec{w}_{i}^{k}\models_{v}C\text{ and
}\vec{w}_{k+1}^{j}\models_{v}C^{\prime}\\\
\vec{w}_{i}^{j}\models_{s}rec~{}X.C&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&~{}\ \vec{w}_{i}^{j}\models_{s}C[X\backslash rec~{}X.C]\\\
\vec{w}_{i}^{j}\models_{v}rec~{}X.C&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&~{}\ \vec{w}_{i}^{j}\models_{v}C[X\backslash rec~{}X.C]\\\ \\\
\vec{w}_{i}^{j}\vDash_{?}C&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&~{}\ \nexists k\leq j:\vec{w}_{i}^{k}\models_{s}C\text{ or
}\vec{w}_{i}^{k}\models_{v}C\end{array}$ Figure 1: Informative semantics rules
over a finite interaction $\vec{w}_{i}^{j}$.

The semantics of our language is defined on an interaction, i.e. a pair of
traces $w_{0}$ and $w_{1}$, restricting our view to a slice with a minimal
position $i$ and maximal one $j$. For the remainder of this paper, we will
refer to this interaction with $\vec{w}_{i}^{j}$.

In Figure 1, we introduce the semantic relations for informative satisfaction
($\models_{s}$) and violation ($\models_{v}$). These capture the moment of
satisfaction and violation of a contract in a finite interaction. We use this
to later define when an infinite interaction models a contract. In Figure 1 we
also capture with $\vDash_{?}$, when the interaction slice neither
informatively satisfies nor violates the contract.

We give some intuition and mention interesting features of the semantics. Note
how we only allow the status of atomic contracts to be informatively decided
in one time-step (when $i=j$), given they only talk about one action. When it
comes to the trigger contract, our goal is to confirm its fulfillment only
when we no longer closely align with the specified trigger language.
Alternatively, we consider it satisfied if we’ve matched it previously and
subsequently maintained compliance with the contract. Conversely, we would
classify a violation if we achieved a close match but then deviated from the
contract’s terms. Regarding the regular expression guard, we have two
scenarios for evaluating satisfaction. First, we ensure satisfaction when
either we have precisely matched the language or have taken actions preventing
any future matching of the guard, with no prior violations or the guarded
contract. Second, we verify satisfaction when there’s still a possibility of a
precise match of the guard, and the guarded contract has already been
satisfied. In contrast, a violation occurs when there remains a chance for a
precise match in the future of the guard, and a violation of the sub-contract
occurs.

The definitions for conjunction and sequence are relatively simple. Note that
for conjunction we take the maximum index at which both contracts have been
satisfied. Sequence and reparation are similar, except in reparation we only
continue in the second contract if the first is violated, while we violate it
if both contracts end up being violated. For recursion, we simply re-write
variable $X$ as needed to determine satisfaction or violation.

######  Example 2.

Note how the semantics ensure that, given traces $w_{0}$ and $w_{1}$ such that
$w_{0}[0]=w_{1}[1]=\\{\textit{charge0},\textit{charge1}\\}$ then
$\vec{w}_{0}^{0}\models_{s}permitCharge$, i.e. both robots try to charge and
allow each other to charge. But if further
$w_{0}[1..3]=\langle\\{\textit{detectProd}\\},\\{\textit{lift}\\},\\{\textit{lift}\\}\rangle$
and $w_{1}[1..3]=\langle\\{\\},\\{\\}.\\{\\}\rangle$, then
$\vec{w}_{0}^{3}\models_{v}CollabRobot$, since robot 0 attempted a lift but
robot 1 declined helping in lifting.

######  Lemma 1.

Given an interaction, we can always transform a contract with top-level
recursion into an equivalent one that is free of recursion.

###### Proof.

We recall that recursion here is restricted, such that $X$ never appears at
the top-level of the contract, but always on the right-hand side of a contract
that requires another contract or regular expression to be evaluated before.
Thus, before the meaning of $X$ needs to be resolved there is always a time-
step before where another part of the contract is being evaluated. Thus, given
a finite interaction $\vec{w}_{i}^{j}$, which has the size $j-i+1$, we can
always unroll all the recursion in a contract $j-i$ times. By replacing the
remaining recursive contracts with $\top$, we get a contract without recursion
that is equivalent to the original one for all finite traces of size $j-i$ for
informative satisfaction and violation. ∎∎

Then, we show that if a contract is informatively satisfied (violated), then
any suffix or prefix of the interaction cannot also be informatively satisfied
(violated): [Unique satisfaction and violation] If there exists $j$ and $k$
such that $\vec{w}_{i}^{j}\models_{s}C$ and $\vec{w}_{i}^{k}\models_{s}C$,
then $j=k$. Similarly, if there exists $j$ and $k$ such that
$\vec{w}_{i}^{j}\models_{v}C$ and $\vec{w}_{i}^{k}\models_{v}C$ then $j=k$. We
prove this by structural induction (here we use satisfies/violates for
informatively satisfies/violates):

#### Base Case

: For $\top$, $\perp$, $O_{p}$, $P_{p}$, and $F_{p}$ this holds immediately by
definition.

#### Inductive Hypothesis (IH)

: We assume the lemma holds for contracts $C$ and $C^{\prime}$, for any $i$,
$j$, and $k$.

#### Inductive Step

: We prove the result holds for contracts built over $C$ and $C^{\prime}$:

  * •

$\langle re\rangle C$:

    1. 1.

By definition of $\models_{s}$, we have two different cases when a formula is
informatively satisfied:

      1. (a)

Either there is a point in time ($m$) at which the regular expression tightly
matches (which by definition of $TL$ we are assured happens at only one point
in a trace), and that $C$ holds on the rest of trace; applying the IH here
(setting $i$ to $m$) we are assured the lemma holds for $\langle re\rangle C$.

      2. (b)

Or there is no such point in time, but instead $j$ and $k$ are points in time
where the trace breaks the safety of the regular expression. The definition
here requires that every strict prefix of the trace is in $cl(re)\setminus
TL(re)$ and that the full (finite) trace is in $\overline{cl}(re)$. The first
condition ensures no prefix is in $\overline{cl}(re)$, by their respective
definitions. This ensures that once a $j$ is found where this case holds,
there is no bigger (or smaller) $k$, ensuring the lemma.

    2. 2.

By definition of $\models_{v}$, we have one case, where is a point in time
where the regular expression tightly matches, and the contract is violated.
Since the point of tight matching $m$ is unique, and by applying the IH on $C$
(setting $i$ to $m$), then the lemma follows.

  * •

$re\rotatebox[origin={c}]{-90.0}{$\bumpeq$}C$:

    1. 1.

By definition of $\models_{s}$, we have two different cases when a formula is
informatively satisfied:

      1. (a)

The trace is in ${cl}(re)$ and it satisfies $C$, and thus the result follows
by simply applying IH on $C$.

      2. (b)

The trace is in $\overline{cl}(re)$ and there is no prefix that violates $C$.
The definition of $\overline{cl}(re)$ ensures that any prefix in not in
${cl}(re)$, and also the definition of ${cl}(re)$ ensures that any extension
of $\overline{cl}(re)$ is not in ${cl}(re)$. And thus the other case does not
hold for strict prefixes and suffixes of a trace that satisfies this case.
Moreover, the definition of $\overline{cl}(re)$ moreover ensures no strict
prefix or suffix of the trace is also in $\overline{cl}(re)$, ensuring the
required result.

    2. 2.

By definition of $\models_{v}$, we have one case, where the trace is in
${cl}(re)$, and the contract is violated, and thus the required result follows
by simply applying the IH on $C$.

  * •

$C\wedge C^{\prime}$:

    1. 1.

For satisfaction, the result follows by applying the IH in both $C$ and
$C^{\prime}$, and taking their maximum. Since the point of satisfaction for
both is assured to be unique, so is their maximum.

    2. 2.

For violation, one of the contracts must violate (and thus apply the IH on
that contract). Both contracts may be violated at different times, but the
second requirement of the definition ensures that we are taking the minimum of
such time points.

  * •

$C;C^{\prime}$:

    1. 1.

For satisfaction, the result follows easily by first applying the IH on $C$
and then on $C^{\prime}$ (setting $i$ to the unique point of
satisfaction/violation of $C$).

    2. 2.

For violation, the result follows similarly, by applying, for the first case,
the satisfaction part of the IH on $C$, and the violation part on
$C^{\prime}$, and for the second case the violation of IH on $C$.

  * •

$C\blacktriangleright C^{\prime}$:

    1. 1.

For satisfaction we have two cases:

      1. (a)

$C$ is satisfied, and the result holds by the IH.

      2. (b)

$C$ is violated, which the IH ensures this is at a unique time point; and
$C^{\prime}$ is then satisfied from that time point, which the IH also ensures
is at a unique time point.

    2. 2.

For violation we have one case, $C$ is violated (at a unique time point, by
IH), and from that point, $C^{\prime}$ is also violated at the end of the
trace, which is ensured to be a unique time point, by IH.

  * •

$rec~{}X.C$: We apply 1, and rely on the inductive hypothesis. ∎

For the atomic contracts, this is clear. By structural induction, the result
follows for conjunction, sequence, and reparation. For the trigger operations,
the definition of $TL$ ensures the result. For recursion, note how given a
finite interaction there is always a finite amount of times the recursion can
be unfolded (with an upper bound of $j-i$) so that we can determine
satisfaction or violation in finite time. (See the Appendix for a detailed
proof.333All the proofs of lemmas, propositions and theorems of this and next
section may be found in the appendix.)

If an interaction is not informative for satisfaction, it is not necessarily
informative for violation, and vice-versa. But we can show that if there is a
point of informative satisfaction then there is no point of informative
violation.

[Disjoint satisfaction and violation] Informative satisfaction and violation
are disjoint: there are no $j,k$ s.t. $\vec{w}_{i}^{j}\models_{s}C$ and
$\vec{w}_{i}^{k}\models_{v}C$. We prove this by structural induction that for
all possible words, it is impossible for there to be prefixes of an
interaction that both informatively satisfy and violate the same contract.

#### Base Case

: For Contracts of $\top$, $\perp$, $O_{p}$, $P_{p}$, and $F_{p}$ this holds
by definition.

#### Inductive Hypothesis (IH)

: We assume the lemma holds for contracts $C$ and $C^{\prime}$, for any $i$,
$j$, and $k$.

#### Inductive Step

: We prove the result holds for contracts built over $C$ and $C^{\prime}$:

Throughout we start by assuming that the contract is satisfied between $i$ and
$j$, and violated between $i$ and $k$. Then we consider all the possible three
cases, $j$ is less than, bigger than, or equal to $k$.

  * •

$\langle re\rangle C$ – For satisfaction, we assume that either: (1)
$\vec{w}_{i}^{j}$ is in the complement closure of $re$, or (2) the prefix can
be split into two finite traces, where the first tightly matches $re$ and the
other informatively satisfies $C$.

    1. 1.

$j<k$: Given (1), consider that traces in the complement closure cannot have
prefixes in the tight language, or be in the tight language. For (2), the
prefix in the tight language is unique, thus the result follows by using the
inductive hypothesis on the suffix and $C$.

    2. 2.

$j>k$: Given (1), the contract cannot be violated, since suffixes in the
complement closure cannot be in the tight language. For (2), as before, the
prefix in the tight language is unique, thus the result follows by using the
inductive hypothesis on the suffix and $C$.

    3. 3.

$j=k$: Consider that a trace cannot be in the complement closure and the tight
language at the same time, while the inductive hypothesis discharges the
second proof obligation, as for the other cases.

  * •

$re\rotatebox[origin={c}]{-90.0}{$\bumpeq$}C$ – For satisfaction, we assume
that either: (1) $\vec{w}_{i}^{j}$ is in the complement closure or tight
language of $re$ and the contract was not previously violated, or (2)
$\vec{w}_{i}^{j}$ is in the closure, and the contract is informatively
satisfied.

    1. 1.

$j<k$: Given (1), and that no extension of a trace in the complement closure
can be in the closure, the result follows. Given (2), the result follows by
the inductive hypothesis.

    2. 2.

$j>k$: The result needed (no previous violation) follows immediately in case
(1). For (2), the result follows by the inductive hypothesis.

    3. 3.

$j=k$: Given (1), violation cannot be the case given a trace cannot both be in
the complement closure and the closure. Given (2) the result follows by the
inductive hypothesis.

  * •

$C\wedge C^{\prime}$ – The result here follows easily from the inductive
hypothesis.

  * •

$C;C^{\prime}$ – Satisfaction requires $\vec{w}_{i}^{j}$ to be split into two,
where $\vec{w}_{i}^{l}$ satisfies $C$ and $\vec{w}_{l+1}^{j}$ satisfies
$C^{\prime}$.

    1. 1.

$j<k$: By the inductive hypothesis, $C$ must be satisfied on a prefix of
$\vec{w}_{i}^{k}$, then $C^{\prime}$ is violated on the remaining suffix.
However, this suffix must be a prefix of $\vec{w}_{l+1}^{j}$, thus the result
follows the inductive hypothesis.

    2. 2.

The proof for the remaining cases mirrors the previous cases’ proof.

  * •

$C\blacktriangleright C^{\prime}$ — The proof follows similarly to that of
sequence.

  * •

$recX.C$ – We apply 1, and rely on the inductive hypothesis.

The proof follows easily by induction on the structure of C.

We can then give semantics to infinite interactions.

######  Definition 2 (Models).

For an infinite interaction $\vec{w}_{0}^{\infty}$, and a $c\mathcal{DL}$
contract $C$, we say $\vec{w}_{0}^{\infty}$ models a contract $C$, denoted by
$\vec{w}_{0}^{\infty}\vDash C$, when there is no prefix of the interaction
that informatively violates $C$: $\vec{w}_{0}^{\infty}\vDash
C\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny def}}}{=}}\nexists
k\in\mathbb{N}\cdot\vec{w}_{0}^{k}\models_{v}C$.

###  3.2 Blame Assignment

$\begin{array}[]{l<EMAIL_ADDRESS>def}}}{=}}&\textit{false}\\\
\vec{w}_{i}^{j}\models_{v}^{p}\bot&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&\textit{false}\\\
\vec{w}_{i}^{j}\models_{v}^{p}O_{1-p}(a)&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&i=j\wedge a\in w_{1-p}[i]\text{ and }a\not\in w_{p}[i]\\\
\vec{w}_{i}^{j}\models_{v}^{p}O_{p}(a)&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&i=j\wedge a\not\in w_{p}[i]\\\
\vec{w}_{i}^{j}\models_{v}^{p}F_{1-p}(a)&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&\textit{false}\\\
\vec{w}_{i}^{j}\models_{v}^{p}F_{p}(a)&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&i=j\wedge a\in w_{p}[i]\text{ and }a\in w_{1-p}[i]\\\
\vec{w}_{i}^{j}\models_{v}^{p}P_{1-p}(a)&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&i=j\wedge a\in w_{1-p}[i]\text{ and }a\not\in w_{p}[i]\\\
\vec{w}_{i}^{j}\models_{v}^{p}P_{p}(a)&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&\textit{false}\\\ \vec{w}_{i}^{j}\models_{v}^{p}\langle re\rangle
C&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny def}}}{=}}&\exists
k<j:\vec{w}_{i}^{k}\models_{s}TL(re)\text{ and
}\vec{w}_{k+1}^{j}\models_{v}^{p}C\\\
\vec{w}_{i}^{j}\models_{v}^{p}re\rotatebox[origin={c}]{-90.0}{$\bumpeq$}C&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&\vec{w}_{i}^{j}\in cl(re)\text{ and
}\vec{w}_{i}^{j}\models_{v}^{p}C\\\ \vec{w}_{i}^{j}\models_{v}^{p}C\wedge
C^{\prime}&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&(\vec{w}_{i}^{j}\models_{v}^{p}C\text{ or
}\vec{w}_{i}^{j}\models_{v}^{p}C^{\prime})\text{ and }\\\ &&(\nexists
k<j:\vec{w}_{i}^{k}\models_{v}^{1-p}C\wedge C^{\prime})\text{ and }\\\
&&\lnot(\textit{conflict}(C,C^{\prime},\vec{w}_{i}^{j-1}))\\\
\vec{w}_{i}^{j}\models_{v}^{p}C\blacktriangleright
C^{\prime}&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny def}}}{=}}&\exists
k:\vec{w}_{i}^{k}\models_{v}C\text{ and
}\vec{w}_{k+1}^{j}\models_{v}^{p}C^{\prime}\\\
\vec{w}_{i}^{j}\models_{v}^{p}rec~{}X.C&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&\vec{w}_{i}^{j}\models_{v}^{p}C[X\backslash rec~{}X.C]\end{array}$
Figure 2: Blame semantics rules over a finite interaction $\vec{w}_{i}^{j}$

We are not interested only in whether a contract is satisfied or violated, but
also on _causation_ and _responsibility_ [ChocklerH03, halpern2015,
chockler2004responsibility]. Here we give a relation that identifies when a
party is responsible for a violation at a certain point in an interaction.
Blame assignment could be specified following multiple criteria, we assign
blame when an agent neglects to perform an action it is obliged to do or that
another agent is obliged to do (passive blame), or for attempting to do an
action it is forbidden from doing (active blame). The blame is forward looking
where we identify the earliest cause of violation. Furthermore, we are only
interested in causation and not on more advanced features such as "moral
responsibility" or "intentionality". The blame semantics is only defined as a
violation by party $p$ relation as in $\models_{v}^{p}$. This semantics is
defined in Figure 2.

For blame assignment, the labeling of norms with parties is crucial. Here we
give meaning to these labels in terms of who is the main subject of the norm
in question. For example, consider that $O_{0}(a)$ can be violated in three
ways: either (i) both parties do not attempt $a$, (ii) party $0$ does not
attempt $a$ but party $1$ does, or (iii) party $0$ attempts $a$ but party $1$
does not. Our interpretation is that since party $0$ is the main subject of
the obligation, party $0$ is blamed when it does not attempt $a$ (cases (i)
and (ii)), but party $1$ is blamed when it does not attempt $a$ (case (iii)).
The intuition is that by not attempting $a$, party $0$ violated the contract,
thus relieving party $1$ of any obligation to cooperate or non-interfere
(given party $0$ knows there is no hope for the norm to be satisfied if they
do not attempt $a$). We use similar interpretations for the other norms.

Another crucial observation is that violations of a contract are not
necessarily caused by a party. For example, the violated contract $\perp$
cannot be satisfied. Moreover, norms can conflict, e.g., $O_{p}(a)\wedge
F_{p}(a)$. Conflicts are not immediately obvious without some analysis, e.g.,
$\langle re\rangle O_{p}(a)\wedge\langle re^{\prime}\rangle F_{p}(a)$ (where
there is some interaction for which $re$ and $re^{\prime}$ tightly match at
the same time). We provide machinery to talk about conflicts, to avoid unsound
blaming, by characterising two contracts to be conflicting when there is no
way to satisfy them together.

######  Definition 3 (Conflicts).

Two contracts $C$ and $C^{\prime}$ are in conflict after a finite interaction
$\vec{w}_{i}^{j}$ if at that point their conjunction has not been
informatively satisfied or violated yet, but all possible further steps lead
to its violation:
$\textit{conflict}(C,C^{\prime},\vec{w}_{i}^{j})\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\nexists\vec{w}^{\prime}:\vec{w^{\prime}}_{i}^{j}=\vec{w}_{i}^{j}\wedge\vec{w^{\prime}}_{i}^{j+1}\not\models_{v}C\wedge
C^{\prime}$.

Another instance of a conflict can be observed between
$C_{1}=O_{0}(a);F_{1}(c)$ and $C_{2}=O_{0}(b)\blacktriangleright O_{0}(c)$ at
the second position. This can be demonstrated with a trace of length one,
$\langle a_{0};a_{1}\rangle$, where the obligation to achieve $c$ for party
$0$ and the prohibition to achieve $c$ for party $1$ have to be enforced
simultaneously.

######  Example 3.

Recall the violating example in Example. 2, where robot 1 declines in helping
lifing, twice. Clearly in that case $\vec{w}_{0}^{3}\models_{v}^{1}\text{
collabRobot }$. However, if robot 0 did not attempt a lift in position 3
(i.e., to attempt to satisfy the reparation), the blame would be on the other
agent.

From the definition of blame it easily follows that a party is blamed for a
violation only when there is a violation:

######  Proposition 1.

If a party $p$ is blamed for the violation of $C$ then $C$ has been violated:
$\exists p\cdot\vec{w}_{i}^{j}\models_{v}^{p}C$ implies
$\vec{w}_{i}^{j}\models_{v}C$.

###### Proof.

Note how each case of $\models_{v}^{p}$ implies its counterpart in
$\models_{v}$. ∎

But the opposite is not true:

######  Proposition 2.

A contract may be violated but both parties be blameless:
$\vec{w}_{i}^{j}\models_{v}C$ does not imply $\exists
p\cdot\vec{w}_{i}^{j}\models_{v}^{p}C$.

###### Proof.

Consider their definitions on $\bot$, and given conjunction and the presence
of conflicts. ∎

######  Proposition 3 (Satisfaction implies no blame).

Satisfaction of contract $C$ means that no party will get blamed:
$\vec{w}_{i}^{j}\models_{s}C$ implies $\nexists
p\cdot\vec{w}_{i}^{j}\models_{v}^{p}C$

###### Proof.

Assume the contrary, i.e. that $C$ is satisfied but party $p$ is blamed. By
Proposition 1 then there is a violation, but Lemma 3.1 implies we cannot both
have a satisfaction or violation. ∎

For any contract $C^{\not{\bot}}$ defined on $c\mathcal{DL}$ free of $\bot$
and free of conflicts, the violation of a contract $C^{\not{\bot}}$ leads to
blame.

[Double blame] Double blame in $c\mathcal{DL}$ for both parties $p$ and $1-p$
is possible. Consider $C=O_{p}(a)\wedge O_{p}(b)$. Violation of the left-hand
side by $p$ and the violation of the right-hand side by $1-p$ can happen at
the same time.

###  3.3 Quantitative Semantics

$\begin{array}[]{l@{\quad}r@{\quad}l}\vec{w}_{i}^{j},\rho\sttstile{}{}_{s}^{p}N&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&\rho=0\wedge\vec{w}_{i}^{j}\models_{s}N\\\
\vec{w}_{i}^{j},\rho\sttstile{}{}_{v}^{p}N&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&\left\\{\begin{array}[]{lll}\rho=1&\quad\text{if}&\vec{w}_{i}^{i}\models_{v}^{p}N\\\
\rho=0&\quad\text{if}&N=\perp\vee\vec{w}_{i}^{i}\models_{v}^{1-p}N\\\
\end{array}\right.\\\
\vec{w}_{i}^{j},\rho\sttstile{}{}_{?}^{p}N&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&\textit{false}\\\ \vec{w}_{i}^{j},\rho\sttstile{}{}_{s}^{p}\langle
re\rangle C&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&\left\\{\begin{array}[]{lll}\rho=0&\quad\text{if}&\vec{w}_{i}^{j}\in\overline{cl}(re)\\\
\vec{w}_{k+1}^{j},\rho\sttstile{}{}_{s}^{p}C&\quad\text{if}&\exists
k:\vec{w}_{i}^{k}\in TL(re)\\\ \end{array}\right.\\\
\vec{w}_{i}^{j},\rho\sttstile{}{}_{v}^{p}\langle re\rangle
C&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny def}}}{=}}&\exists
k:\vec{w}_{i}^{k}\in TL(re)\text{ and
}\vec{w}_{k+1}^{j},\rho\sttstile{}{}_{v}^{p}C\\\
\vec{w}_{i}^{j},\rho\sttstile{}{}_{?}^{p}\langle re\rangle
C&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&\left\\{\begin{array}[]{lcl}\rho=0&\text{if}&\nexists k\leq
j:\vec{w}_{i}^{k}\in TL(re)\\\
\vec{w}_{k+1}^{j},\rho\sttstile{}{}_{?}^{p}C&\quad\text{else}&\exists k\leq
j:\vec{w}_{i}^{k}\in TL(re)\\\ \end{array}\right.\\\
\vec{w}_{i}^{j},\rho\sttstile{}{}_{s}^{p}re\rotatebox[origin={c}]{-90.0}{$\bumpeq$}C&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&\left\\{\begin{array}[]{lll}\vec{w}_{i}^{j-1},\rho\sttstile{}{}_{?}^{p}C&\text{if}&\vec{w}_{i}^{j}\in\overline{cl}(re)\cup
TL(re)\\\ &&\textit{ and
}\nexists\rho^{\prime},k<j:\vec{w}_{i}^{k},\rho^{\prime}\sttstile{}{}_{v}^{p}C\\\
\vec{w}_{i}^{j},\rho\sttstile{}{}_{s}^{p}C&\text{if
}&\vec{w}_{i}^{j}\in{cl}(re)\\\ \end{array}\right.\\\
\vec{w}_{i}^{j},\rho\sttstile{}{}_{v}^{p}re\rotatebox[origin={c}]{-90.0}{$\bumpeq$}C&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&\vec{w}_{i}^{j}\in{cl}(re)\text{ and
}\vec{w}_{i}^{j},\rho\sttstile{}{}_{v}^{p}C\\\
\vec{w}_{i}^{j},\rho\sttstile{}{}_{?}^{p}re\rotatebox[origin={c}]{-90.0}{$\bumpeq$}C&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&\vec{w}_{i}^{j}\in{cl}(re)\text{ and
}\vec{w}_{i}^{j},\rho\sttstile{}{}_{?}^{p}C\\\
\vec{w}_{i}^{j},(\rho_{1}+\rho_{2})\sttstile{}{}_{s}^{p}C\wedge
C^{\prime}&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny def}}}{=}}&\exists
k,l:\vec{w}_{i}^{k},\rho_{1}\sttstile{}{}_{s}^{p}C\text{ and
}\vec{w}_{i}^{l},{\rho_{2}}\sttstile{}{}_{s}^{p}C^{\prime}\\\ &&\text{ and
}j=max(k,l)\\\ \vec{w}_{i}^{j},(\rho_{1}+\rho_{2})\sttstile{}{}_{v}^{p}C\wedge
C^{\prime}&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&((\vec{w}_{i}^{j},\rho_{2}\sttstile{}{}_{v}^{p}C^{\prime}\text{ or
}\vec{w}_{i}^{j},\rho_{2}\sttstile{}{}_{s}^{p}C^{\prime})\\\ &&\qquad\text{
and }\vec{w}_{i}^{j},\rho_{1}\sttstile{}{}_{v}^{p}C)\\\ &&\text{ or
}((\vec{w}_{i}^{j},\rho_{1}\sttstile{}{}_{v}^{p}C^{\prime}\text{ or
}\vec{w}_{i}^{j},\rho_{1}\sttstile{}{}_{s}^{p}C^{\prime})\\\ &&\qquad\text{
and }\vec{w}_{i}^{j},\rho_{2}\sttstile{}{}_{v}^{p}C^{\prime})\\\ &&\text{ or
}(\vec{w}_{i}^{j},\rho_{1}\sttstile{}{}_{v}^{p}C\text{ and
}\vec{w}_{i}^{j},\rho_{2}\sttstile{}{}_{v}^{p}C^{\prime}\\\ &&\qquad\text{ and
}\neg\textit{conflict}(C,C^{\prime},\vec{w}_{i}^{j-1}))\\\ &&\text{ or
}(\vec{w}_{i}^{j-1},\rho_{1}\sttstile{}{}_{?}^{p}C\text{ and
}\vec{w}_{i}^{j-1},\rho_{2}\sttstile{}{}_{?}^{p}C^{\prime}\\\ &&\qquad\text{
and }\textit{conflict}(C,C^{\prime},\vec{w}_{i}^{j-1}))\\\
\vec{w}_{i}^{j},(\rho_{1}+\rho_{2})\sttstile{}{}_{?}^{p}C\wedge
C^{\prime}&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&(\vec{w}_{i}^{j},\rho_{1}\sttstile{}{}_{s}^{p}C\text{ and
}\vec{w}_{i}^{j},\rho_{2}\sttstile{}{}_{?}^{p}C^{\prime})\\\ &&\text{ or
}(\vec{w}_{i}^{j},\rho_{1}\sttstile{}{}_{?}^{p}C\text{ and
}\vec{w}_{i}^{j},\rho_{2}\sttstile{}{}_{s}^{p}C^{\prime})\\\
\vec{w}_{i}^{j},(\rho_{1}+\rho_{2})\sttstile{}{}_{s}^{p}C;C^{\prime}&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&\exists k<j:\vec{w}_{i}^{k},\rho_{1}\sttstile{}{}_{s}^{p}C\text{
and }\vec{w}_{k+1}^{j},{\rho_{2}}\sttstile{}{}_{s}^{p}C^{\prime}\\\
\vec{w}_{i}^{j},\rho\sttstile{}{}_{v}^{p}C;C^{\prime}&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&\left\\{\begin{array}[]{lll}\rho=\rho_{1}+\rho_{2}&\text{if}&\exists
k<j:\vec{w}_{i}^{k},\rho_{1}\sttstile{}{}_{s}^{p}C\\\ &&\text{ and
}\vec{w}_{k+1}^{j},\rho_{2}\sttstile{}{}_{v}^{p}C^{\prime}\\\
\vec{w}_{i}^{j},\rho\sttstile{}{}_{v}^{p}&\text{else}&\\\
\end{array}\right.\\\
\vec{w}_{i}^{j},(\rho_{1}+\rho_{2})\sttstile{}{}_{?}^{p}C~{};~{}C^{\prime}&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&\vec{w}_{i}^{j},\rho\sttstile{}{}_{?}^{p}C\\\ &&\quad\text{ or
}(\vec{w}_{i}^{k},\rho_{1}\sttstile{}{}_{s}^{p}C\text{ and
}\vec{w}_{k+1}^{j},{\rho_{2}}\sttstile{}{}_{?}^{p}C^{\prime})\\\
\vec{w}_{i}^{j},\rho\sttstile{}{}_{s}^{p}C\blacktriangleright
C^{\prime}&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&\vec{w}_{i}^{j},\rho\sttstile{}{}_{s}^{p}C\\\ &&\text{ or }(\exists
k<j:\vec{w}_{i}^{k},\rho_{1}\sttstile{}{}_{v}^{p}C\\\ &&\quad\text{ and
}\vec{w}_{k+1}^{j},\rho_{2}\sttstile{}{}_{s}^{p}C\wedge\rho=\rho_{1}+\rho_{2})\\\
\vec{w}_{i}^{j},(\rho_{1}+\rho_{2})\sttstile{}{}_{v}^{p}C\blacktriangleright
C^{\prime}&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny def}}}{=}}&(\exists
k<j:\vec{w}_{i}^{k},{\rho_{1}}\models_{v}^{p}C\text{ and
}\vec{w}_{k+1}^{j},{\rho_{2}}\sttstile{}{}_{v}^{p}C^{\prime})\\\
\vec{w}_{i}^{j},\rho\sttstile{}{}_{?}^{p}C\blacktriangleright
C^{\prime}&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&\left\\{\begin{array}[]{lll}\rho=\rho_{1}+\rho_{2}&\text{if}&\vec{w}_{i}^{k},\rho_{1}\sttstile{}{}_{v}^{p}C\\\
&&\text{ and }\vec{w}_{k+1}^{j},{\rho_{2}}\sttstile{}{}_{?}^{p}C^{\prime}\\\
\vec{w}_{i}^{j},\rho\sttstile{}{}_{?}^{p}C&\text{else}\end{array}\right.\\\
\vec{w}_{i}^{j},\rho\sttstile{}{}_{\gamma}^{p}rec~{}X.C&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&\vec{w}_{i}^{j},\rho\sttstile{}{}_{\gamma}^{p}C[X\setminus
rec~{}X.C]\qquad\text{for }\gamma\in\\{s,v,?\\}\end{array}$ Figure 3:
Quantitative semantics rules over a finite interaction $\vec{w}_{i}^{j}$.

While it is possible to assign blame to one party for violating a contract,
other qualitative metrics can provide additional information about the
violation. These metrics can determine the number of violations caused by each
party, as well as the level of satisfaction with the contract. To assess
responsibility for contract violations, we introduce the notion of a mistake
score, $\rho$, for each party, enabling us to calculate a responsibility
degree. It is important to note that our language permits reparations, whereby
violations can be corrected in the next time step. However, interactions that
are satisfied with reparations are not considered ideal. We present
quantitative semantics to compare satisfying interactions based on the number
of repaired violations a party incurs. We define relations that track the
number of repaired violations attributed to each party with a mistake score,
$\rho$, written $\sttstile{}{}_{s}^{p}$ for informative satisfaction and
$\sttstile{}{}_{v}^{p}$ for informative violation of the contract. We can also
keep track of the number of violations when the trace is not informative
through $\sttstile{}{}_{?}^{p}$. Figure 3 provides a definition of this
semantics. Note this definition intersects the previous semantic definitions,
and due to space constraints, we do not re-expand that further. The addition
is that we are disambiguating some cases to identify when to add to the score
to identify a violation caused by $p$. For example, see the definition of
$\sttstile{}{}_{v}^{p}$ for a norm.

######  Example 4.

Consider again Example 1, and consider the finite interaction
$(\langle\\{\textit{charge0}\\},\\{\textit{detectProd}\\},\\{\\},\\{\textit{lift}\\}\rangle$
and
$\langle\\{\textit{charge0}\\},\\{\\},\\{\textit{lift}\\},\\{\textit{lift}\\}\rangle$.
Note how this will lead to robot 0 being given a score of one since on the
third step there is a violation that is repaired subsequently.

[Soundness and completeness] The quantitative semantics is sound and complete
with regard to the informative semantics:
$\vec{w}_{i}^{j}\models_{\gamma}C\iff\exists\rho_{1},\rho_{2}:\vec{w}_{i}^{j},{\rho_{1}}\sttstile{}{}_{v}^{p}C\text{
and }\vec{w}_{i}^{j},{\rho_{2}}\sttstile{}{}_{v}^{1-p}$ with
$\gamma\in\\{s,v,?\\}.$ By induction on the quantitative semantics and
informative semantics. We prove this by structural induction on C.

#### Base Case

: For atomic contracts the result follows easily.

#### Inductive Hypothesis

: We assume the lemma holds for contracts $C$ and $C^{\prime}$, for any $i$
and $j$.

#### Inductive Step

: We prove the result holds for contracts built over $C$ and $C^{\prime}$:

  * •

$\langle re\rangle C$ –

    1. 1.

For satisfaction, note the conditions in the quantitative semantics cover all
the cases in the informative satisfaction semantics, thus by the inductive
hypothesis the result immediately follows.

    2. 2.

The argument for violation follows similarly.

    3. 3.

For $?$, consider that the cases imply either that the finite interaction is
inside the closure (thus there is no satisfaction and no violation), or that a
prefix is in the tight language, and the status of $C$ is unknown. The result
follows by applying the inductive hypothesis on the latter.

  * •

$re\rotatebox[origin={c}]{-90.0}{$\bumpeq$}C$ –

    1. 1.

For satisfaction, note how the first condition ensures we are in the
complement closure or tight language, and that the contract has not been
previously violated, as in the informative semantics, while applying the
inductive hypothesis on the return hypothesis ensures the contract was not
satisfied in the previous step in both the quantitative and informative, as
required, but gives a value for $\rho$. For the second condition, this also
matches the respective disjunct in the informative semantics, and we apply the
inductive hypothesis on the result to get what is needed.

    2. 2.

For violation, again the definition mirrors the informative semantics and we
can just apply the inductive hypothesis.

    3. 3.

For $?$ we can apply the inductive hypothesis, and discern that the
requirement that the finite interaction is in the closure of $re$ follows from
the informative definition of $?$.

  * •

$C\wedge C^{\prime}$ –

    1. 1.

For satisfaction, the definitions mirror each other, and applying the
inductive hypothesis gives us what we need.

    2. 2.

For violation, in the quantitative semantics we enumerate every possible way
to violate the conjunction. This corresponds to the informative definition,
however, we present it differently, by checking that no prefix also violates
the contract. The two approaches are equivalent. By applying the inductive
hypothesis, and comparing each resulting disjunct from the quantitative
definition to the informative definition we get the result we need. Note the
conditions cover all possible combinations leading to a violation. For
example, for the first case
$(\vec{w}_{i}^{j},\rho_{1}\sttstile{}{}_{v}^{p}C\text{ and
}(\vec{w}_{i}^{j},\rho_{2}\sttstile{}{}_{v}^{p}C^{\prime}\text{ or
}\vec{w}_{i}^{j},\rho_{2}\sttstile{}{}_{s}^{p}C^{\prime}))$ iff, by the
inductive hypothesis, $(\vec{w}_{i}^{j}\models_{v}C\text{ and
}(\vec{w}_{i}^{j}\vDash_{?}C^{\prime}\text{ or
}\vec{w}_{i}^{j}\models_{s}C^{\prime})$, which in turn implies the informative
definition.

Here we also deal with conflicts for the purpose of incrementing the score in
case of a conflict, this does not affect the correctness of our argument.

    3. 3.

For $?$, note how applying the inductive hypothesis, the results cover the
exact cases where the determination remains unknown.

  * •

$C;C^{\prime}$

    1. 1.

For satisfaction and violation, the quantitative definition mirrors the
informative definition, and the result then immediately follows from the
inductive hypothesis.

    2. 2.

For $?$, the quantitative definition can be easily seen to cover all cases
where there is no violation in the informative definition, the result follows
from the inductive hypothesis.

  * •

$C\blacktriangleright C^{\prime}$ –

    1. 1.

For satisfaction and violation, the quantitative definition mirrors the
informative definition, and the result then immediately follows from the
inductive hypothesis.

    2. 2.

For $?$, the quantitative definition can be easily seen to cover all cases
where there is no violation in the informative definition, the result follows
from the inductive hypothesis.

  * •

$recX.C$

    1. 1.

By Lemma 1 and the inductive hypothesis the result follows.

[Fairness of the Quantitative semantics] The quantitative semantic is fair,
meaning that if the score of a player $p$ is $\rho$ then $p$ is to be blamed
for non-fulfilling $\rho$ norms of the contract:
$\vec{w}_{i}^{j},\rho\sttstile{}{}_{\gamma}^{p}C\implies\exists N_{1}\dots
N_{\rho}\in\textit{subcontracts}(C):\vec{w}_{i}^{j}\sttstile{}{}_{\gamma}^{p}N_{i}$
with $\gamma\in\\{s,v,?\\}$, where $\textit{subcontracts}(C)$ is a multiset
containing the subcontracts of $C$, up to how often they appear. We prove,
this by structural induction, noting that the score only increases when $p$ is
blamed for the violation of a norm, while the inductive case easily follows
from the inductive hypothesis. We prove this by structural induction on C.

#### Base Case

: By analysis of the definition, one can easily see that $\rho$ is set to $1$
only when party $p$ is to blame for the violation of a norm.

#### Inductive Hypothesis (IH)

: We assume the lemma holds for contracts $C$ and $C^{\prime}$, for any $i$,
$j$, and $k$.

#### Inductive Step

: We prove the result holds for contracts built over $C$ and $C^{\prime}$:

  * •

In all cases except, $\rho$ is not modified but its value depends on the
evaluation of sub-contracts. This allows us to dispatch all the proof
obligations to the inductive hypothesis.

##  4 Analysis

In this section, we define an automata-theoretic approach to analyzing
$c\mathcal{DL}$ contracts, through a construction to a safety automaton. We
use this for model checking and blame analysis, but leave the application for
quantitative analysis for future work.

###  4.1 Contracts to Automata

We give a construction from $c\mathcal{DL}$ contracts to automata that
recognize interactions that are informative for satisfaction or violation. For
brevity, we keep the definition of the automata symbolic, with transitions
tagged by propositions over party actions, representing a set of concrete
transitions. The automaton is over the alphabet $\Sigma_{0,1}$ since it
requires information about the parties.

######  Definition 4.

The deterministic _automaton of contract_ $C$ is:

$aut(C)\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\langle\Sigma_{0,1},S,s_{0},\\{s_{B}\\},\rightarrow\rangle\text{.}$

We define $\rightarrow$ through the below function
$\tau(C,s_{0},s_{G},s_{B},\\{\\})$ that computes a set of transitions, given a
contract, an initial state ($s_{0}$), a state denoting satisfaction ($s_{G}$),
a state denoting violation ($s_{B}$), and a partial function $V$ from
recursion variables ($\mathbb{X}$) to states, characterised by (with $s$ as a
fresh state):

$\displaystyle\tau(\top,s_{0},s_{G},s_{B},V)$
$\displaystyle\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\\{s_{0}\xrightarrow{true}s_{G}\\}$
$\displaystyle\tau(\perp,s_{0},s_{G},s_{B},V)$
$\displaystyle\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\\{s_{0}\xrightarrow{true}s_{B}\\}$
$\displaystyle\tau(O_{p}(a),s_{0},s_{G},s_{B},V)$
$\displaystyle\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\\{s_{0}\xrightarrow{a_{p}\wedge
a_{1-p}}s_{G},s_{0}\xrightarrow{\neg(a_{p}\wedge a_{1-p})}s_{B}\\}$
$\displaystyle\tau(F_{p}(a),s_{0},s_{G},s_{B},V)$
$\displaystyle\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\\{s_{0}\xrightarrow{\neg(a_{p}\wedge
a_{1-p})}s_{G},s_{0}\xrightarrow{a_{p}\wedge a_{1-p}}s_{B}\\}$
$\displaystyle\tau(P_{p}(a),s_{0},s_{G},s_{B},V)$
$\displaystyle\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\\{s_{0}\xrightarrow{a_{p}\implies
a_{1-p}}s_{G},s_{0}\xrightarrow{\neg(a_{p}\implies a_{1-p})}s_{B}\\}$
$\displaystyle\tau(\langle re\rangle C,s_{0},s_{G},s_{B},V)$
$\displaystyle\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}A(re,s_{0},s,s_{G})\cup\tau(C,s,s_{G},s_{B},V)$
$\displaystyle\tau(re\rotatebox[origin={c}]{-90.0}{$\bumpeq$}C,s_{0},s_{G},s_{B},V)$
$\displaystyle\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}(A(re,s_{0},s_{G},s_{G})\|\tau(C,s_{0},s_{G},s_{B},V))$
$\displaystyle\quad\ [(s_{G},*)/s_{G}][(*,s_{B})/s_{B}][(*,s_{G})/s_{G}]$
$\displaystyle\tau(C\wedge C^{\prime},s_{0},s_{G},s_{B},V)$
$\displaystyle\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}(\tau(C,s_{0},s_{G},s_{B},V)\|^{r}\tau(C^{\prime},s_{0},s_{G},s_{B},V))$
$\displaystyle\quad\ [(s_{G},s_{G})/s_{G}][(s_{B},*)/s_{B}][(*,s_{B})/s_{B}]$
$\displaystyle\tau(C;C^{\prime},s_{0},s_{G},s_{B},V)$
$\displaystyle\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\tau(C,s_{0},s,s_{B},V)\cup\tau(C^{\prime},s,s_{G},s_{B},V)$
$\displaystyle\tau(C\blacktriangleright C^{\prime},s_{0},s_{G},s_{B},V)$
$\displaystyle\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\tau(C,s_{0},s_{G},s,V)\cup\tau(C^{\prime},s,s_{G},s_{B},V)$
$\displaystyle\tau(X,s_{0},s_{G},s_{B},V)$
$\displaystyle\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\\{s_{G}\xrightarrow{\epsilon}V(X)\\}$
$\displaystyle\tau(recX.C,s_{0},s_{G},s_{B},V)$
$\displaystyle\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\tau(C,s_{0},s_{G},s_{B},V[X\mapsto s_{0}])$

We define $\rightarrow^{\prime}$ as $\tau(C,s_{0},s_{G},s_{B},\\{\\})$ without
all transitions outgoing from $s_{G}$ and $S_{B}$, and define
$\rightarrow\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\rightarrow^{\prime}\cup\\{s_{B}\xrightarrow{\textit{true}}s_{B}\\}\cup\\{s_{G}\xrightarrow{true}s_{G}\\}$,
where $S$ is the set of states used in $\rightarrow$. We assume the
$\epsilon$-transitions are removed using standard methods.

We give some intuition for the construction. The transitions for the atomic
contracts follow quite clearly from their semantics. For the trigger
contracts, we use a fresh state $s$ to connect the automaton for the regular
expression, with that of the contract, ensuring the latter is only entered
when the former tightly matches. For the guard contract, we instead
synchronously compose ($\|$) both automata (i.e., intersect their languages),
getting a set of transitions. Here we also relabel tuples of states to single
states. Recall we use $(*,s)$ to match any pair, where the second term is $s$,
and similarly for $(s,*)$. Through the sequence of re-labellings, we ensure:
first that reaching $s_{G}$ in the acceptance of the first means; (2) reaching
$s_{B}$ in the second means violation; and (3) if the previous two situations
are not the case, reaching $s_{G}$ in the second means acceptance.

For conjunction, instead of using the synchronous product, we use the relaxed
variant ($\|^{r}$), since the contracts may require traces of different
lengths for satisfaction. This relaxed product allows the ‘longer’ contract to
continue after the status of the other is determined. For sequence, we use the
fresh state $s$ to move between the automata, once the first contract has been
satisfied. For reparation this is similar, except we move between the
contracts at the moment the first is violated. For recursion, we simply loop
back to the initial state of the recursed contract with an
$\epsilon$-transition once the corresponding recursion variable is
encountered.

Note how analyzing states without viable transitions, after applying $\tau$,
can be used for conflict analysis of $c\mathcal{DL}$ contracts. For example,
when there is a conflict, e.g., $O_{p}(a)\wedge F_{p}(a)$, there will be a
state with all outgoing transitions to $s_{B}$.

[Correctness] An infinite interaction is a model of $C$, iff it never reaches
a rejecting state in $aut(C)$:
$\forall\vec{w}_{0}^{\infty}\cdot\vec{w}_{0}^{\infty}\models C\iff
w_{0}\sqcup^{0}_{1}w_{1}\in L(aut(C))$.

For the atomic contracts, the correspondence should be clear. By structural
induction on the rest: triggering, sequence, and reparation should also be
clear from the definition. For conjunction, the relaxed synchronous product
makes sure the contract not yet satisfied continues being executed, as
required, while the replacements ensure large nestings of conjunctions do not
lead to large tuples of accepting or rejecting states. For  $\bumpeq$ , using
the synchronous product ensures the path ends when either is
satisfied/violated, as required.

First, some observations. Looking at the left-hand side,
$w_{0}\sqcup^{0}_{1}w_{1}\in L(aut(C))$ means that no finite prefix of
$w_{0}\sqcup^{0}_{1}w_{1}$ reaches a rejecting state.

Looking at the right-hand side, $\vec{w}_{0}^{\infty}\models C$ means that
there is no finite prefix of $\vec{w}_{0}^{\infty}$ that informatively
violates: $\nexists k\in\mathbb{N}\cdot\vec{w}_{0}^{k}\vDash_{\perp}C$. Note
how $\vec{w}_{0}^{k}$ has a direct correspondence to
$(w_{0}\sqcup^{0}_{1}w_{1})[0...k]$ (recall $\vec{w}_{0}^{k}$ is
$(w_{0}[0...k],w_{1}[0...k])$, and
$(w_{0}\sqcup^{0}_{1}w_{1})[0...k]=w_{0}[0...k]\sqcup^{0}_{1}w_{1}[0...k]$).
We use this direct correspondence implicitly throughout.

We now start the proof, relying on structural induction on $C$.

#### Base Case

  1. 1.

The result should be clear for $\top$ and $\perp$.

  2. 2.

$O_{p}(a)$:

    1. (a)

LHS: $\vec{w}_{0}^{\infty}\models
O_{p}(a)\xLeftrightarrow{\text{def~{}\ref{def:infinitesat}}}\nexists
k.\vec{w}_{0}^{k}\models_{v}O_{p}(a)\xLeftrightarrow{\text{fig.\ref{fig:informative}}}\nexists
k\cdot 0=k\text{ and }a\notin w_{p}[0]\text{ or }a\notin w_{1-p}[0]$;

    2. (b)

RHS: In $aut(O_{p}(a))$, the only way to reach a rejecting state is to take
the transition $s_{0}\xrightarrow{\neg(a_{p}\wedge a_{1-p})}s_{B}$. Taking
this transition implies $\neg(a_{p}\in w_{p}[0]\wedge a_{1-p}\in w_{1-p}[0])$,
which contradicts the LHS.

  3. 3.

$F(a)$:

    1. (a)

LHS: $\vec{w}_{0}^{\infty}\models
F_{p}(a)\xLeftrightarrow{\text{def~{}\ref{def:infinitesat}}}\nexists
k.\vec{w}_{0}^{k}\models_{v}F_{p}(a)\xLeftrightarrow{\text{}}\nexists k\cdot
0=k\text{ and }a\in w_{p}[0]\text{ or }a\in w_{1-p}[0]$;

    2. (b)

RHS: In $aut(F_{p}(a))$, the only way to reach a rejecting state is to take
the transition $s_{0}\xrightarrow{a_{p}\wedge a_{1-p}}s_{B}$. Taking this
transition implies $a_{p}\in w_{p}[0]\wedge a_{1-p}\in w_{1-p}[0]$ which
contradicts the LHS.

  4. 4.

$P_{p}(a)$:

    1. (a)

LHS: $\vec{w}_{0}^{\infty}\models
P_{p}(a)\xLeftrightarrow{\text{def~{}\ref{def:infinitesat}}}\nexists
k.\vec{w}_{0}^{k}\models_{v}P(a)\xLeftrightarrow{\text{\ref{fig:informative}}}\nexists
k\cdot 0=k\text{ and }a\in w_{p}[0]\text{ and }a\notin w_{p}[0]$;

    2. (b)

RHS: In $aut(P_{p}(a)))$ the only way to reach the rejecting state is to take
the transition $s_{0}\xrightarrow{\neg(a_{p}\implies a_{1-p})}s_{B}$. Taking
this transition implies $\neg(a_{p}\in w_{p}[0]\implies a_{1-p}\in
w_{1-p}[0])$ which contradicts the LHS.

#### Inductive Hypothesis

We assume the theorem for contracts $C$ and $C^{\prime}$.

#### Inductive Step

We prove it now for contracts built over $C$ and $C^{\prime}$:

We present the proofs from left-to-right, they also apply from right-to-left,
unless explicitly stated.

  * •

$\langle re\rangle C$ –

    1. 1.

Starting from the LHS, all finite prefixes are of two types:

      1. (a)

The prefix is not in the tight language of $re$, ensuring that no finite
prefix of it reaches $s$ in $A(re,s_{0},s,s_{G})$, thus the automaton of $C$
is never entered, and $s_{B}$ is unreachable.

      2. (b)

The prefix tightly matches $re$, say $\vec{w}_{0}^{k}$, and its corresponding
finite suffix violates $C$, say $\vec{w}_{k+1}^{j}$. We can apply the IH on
$\vec{w}_{k+1}^{\infty}\vdash C$, concluding that the automaton of $C$ accepts
$\vec{w}_{k+1}^{\infty}$. Moreover, by $A(re,s_{0},s,s_{G})$,
$\vec{w}_{0}^{k}$ reaches $s$, the initial state of the automaton for $C$,
ensuring $\vec{w}_{0}^{j}$ reaches $s_{G}$, a sink state, and never $s_{B}$,
such that then we can conclude the RHS.

  * •

$re\rotatebox[origin={c}]{-90.0}{$\bumpeq$}C$ –

    1. 1.

Starting from the LHS, all finite prefixes are of two types:

      1. (a)

The prefix $\vec{w}_{0}^{k}$ is not in the closure of the language. It, or a
prefix of it, thus reaches $s_{G}$ in $A(re,s_{0},s_{G},s_{G})$. On the RHS,
we compose this automaton with the automaton for $C$. Note $s_{G}$ has no
outgoing transitions in $A(re,s_{0},s_{G},s_{G})$, therefore states of the
form $(s_{G},*)$ have no outgoing transitions. Similarly for states of the
form $(*,s_{B})$. Given the relabelling, we ensure reaching $s_{G}$ in $re$’s
automaton means acceptance, giving us the result we need.

      2. (b)

There is a prefix in the closure of $re$ and this prefix does not violate $C$.
Any infinite extension is thus a model of $C$, including
$\vec{w}_{0}^{\infty}$, thus this interaction is a model of $C$. By the
inductive hypothesis, it is also in the language of $aut(C)$. Moreover, the
definition of the synchronous composition ensures this interaction is also
accepted by the composed automaton, giving us the result we need.

  * •

$C\wedge C^{\prime}$ —

    1. 1.

Starting from the LHS:

      1. (a)

There is no prefix that informatively violates $C$, and no prefix that
informatively violates $C^{\prime}$. By the inductive hypothesis then the
interaction must be in the automaton of each. For the conjunction, we computed
the relaxed synchronous product of the two automata that computes the union of
two languages. While relabelling ensures violating in one automaton means
violating in the composed one. This gives us the result needed.

  * •

$C;C^{\prime}$ –

    1. 1.

Starting from the LHS, every finite prefix does not informatively violate $C$
(0) and moreover can be of two types:

      1. (a)

It has no strict prefix that satisfies $C$. Applying the inductive hypothesis
(given (0)) ensures any infinite continuation of such a prefix remains in the
language of the automaton of $C$.

      2. (b)

It has a strict prefix that satisfies $C$ and the corresponding finite suffix
does not violate $C^{\prime}$. Applying the inductive hypothesis, we can
conclude that the latter prefix reaches $s$, and then the suffix continues
executing in the automaton of $C^{\prime}$, where it never reaches $s_{B}$
(given the inductive hypothesis on $C^{\prime}$).

  * •

$C\blacktriangleright C^{\prime}$ –

    1. 1.

Starting from the LHS, every finite prefix is of two types:

      1. (a)

The prefix does not informatively violate $C$. By applying the inductive
hypothesis directly the result follows.

      2. (b)

The prefix informatively violates $C$ and it has no corresponding finite
suffix that violates $C^{\prime}$. Applying the inductive hypothesis on both,
the prefix will reach the intermediate bad state ($s$) in $C$’s automaton, and
thus enter $C^{\prime}$’s automaton, where it never reaches the bad state
$s_{B}$, as required.

  * •

$recX.C$ –

    1. 1.

The correctness of this depends on the correctness of $C$, note how the
automaton loops back to the initial state once a recursion variable is
reached.

∎

######  Corollary 1.

An infinite interaction is not a model of $C$, if and only if it reaches a
rejecting state in $aut(C)$: $\forall(w_{0},w_{1})\not\models C\iff\exists
j\in\mathbb{N}\cdot
s_{0}\xRightarrow{(w_{0}\sqcup^{0}_{1}w_{1})[0...j]}s_{B}$.

Follows from Theorem. 4 and completeness (up to rejection) of $aut(C)$.
Complexity From the translation note that without regular expressions the
number of states and transitions is linear in the number of sub-clauses and
operators in the contract, but is exponential in the presence of regular
expressions.444For example, a contract $recX.\top;(O_{0}(a)\wedge P_{1}(b));X$
has size 8 (note normed actions are not counted).

###  4.2 Model Checking

We represent the behaviour of each party as a Moore machine ($M_{0}$, and
$M_{1}$). For party 0, the input alphabet is $\Sigma_{1}$ and the output
alphabet is $\Sigma_{0}$, and vice-versa for party 1. We characterise the
composed behaviour of two parties by defining the product of the two dual
Moore machines: $M_{0}\otimes M_{1}$, getting an automaton over
$\Sigma_{0}\cup\Sigma_{1}$.

We can then compose this automaton that represents the interactive behaviour
of the parties with the contract’s automaton, $(M_{0}\otimes M_{1})\|aut(C)$.
Then, if no rejecting state is reachable in this automaton, the composed
party’s behaviour respects the contract.

######  Theorem 4.1 (Model Checking Soundness and Completeness).

$\emptyset=RL((M_{0}\otimes M_{1})\|aut(C))$ iff
$\nexists\vec{w}_{0}^{\infty}:w_{0}\sqcup^{0}_{1}w_{1}\in L(M_{0}\otimes
M_{1})\wedge\vec{w}_{0}^{\infty}\models_{v}C$.

###### Proof.

Consider that $\|$ computes the intersection of the languages, while Theorem.
4 states that $L(aut(C))$ contains exactly the traces satisfying $C$ (modulo a
simple technical procedure to move between labelled traces and pairs of
traces). Then it follows easily that $RL((M_{0}\otimes M_{1})\|aut(C))$ is
empty only when there is no trace in $(M_{0}\otimes M_{1})$ that leads to a
rejecting state in $aut(C)$. The same logic can be taken in the other
direction. ∎

∎

###  4.3 Blame Assignment

For the blame assignment, we can modify the automaton construction by adding
two other violating states: $s^{0}_{B}$ and $s^{1}_{B}$, and adjust the
transitions for the basic norms accordingly.

######  Definition 5.

The deterministic _blame automaton of contract_ $C$ is:

$blAut(C)\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\langle\Sigma_{0,1},S,s_{0},\\{s_{B},s^{0}_{B},s^{1}_{B},(s^{0}_{B},s^{1}_{B})\\},\rightarrow\rangle\text{}$

We define $\rightarrow$ through the function
$\tau(C,s_{0},s_{G},s^{0}_{B},s^{1}_{B},V)$ that computes a set of
transitions, as in Definition 4 but now assigning blame by transitioning to
the appropriate state. We focus on a subset of the rules, given limited space,
where there are substantial changes555The missing rules essentially mirror the
previous construction with the added states, and the different domains.:

$\displaystyle\tau(O_{p}(a),s_{0},s_{G},s^{0}_{B},s^{1}_{B},V)$
$\displaystyle\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\\{s_{0}\xrightarrow{a_{p}\wedge
a_{1-p}}s_{G},s_{0}\xrightarrow{\neg
a_{p}}s^{p}_{B},s_{0}\xrightarrow{a_{p}\wedge\neg a_{1-p}}s^{1-p}_{B}\\}$
$\displaystyle\tau(F_{p}(a),s_{0},s_{G},s^{0}_{B},s^{1}_{B},V)$
$\displaystyle\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\\{s_{0}\xrightarrow{\neg(a_{p}\wedge
a_{1-p})}s_{G},s_{0}\xrightarrow{a_{p}\wedge a_{1-p}}s^{p}_{B}\\}$
$\displaystyle\tau(P_{p}(a),s_{0},s_{G},s^{0}_{B},s^{1}_{B},V)$
$\displaystyle\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\\{s_{0}\xrightarrow{a_{p}\implies
a_{1-p}}s_{G},s_{0}\xrightarrow{a_{p}\wedge\neg a_{1-p}}s^{1-p}_{B}\\}$
$\displaystyle\tau(C\blacktriangleright
C^{\prime},s_{0},s_{G},s^{0}_{B},s^{1}_{B},V)$
$\displaystyle\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\tau(C,s_{0},s_{G},s^{0},s^{1},V)$
$\displaystyle\quad\cup\tau(C^{\prime},s^{0},s_{G},s^{0}_{B},V)\cup\tau(C^{\prime},s^{1},s_{G},s^{1}_{B},V)$

Given $\rightarrow^{\prime}=\tau(C,s_{0},s_{G},s_{B},\\{\\})$, $\rightarrow$
is defined as $\rightarrow^{\prime}$ with the following transformations, in
order: (1) any tuple of states containing both $s^{0}_{B}$ and $s^{1}_{B}$ is
relabelled as $(s^{0}_{B},s^{1}_{B})$; (2) any tuple of states containing
$s^{0}_{B}$ ($s^{1}_{B}$) is relabelled as $s^{0}_{B}$ ($s^{1}_{B}$); (3) any
state for which all outgoing transitions go to a bad state are redirected to
$s_{B}$; (4) any tuple of states containing $s_{G}$ is relabelled as $s_{G}$;
and (5) all bad states and $s_{G}$ become sink states. $S$ is the set of
states used in $\rightarrow$. We assume the $\epsilon$-transitions are removed
using standard methods.

Note how this automata simply refines the bad states of the original automata
construction, by assigning blame for the violation of norms through a
transition to an appropriate new state. While the post-processing (see (3)),
allows violations caused by conflicts to go instead to state $s_{B}$, where no
party is blamed.

Then we prove correspondence with the blame semantics: [Blame Analysis
Soundness and Completeness] Where $RL_{p}$, for $p\in\\{0,1\\}$, is the
rejecting language of the automaton through states that pass through
$s^{p}_{B}$ or the tuple state $(s^{0}_{B},s^{1}_{B})$:

$\emptyset=RL_{p}((M_{0}\otimes M_{1})\|blAut(C))$ iff $\nexists
w_{0},w_{1}\in(2^{\Sigma})^{*}:w_{0}\sqcup^{0}_{1}w_{1}\in L(M_{0}\otimes
M_{1})\wedge(w_{0},w_{1})\models_{v}^{p}C$.

###### Proof.

This follows from a slight modification of Corollary. 1 (since here we are
just refining the bad states of $aut(C)$) with the replacement of $s_{B}$ by
party-tagged states when someone can be blamed, and from a similar argument to
Theorem. 4.1. ∎

This automaton can be used for model checking as before, but it can also
answer queries about who is to blame.

######  Example 5.

We illustrate in Figure 4(c) an example of two Moore machines representing the
behaviour of two parties (Figures 4(a) and 4(b)). Note these are
deterministic, therefore their composition (Figure 4(c)) is just a trace. Note
the same theory applies even when the Moore machines are non-deterministic. In
Figures 4(d) and 4(e) we show the automaton and blame automaton for the
contract $recX.(O_{1}(c)\blacktriangleright O_{0}(b);X)$. Our model checking
procedure (without blame) will compose Figure 4(c) and Figure 4(d), and
identify that the trace reaches the bad state. Consider that the reparation
consisting of an obligation to perform an action $b$ was not satisfied.
Similarly (not shown here) blame automaton would blame party 1 for the
violation.

$s_{0}/\mathrm{a_{0}}$start$s_{1}/\mathrm{b_{0}}$$a_{1}$$\lnot a_{1}$$\lnot
b_{1}$$b_{1}$

(a) $M_{0}$: Moore machine for agent 0.

$s_{0}/\mathrm{c_{1}}$start$s_{1}/\mathrm{b_{1}}$$b_{0}$$\lnot
b_{0}$$\lnot{a_{0}}$$a_{0}$

(b) $M_{1}$: Moore machine for agent 1.

$s_{0},s_{0}$start$s_{1},s_{1}$$s_{0},s_{1}$$s_{1},s_{0}$$\\{a_{0},c_{1}\\}$$\\{b_{0},b_{1}\\}$$\\{a_{0},b_{1}\\}$$\\{b_{0},c_{1}\\}$

(c) The composition $M_{0}\otimes M_{1}$.

$s_{0}$start$s_{G}$$s_{2}$$s_{B}$$a_{0}\wedge a_{1}$$\lnot(a_{0},\wedge
a_{1})$$\begin{array}[]{l}\\\ b_{0}\wedge b_{1}\end{array}$$\lnot(b_{0}\wedge
b_{1})$$\epsilon$

(d) $C=aut(recX.(O_{1}(a)\blacktriangleright O_{0}(b));X)$

$s_{0}$start$s_{G}$$s_{2}$$s_{B}^{0}$$s_{B}^{1}$$a_{0}\wedge
a_{1}$$\lnot(a_{0}\wedge a_{1})$$\qquad b_{0}\wedge b_{1}$$\qquad\ \lnot
b_{0}$$\qquad b_{0}\wedge\lnot b_{1}$$\epsilon$

(e) $blAut(recX.(O_{1}(a)\blacktriangleright O_{0}(b));X)$

$s_{2}$start$s_{G}$$s_{0}$$s_{2}$$s_{B}$

(f) $(M_{0}\otimes M_{1})\|C$

Figure 4: Example of the model checking approach.

##  5 Related Work

Multi-agent systems. A number of logics can express properties about multi-
agent systems. For example, ATL can express the existence of a strategy for
one or more agents to enforce a certain specification [alur2002alternating],
while strategy logic makes strategies first-class objects
[10.1007/978-3-540-74407-8_5]. Checking for the existence of strategies is in
2EXPTIME. Our logic is not concerned with the existence of strategies, but
with analyzing the party strategies to ensure they respect a contract. So, our
approach is more comparable to LTL than to game-based logic, limited to
(co-)safety properties and with a notion of norms that allows us to talk about
blame natively.

Concerning blame, [Friedenberg_Halpern_2019] considers the notion of
blameworthiness. They use structural equations to represent agents, but the
approach is not temporal, and each agent performs only one action. Work in
this area (e.g., [Friedenberg_Halpern_2019, 10.5555/3504035.3504261,
ChocklerH03]) tends to be in a different setting than ours.

They consider the cost of actions and agents’ beliefs about the probability of
their actions not achieving the expected outcome. Instead, we assume all the
parties have knowledge of the contract, and we take an automata-theoretic
approach. Moreover, our blame derives from the norms, whereas other work
depends on a notion of causality [DBLP:journals/corr/Chockler16].

The work [DBLP:conf/atal/AbarcaB22] extends STIT logic with notions of
responsibility, allowing reasoning about blameworthiness and praiseworthiness.
This, and other similar work (e.g., [10.1093/logcom/ext072]) is more related
to our work and even has a richer notion of blame. However, we give an
automata-based model checking procedure.

Deontic logics Deontic logics have been used in a multi-agent setting before.
For example, [10.1007/11786849_7] define deontic notions in terms of ATL,
allowing reasoning like an obligation holds for an agent iff they have a
strategy to carry it out. These approaches (e.g., [10.1007/11786849_7,
10.1145/860575.860609, DBLP:conf/hybrid/Shea-BlymyerA20]) focus on obligations
and neglect both reparations and our view of permissions as rights. Some
approaches (e.g., [10.1145/860575.860609, 10.1007/978-3-540-25927-5_15])
however do perform model checking for a deontic logic in a multi-agent system
setting. The work most similar to ours is that of contract automata
[10.1007/s10506-016-9185-2], wherein a contract is represented as a Kripke
structure (with states tagged by norms), two parties as automata, and
permissions with a similar rights-based view. However, it takes a purely
operational approach, and lacks a notion of blame.

Our language is an extension and combination of the deontic languages
presented in [DBLP:conf/jurix/AzzopardiGP16, DBLP:conf/jurix/AzzopardiPS18,
DBLP:conf/wollic/PrisacariuS09], combining action attempts, a right-based view
of permission, a two-party setting, and regular expressions as conditions.

Besides maintaining all these, we give denotational trace semantics, and
provide blame and model checking algorithms.

##  6 Conclusions

In this paper we have introduced a deontic logic for reasoning about a two-
party synchronous setting. This logic allows one to define constraints on when
parties should support or non-interfere with the carrying out of a certain
action or protocol. Using a pair of party traces, we can talk about attempts
and success to perform collaborative actions. We consider automata
constructions describing both the set of all satisfying and violating
sequences. Given the behavior of the agents in the form of suitable automata,
we have also provided algorithms for model checking and for blame assignment.
To differentiate between satisfying a formula in the expected manner or by
fullfilling the exceptional case, we introduce a quantitative semantics. This
allows ordering satisfying traces depending on how often they use these
exceptions.

This work may be extended in many directions. First, we could consider
asynchronous interaction, distinguishing between sending and receiving. The
syntax and semantics can also be extended easily to handle multi-party agents
rather than just a two-party setting. Different quantitative semantics could
be given, for example considering the _costs of actions_ to reason when it is
better to pay a fine rather than to behave as expected. We plan to study how
to synthesise strategies for the different parties, for instance to ensure the
optimal behaviour of agents.

## References

  * [1] Abarca, A.I.R., Broersen, J.M.: A stit logic of responsibility. In: Faliszewski, P., Mascardi, V., Pelachaud, C., Taylor, M.E. (eds.) 21st International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2022, Auckland, New Zealand, May 9-13, 2022. pp. 1717–1719. International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS) (2022). https://doi.org/10.5555/3535850.3536087, https://www.ifaamas.org/Proceedings/aamas2022/pdfs/p1717.pdf
  * [2] Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM (JACM) 49(5), 672–713 (2002)
  * [3] Azzopardi, S., Gatt, A., Pace, G.J.: Reasoning about partial contracts. In: JURIX’16. Frontiers in Artificial Intelligence and Applications, vol. 294, pp. 23–32. IOS Press (2016). https://doi.org/10.3233/978-1-61499-726-9-23
  * [4] Azzopardi, S., Pace, G.J., Schapachnik, F.: On observing contracts: Deontic contracts meet smart contracts. In: JURIX’18. Frontiers in Artificial Intelligence and Applications, vol. 313, pp. 21–30. IOS Press (2018). https://doi.org/10.3233/978-1-61499-935-5-21
  * [5] Azzopardi, S., Pace, G.J., Schapachnik, F., Schneider, G.: Contract automata. Artif. Intell. Law 24(3), 203–243 (sep 2016). https://doi.org/10.1007/s10506-016-9185-2, https://doi.org/10.1007/s10506-016-9185-2
  * [6] Broersen, J.: Strategic deontic temporal logic as a reduction to atl, with an application to chisholm’s scenario. In: DEON’06. p. 53–68. Springer (2006). https://doi.org/10.1007/11786849_7
  * [7] Chatterjee, K., Henzinger, T.A., Piterman, N.: Strategy logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007 – Concurrency Theory. pp. 59–73. Springer Berlin Heidelberg, Berlin, Heidelberg (2007)
  * [8] Chockler, H.: Causality and responsibility for formal verification and beyond. In: CREST@ETAPS’16. EPTCS, vol. 224, pp. 1–8 (2016). https://doi.org/10.4204/EPTCS.224.1
  * [9] Chockler, H., Halpern, J.Y.: Responsibility and blame: A structural-model approach. In: Gottlob, G., Walsh, T. (eds.) IJCAI-03, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, Acapulco, Mexico, August 9-15, 2003. pp. 147–153. Morgan Kaufmann (2003), http://ijcai.org/Proceedings/03/Papers/021.pdf
  * [10] Chockler, H., Halpern, J.Y.: Responsibility and blame: A structural-model approach. Journal of Artificial Intelligence Research 22, 93–115 (2004)
  * [11] Friedenberg, M., Halpern, J.Y.: Blameworthiness in multi-agent settings. Proceedings of the AAAI Conference on Artificial Intelligence 33(01), 525–532 (2019). https://doi.org/10.1609/aaai.v33i01.3301525
  * [12] Halpern, J.Y.: Cause, responsibility and blame: a structural-model approach. Law, probability and risk 14(2), 91–118 (2015)
  * [13] Halpern, J.Y., Kleiman-Weiner, M.: Towards formal definitions of blameworthiness, intention, and moral responsibility. In: AAAI/IAAI/EAAI’18. AAAI Press (2018)
  * [14] Jackson, F.: On the semantics and logic of obligation. Mind 94(374), 177–195 (1985)
  * [15] Lorini, E., Longin, D., Mayor, E.: A logical analysis of responsibility attribution: emotions, individuals and collectives. Journal of Logic and Computation 24(6), 1313–1339 (12 2013). https://doi.org/10.1093/logcom/ext072, https://doi.org/10.1093/logcom/ext072
  * [16] McNamara, P.: Deontic logic. In: Gabbay, D.M., Woods, J. (eds.) Logic and the Modalities in the Twentieth Century, Handbook of the History of Logic, vol. 7, pp. 197–288. Elsevier (2006). https://doi.org/10.1016/S1874-5857(06)80029-4, https://doi.org/10.1016/S1874-5857(06)80029-4
  * [17] Penczek, W., Lomuscio, A.: Verifying epistemic properties of multi-agent systems via bounded model checking. In: Proceedings of the Second International Joint Conference on Autonomous Agents and Multiagent Systems. p. 209–216. AAMAS ’03, Association for Computing Machinery, New York, NY, USA (2003). https://doi.org/10.1145/860575.860609, https://doi.org/10.1145/860575.860609
  * [18] Prisacariu, C., Schneider, G.: Cl: An action-based logic for reasoning about contracts. In: WoLLIC’09. LNCS, vol. 5514, pp. 335–349. Springer (2009). https://doi.org/10.1007/978-3-642-02261-6_27
  * [19] Raimondi, F., Lomuscio, A.: Automatic verification of deontic properties of multi-agent systems. In: Lomuscio, A., Nute, D. (eds.) Deontic Logic in Computer Science. pp. 228–242. Springer Berlin Heidelberg, Berlin, Heidelberg (2004)
  * [20] Shea-Blymyer, C., Abbas, H.: A deontic logic analysis of autonomous systems’ safety. In: HSCC’20. pp. 26:1–26:11. ACM (2020). https://doi.org/10.1145/3365365.3382203, https://doi.org/10.1145/3365365.3382203
  * [21] Von Wright, G.H.: Deontic logic. Mind 60(237), 1–15 (1951)