[1]organization=Université de Lorraine, CNRS, LORIA, city=Nancy,
country=France [2]organization=University College London, city=London,
country=United Kingdom [3]organization=University College London & Institute
of Philosophy, city=London, country=United Kingdom

# Minimalistic System Modelling: Behaviours,
Interfaces, and Local Reasoning

Didier Galmiche<EMAIL_ADDRESS>Timo Lang<EMAIL_ADDRESS>David
Pym<EMAIL_ADDRESS>
###### Abstract

The infrastructure upon which the functioning of society depends is composed
of complex ecosystems of systems. Consequently, we must reason about the
properties of such ecosystems, which requires that we construct models of
them. There are very many approaches to systems modelling, typically building
on complex structural and dynamic frameworks. Our purpose here is to explore a
modelling framework based on minimal assumptions, starting from a primitive
notion of behaviour, and to show that such an approach allows the recovery of
the key ideas, including a generalized CAP theorem, required for effective
modelling of and reasoning about ecosystems of systems. We establish a logic
of behaviours and use it to express local reasoning principles for the
compositional structure of systems.

##  1 Introduction

The aim of this paper is to propose and study an extremely simple but general
framework for modelling _distributed systems_ , seen as a metaphor for
ecosystems of systems.

There is a good deal of work on systems modelling in the literature, much of
it — such as [22] and [9, 8, 1], for example — deriving from process algebra.
Some of this work, such as [8, 7], considers composition of models via notions
of interface. Other work, such as [17], derives from the world of management
science and organizational theory. Other approaches are based more immediately
on notions of composition and interface and their dynamics. For example,
interface automata [12, 13], relational interfaces [34], and bigraphs, [27,
28]. Our approach differs from all of these (and others) in its desire to
employ minimal assumptions about structure and dynamics, beginning with a very
primitive notion of behaviour.

There are very many — far too numerous to discuss here — informal definitions
of systems discussed across many disciplines. However, we can identify a
common core of these definitions that will serve as a starting point for our
work:

> A system is something whose behaviour is reflected in the behaviour of its
> components.

This definition is deceptively simple: it identifies, at least implicitly, not
only _behaviour_ and _components_ , but also _composition_ (necessarily, of
components) and so (again, necessarily) _interfaces_ between components.

In our framework, then, the notion of a ‘behaviour’ will be a primitive. The
standard model of a behaviour is a trace (finite or infinite), but we do not
have to subscribe to this interpretation. Indeed, our primitive notion of
behaviour requires not even a commitment to that degree of structure, although
traces will be an important example. The architectural aspect of a system,
namely the subsystems or components of which it consists, will be considered a
priori knowledge.

We will see that from this simple starting point — that is, a primitive notion
of behaviour — a rather expressive theory emerges. In Section 2, we introduce
the main notions of our modelling approach. Essentially, we define what we
consider to be a ‘system’, and this will built on a primitive notion of
_behaviour_. After defining the crucial notion of an _implementation_ between
systems, we then derive further well-known concepts from system modelling; in
particular, _interfaces_ and _composition_.

A thorough epistemological investigation of our choices of primitives is
beyond the scope of this paper. However, we believe it is evident that we have
identified a credible minimalistic position.

In Section 3, by way of demonstrating the relevance of our approach, we use
our framework to establish an abstract statement of the famous CAP theorem [5,
21]. Brewer’s original conjecture [4] is expressed rather generally. It
concerns three key properties of distributed systems. We suppose a system with
multiple, connected components that is intended to deliver a specified
service. Informally:

  * -

_(C)onsistency_ : all the system’s clients see the same data at the same time,
irrespective of the component of the system to which they connect;

  * -

_(A)vailability_ : every request for the service that is sent to the system
receives a response that is not the ‘error’ response;

  * -

_(P)artition-tolerance_ : the system continues to deliver the service even if
there are failures of the connections between its components.

Brewer stated that these three guarantees cannot be satisfied simultaneously
in a distributed system. Gilbert and Lynch gave a formal formulation and proof
[20] in a set up that is quite concrete. Specifically, they give a formal
statement of Brewer’s conjecture for an account of the CAP properties in ‘web
services’. In our framework, we are able to establish the CAP theorem in a
conceptually quite general way. However, we show, in A, that Gilbert and
Lynch’s formulation can be recovered from ours.

In Section 4, we introduce a primitive logic of behaviours in which formulae
are satisfied relative to ‘behaviours as worlds’. We consider the basic
classical propositional connectives and modal operators, so obtaining a
syntactic variant of S5. We establish the equivalence of behavioural
equivalence and logical equivalence (see, for example, [35, 33, 3]). We
discuss local reasoning principles (in the sense, for example, of [29]) for
the composition of systems. Finally, in Section 5, we discuss a range of
directions for future research, including _time_ (Section 5.1) and _tableaux
proof systems_ for the logic (Section 5.2).

##  2 The basic theory

Any formal model of a distributed system must capture the following two key
points:

  * -

The topology of the system: How do the components of the system sit together?

  * -

The dynamics of the system: How does the system as a whole and its components
behave?

Of these two, modelling the topology is unproblematic: We can usually take
some graph-like structure, where edges denote potential communication channels
between the parts of a system.

Modelling the dynamics of a system is a more subtle issue. It is usually not
feasible to give a full realistic description of a system’s behaviour;
therefore one works with abstractions. The choice of abstraction is then
dependent on the intended application. Some common formalizations of behaviour
include _state sets_ , (finite or infinite) _traces_ and possibly stochastic
extensions thereof.

We seek to find a common abstraction of these formalizations. To this end it
is useful to contemplate the relation between the topological and the
dynamical aspect of a distributed system. We can always observe the following
_reflection principle_ :

> The global behaviour of a system is reflected at the local behaviour of its
> components.

This principle connects the topological and dynamical aspects of a system by
expressing a functional relationship between global and local behaviours,
manifesting in various ways. For example, the global behaviour of an
input/output system might be modelled by the trace $\langle
read(x),write(y),write(y^{\prime}),read(x^{\prime})\rangle$ of interactions;
at the component responsible for reading the inputs, this global behaviour
will be reflected as $\langle read(x),read(x^{\prime})\rangle$. Cyberphysical
systems might have complex behaviours, including a measuring of temperature,
and one simple component that only records whether the system is overheated;
then the global behaviour of the system is reflected by one of the behaviours
$overheat=0$ or $overheat=1$.

The above reflection principle forms the core of our modelling approach. It
then turns out that we can leave the question what behaviours ‘really are’
largely open. What matters is only the relation between global and local
behaviours, as mediated by the reflection function.

###  2.1 Systems and Implementations

We assume a given collection $\mathbb{C}$ of _basic components_ that will form
the building blocks of our distributed systems. Each $c\in\mathbb{C}$ comes
equipped with a set $\mathrm{Beh}(c)$, whose elements we call _behaviours_.
For nonempty $C\subseteq\mathbb{C}$ we call $\mathrm{Beh}(C):=\Pi_{c\in
C}\mathrm{Beh}(c)$ a _set of $C$-snapshots_.

######  Definition 1 (system).

  * -

A _system_ is a function whose codomain is a set of snapshots.

  * -

If $f:B\to\mathrm{Beh}(C)$ is a system, we call the elements of
$\mathrm{Beh}(f):=B$ and $\mathrm{Comp}(f):=C$ the _behaviours of $f$_ and the
_components of $f$_ respectively.

We think of a system as a set $B$ of high-level descriptions of system
behaviours together with a translation $f$ into concrete component behaviours.
In this way the definition of a system proposed here is not a fully semantic
definition: We do allow, e.g., that $f(b_{1})=f(b_{2})$ for _different_
$b_{1},b_{2}\in B$. Such behaviours then differ only by their high-level
description, not by any observable factors component behaviour. The
motiviation for allowing syntactic elements is that it facilitates the
modelling of a system.

On the other hand, a fully semantic view of systems could be obtained by
requiring $f$ to be injective. In this case, a system can be identified with a
(labelled) subset of $\mathrm{Beh}(C)$.

######  Example 2.

Consider two components $c,d\in\mathbb{C}$ with $\mathrm{Beh}(c)=\\{x\\}^{*}$
and $\mathrm{Beh}(d)=\\{y,z\\}^{*}$. Then every $S\subseteq\\{x,y,z\\}^{*}$
can be seen as the behaviours of a system $f$ with
$\mathrm{Comp}(f)=\\{c,d\\}$ where $f$ projects on substrings, e.g.
$f(xxyxzzxy)=(xxxx,yzzy)$. Note that this $f$ is not injective, as we have
$f(xxyxzzxy)=f(xxxxyzzy)$.

Before coming to our second crucial definition, we introduce some notational
conventions. If $f:B\rightarrow\mathrm{Beh}(C)$ and $D\subseteq C$, we denote
$f_{D}:B\rightarrow\mathrm{Beh}(D)$ the composition of $f$ with the obvious
projection function $\mathrm{Beh}(C)\rightarrow\mathrm{Beh}(D)$. If $D$ is a
singleton $\\{d\\}$ we write $f_{d}$ instead of $f_{\\{d\\}}$. In Example 2 we
have $f_{d}(xxyxzzxy)=yzzy$. Second, it will be useful to view sets of
components as systems; for this, we identify $C\subseteq\mathbb{C}$ with the
identity function $\mathrm{Beh}(C)\rightarrow\mathrm{Beh}(C)$.

######  Definition 3 (implementation).

Let $f,g$ be systems with $\mathrm{Comp}(g)\subseteq\mathrm{Comp}(f)$. An
_implementation of $g$ in $f$_ is a function
$\sigma:\mathrm{Beh}(f)\rightarrow\mathrm{Beh}(g)$ such that
$f_{\mathrm{Comp}(g)}=g\circ\sigma$.

In other words, $\sigma:\mathrm{Beh}(f)\rightarrow\mathrm{Beh}(g)$ is an
implementation if the following diagram commutes:

${{\mathrm{Beh}(f)}}$${{\mathrm{Beh}(g)}}$${{\mathrm{Beh}(E)}}$$\scriptstyle{\sigma}$$\scriptstyle{g}$$\scriptstyle{f_{E}}$

$E:=\mathrm{Comp}(g)$

In this case we write $f\overset{\sigma}{\Longrightarrow}g$ and say that _$f$
implements $g$ (via $\sigma$)_, or that $g$ is a _subsystem_ of $f$. If $f$
implements $g$, then the local behaviour of $f$ at $c\in\mathrm{Comp}(g)$ can
always be explained in terms of the behaviour of $g$. We say that $\sigma$
_realizes $y\in\mathrm{Beh}(g)$_ if there is an $x\in\mathrm{Beh}(f)$ such
that $\sigma(x)=y$.

As a simple example of Definition 3, systems implement their components: For
$C\subseteq\mathrm{Comp}(f)$ we have $f\overset{f_{C}}{\Longrightarrow}C$
because $f_{C}=id_{C}\circ f_{C}$. Here we have used the identification of $C$
with the system $id_{C}$ as described above.

It should be stressed that $f\overset{\sigma}{\Longrightarrow}g$ does _not_
mean that $f$ is in control of $g$. While $\sigma$ denotes a relation between
the behaviours of $f$ and $g$, this relation is not necessarily causation. In
fact our model does not have an explicit notion of causation, say via input
and output polarities (inputs react, outputs act). On the other hand, such
notions can be derived from the setup, for example:

######  Definition 4.

If $f\overset{\sigma}{\Longrightarrow}g$ and $\sigma$ is _surjective_ , then
$\sigma$ is called an _input implementation_. $E\subseteq\mathrm{Comp}(f)$ is
an _input of $f$_ if $f_{E}$ is an input implementation.

The intuition is the following: If $\sigma$ is surjective, then every
behaviour of $g$ is realized by $\sigma$. Thus $g$ is not constrained as a
subsystem of $f$, and we can think of $f$ as merely ‘observing’ the behaviour
of $g$ and possibly reacting to it.

We close this section with a simple yet fundamental example, which illustrates
how a basic communication channel between two systems can be modelled in our
framework. A general treatment of the composition of systems follows in the
next section.

######  Example 5 (message passing).

Let $\Sigma$ be an alphabet, and let $c$ be a ‘communication component’ with
$\mathrm{Beh}(c)=\Sigma^{*}$; that is, behaviours are finite $\Sigma$-strings.
Now for some arbitrary set $G\neq\emptyset$ of additional behaviours, let $g$
be a system with $\mathrm{Beh}(g)\subseteq G\times\\{send(s)\mid
s\in\Sigma^{*}\\}$ that implements $c$ via $g_{c}(g,send(s))=s$. Furthermore
let $f$ be another system with $\mathrm{Beh}(f)\subseteq
F\times\\{receive(s)\mid s\in\Sigma^{*}\\}$ that implements $c$ via
$f_{c}(f,receive(s))=s$ and where $F\cap G=\emptyset$, and assume moreover
that $c$ is an input of $f$: for all $s\in\Sigma^{\ast}$, there exists $x\in
f$ such that $(x,receive(s))\in\mathrm{Beh}(f)$.

We now construct a system $h$ that allows message passing from $g$ to $f$. For
this let $\mathrm{Comp}(h)=\mathrm{Comp}(f)\cup\mathrm{Comp}(g)$ and let
$\mathrm{Beh}(h)$ contain those triples $(y,transmit(s),x)$ such that
$(y,send(s))\in\mathrm{Beh}(g)$ and $(x,reveice(s))\in\mathrm{Beh}(f)$. Then
$h$ implements both $f$ and $g$, and it stipulates that the messages that $g$
sends are those that $f$ receives.

We conclude this section by introduction a notion of _system equivalence_.

######  Definition 6.

$f$ and $g$ are equivalent, written $f\equiv g$, if
$f\overset{}{\Longrightarrow}g$ and $g\overset{}{\Longrightarrow}f$.

###  2.2 Compositions

######  Definition 7 (environment and composition).

An _environment for for $g_{1}$ and $g_{2}$_ is any system $f$ implementing
both $g_{1}$ and $g_{2}$. An environment $f$ is a _composition_ if
$\mathrm{Comp}(f)=\mathrm{Comp}(g_{1})\cup\mathrm{Comp}(g_{2})$.

We will often write
$g_{1}\overset{\sigma_{1}}{\Longleftarrow}f\overset{\sigma_{2}}{\Longrightarrow}g_{2}$
to denote a system $f$ implementing both $g_{1}$ and $g_{2}$.

######  Definition 8 (interface).

$\mathsf{Int}(g_{1},g_{2}):=\mathrm{Comp}(g_{1})\cap\mathrm{Comp}(g_{2})$ is
called the _interface_ of $g_{1}$ and $g_{2}$.

If
$g_{1}\overset{\sigma_{1}}{\Longleftarrow}f\overset{\sigma_{2}}{\Longrightarrow}g_{2}$
and $I:=\mathsf{Int}(g_{1},g_{2})$ we have the following commutative diagram,
assuming $I\neq\emptyset$:

${{\mathrm{Beh}(f)}}$${{\mathrm{Beh}(g_{1})}}$${{\mathrm{Beh}(g_{2})}}$${{\mathrm{Beh}(I)}}$$\scriptstyle{\sigma}$$\scriptstyle{\rho}$$\scriptstyle{(g_{1})_{I}}$$\scriptstyle{(g_{2})_{I}}$$\scriptstyle{f_{I}}$

Call $(y_{1},y_{2})\in\mathrm{Beh}(g_{1})\times\mathrm{Beh}(g_{2})$
_compatible_ if $I=\emptyset$ or $(g_{1})_{I}(y_{1})=(g_{2})_{I}(y_{2})$. One
is often interested in compositions which are ‘derived’ from the systems
$g_{1}$ and $g_{2}$; such compositions impose only those restrictions on its
subsystems that are necessary to compose them. This is captured in the next
definition.

######  Definition 9 (free composition).

A composition
$g_{1}\overset{\sigma_{1}}{\Longleftarrow}f\overset{\sigma_{2}}{\Longrightarrow}g_{2}$
is called _free_ if for every compatible pair
$(y_{1},y_{2})\in\mathrm{Beh}(g_{1})\times\mathrm{Beh}(g_{2})$ there exists
$x\in\mathrm{Beh}(f)$ such that $\sigma_{1}(x)=y_{1}$ and
$\sigma_{2}(x)=y_{2}$.

For example, the system $h$ from Example 5 is a free composition. Given two
systems $f,g$, there is a canonical free composition of $f$ and $g$ whose
behaviours are exactly the compatible pairs and which has projections as
implementation functions. We denote this composition by $f\otimes g$; it is
essentially the category-theoretic _pullback_ of the maps $(g_{1})_{I}$ and
$(g_{2})_{I}$.111Pullbacks as models of synchronization also appear in [2]

######  Definition 10 (canonical free composition).

Let $f,g$ be two systems, and let $I:=\mathsf{Int}(f,g)$. $f\otimes g$ is the
composition of $f$ and $g$ whose behaviour set is
$\\{(x,y)\in\mathrm{Beh}(f)\times\mathrm{Beh}(g)\mid I=\emptyset\lor
f_{I}(x)=g_{I}(y)\\}$ and whose function is given by

$(f\otimes g)_{c}(x,y)=\begin{cases}f_{c}(x)\quad\text{if
}c\in\mathrm{Comp}(f)\\\ g_{c}(y)\quad\text{if
}c\in\mathrm{Comp}(g)\setminus\mathrm{Comp}(f)\end{cases}$

Note that if $c\in\mathsf{Int}(f,g)$, then $(f\otimes
g)_{c}(x,y)=f_{c}(x)=g_{c}(y)$ by compatibility.

We say that $f$ is _runnable_ if $\mathrm{Beh}(f)\neq\emptyset$ (or
equivalently, $f\neq\emptyset$). The existence of at least one compatible pair
is the minimal requirement for runnable compositions:

######  Lemma 11.

If $\mathsf{Int}(f,g)\neq\emptyset$, a runnable composition of $f$ and $g$
exists iff there is a compatible pair.

###### Proof.

If some compatible pair exists, then $f\otimes g$ as described in Def. 10
above is runnable. Conversely, let
$f\overset{\sigma}{\Longleftarrow}h\overset{\rho}{\Longrightarrow}g$ be any
runnable composition of $f,g$ and pick $z\in\mathrm{Beh}(h)$. Let
$x=\sigma(z)$, $y=\rho(z)$, and $I=\mathsf{Int}(f,g)$. Then, by the properties
of implementations, we can show that $(x,y)$ is a compatible pair:
$f_{I}(x)=f_{I}(\sigma(z))=h_{I}(z)=g_{I}(\rho(z))=g_{I}(y)$. ∎

We can show that ‘directed’ compositions are always runnable:

######  Lemma 12.

Assume that $g$ is runnable. If $\mathsf{Int}(f,g)=\mathrm{Comp}(e)$ and the
system $e$ is an input of $f$ (see Def. 4), then there is a runnable
composition of $f$ and $g$.

###### Proof.

Let $f\overset{\rho}{\Longrightarrow}e$ be an input implementation and
$g\overset{\sigma}{\Longrightarrow}e$ any implementation. Since $g$ is
runnable, there exists $y\in\mathrm{Beh}(g)$, and as $e$ is an input component
we can find $x\in\mathrm{Beh}(f)$ such that $\rho(x)=\sigma(y)$. For
$I:=\mathrm{Comp}(e)$ we consequently have
$f_{I}(x)=e(\rho(x))=e(\sigma(y))=g_{I}(y)$ and so $(x,y)$ is a compatible
pair. Thus $f$ and $g$ are composable by Lemma 11. ∎

######  Example 13.

Let $f,g$ be systems with $\mathrm{Beh}(f)\subseteq\\{a,b,c\\}^{*}$ and
$\mathrm{Beh}(g)\subseteq\\{b,c,d\\}^{*}$, both closed under inital segments
(think traces of actions), and let $\mathsf{Int}(f,g)=\\{e\\}$ where
$\mathrm{Beh}(e)=\\{b,c\\}^{*}$. Assuming that $f$ and $g$ implement $e$ via
the obvious projections, $\mathrm{Beh}(f\otimes g)$ consists of pairs
$(s_{1},s_{2})\in\\{a,b,c\\}^{*}\times\\{b,c,d\\}^{*}$ whose restriction to
the common actions $\\{b,c\\}$ coincides. For example, if $x=\langle
a,b,b,c,a,b\rangle\in\mathrm{Beh}(f)$ and $y=\langle
b,d,b,c,d,b\rangle\in\mathrm{Beh}(g)$ then $(x,y)\in\mathrm{Beh}(f\otimes g)$,
as their restriction to $\\{b,c\\}$ coincides in the trace $\langle
b,b,c,b\rangle$. We can interpret this as a partially asynchronuous
computation:

${{f:}}$${a}$${b}$${b}$${c}$${a}$${b}$${{g:}}$${b}$${d}$${b}$${c}$${d}$${b}$

######  Example 14 (heaps).

Take as basic components a set $L$ of _locations_ , with
$\mathrm{Beh}(l)=\mathbb{N}$ for $l\in L$. For $L_{0}\subseteq^{fin}L$,
$S(L_{0})$ is the system whose behaviours are the $L_{0}$-based _heaplets_ ,
i.e. functions $h:L_{0}\rightarrow\mathbb{N}$. $S_{0}$ implements every $l\in
L_{0}$ via the function $h\mapsto h(l)$. An $L_{0}$-stream is the system whose
behaviours are sequences $\sigma$ of commands $l:=n$ where $l\in L_{0}$ and
$n\in\mathbb{N}$. It implements $S_{0}$ via the function that sends $\sigma$
to the the heaplet $h$ where $h(l)$ is the value $n$ of the last command
$l:=n$ in $\sigma$.

Let $L_{0}$ be the disjoint union of $L_{1}$ and $L_{2}$. Then every
$L_{0}$-stream is the free composition of an $L_{1}$-stream and an
$L_{2}$-stream.

In Example 13, nothing is said about the temporal relation between actions
outside the interface, and so we have a model of ‘true’ asynchronicity. On the
other hand, if
$f\overset{\sigma}{\Longleftarrow}h\overset{\rho}{\Longrightarrow}g$ is any
free composition, then one can show that $h$ factors through
$\mathrm{Beh}(f\otimes g)$ via a _surjective_ map:

${{\mathrm{Beh}(h)}}$${{\mathrm{Beh}(f\otimes
g)}}$${{\mathrm{Beh}(f)}}$${{\mathrm{Beh}(g)}}$${{\mathrm{Beh}(I)}}$$\scriptstyle{f_{I}}$$\scriptstyle{g_{I}}$$\scriptstyle{(f\otimes
g)_{I}}$$\scriptstyle{\sigma}$$\scriptstyle{\pi}$

Intuitively, this means that in any free composition $h$, $\mathrm{Beh}(h)$
extends $\mathrm{Beh}(f\otimes g)$ with some extra information. This can be
seen as the information about how a pair $(x,y)$ of compatible behaviours is
combined together: is it sequential, synchronous, or asynchronous?

######  Example 15.

Let $f$ and $g$ be as in Example 13. Let $h$ be a system whose behaviours are
all elements of $\\{a,b,c,d\\}^{*}$ whose restriction to actions in
$\\{a,b,c\\}$ and $\\{b,c,d\\}$ lies in $\mathrm{Beh}(f)$ and
$\mathrm{Beh}(g)$ respectively. $h$ is a free composition of $f$ and $g$ via
the obvious projection maps. Assuming again that $x=\langle
a,b,b,c,a,b\rangle\in\mathrm{Beh}(f)$ and that $y=\langle
b,d,b,c,d,b\rangle\in\mathrm{Beh}(g)$ we now have, for example, that $\langle
a,b,d,b,c,a,d,b\rangle\in\mathrm{Beh}(h)$. Thus $h$ ‘linearizes’ the
behaviours $x$ and $y$.

##  3 Implementation Guarantees and the CAP theorem

The aim of this section is to prove a formal version of the Brewer’s CAP
theorem. Recall that the CAP theorem states that the three guarantees of
_consistency_ , _availability_ and _partition tolerance_ cannot be
simultanously satisfied in a distributed system (cf. the introduction to this
article).

We start by formalising the notion of an _implementation guarantee_ :

######  Definition 16 (implementation guarantee).

An _implementation guarantee_ for a system $g$ is a set
$\mathcal{X}\subseteq\mathcal{P}(\mathrm{Beh}(g))$. The implementation
$f\overset{\sigma}{\Longrightarrow}g$ satisfies $\mathcal{X}$, written
$\sigma\models\mathcal{X}$, if $\\{\sigma(x)\mid
x\in\mathrm{Beh}(f)\\}\in\mathcal{X}$.

######  Definition 17 (consistency).

For $C\subseteq\mathrm{Beh}(g)$, the implementation guarantee
$\\{X\subseteq\mathrm{Beh}(g)\mid X\subseteq C\\}$is called _$C$ -consistency
guarantee_.

Simply put, an implementation guarantee satisfies $C$-consistency if it only
realizes behaviours in $C$. To avoid trivial solutions to consistency, one
also needs to consider guarantees that sufficiently many behaviours are
realized. We formula such _availability guarantees_ relative to a binary
relation $R\subseteq\mathrm{Beh}(g)^{2}$. Henceforth $R(x,\bullet):=\\{y\mid
xRy\\}$ and $dom(R):=\\{x\mid R(x,\bullet)\neq\emptyset\\}$.

######  Definition 18 (availability).

For a binary relation $R$ on $Beh(g)$, the implementation guarantees

$\displaystyle\\{X\subseteq\mathrm{Beh}(g)\mid\forall x\in
X(x\in\mathrm{dom}(R)\text{ implies }\exists y\in X\cap R(x,\bullet)\\}$
$\displaystyle\\{X\subseteq\mathrm{Beh}(g)\mid\forall x\in
X(R(x,\bullet)\subseteq X)\\}$

are called _weak_ and _strong $R$-availability_ respectively.

More directly, if an implementation realizes some behaviour
$x\in\mathrm{dom}(R)$, then weak (resp. strong) $R$-availability states that
it must also realize some (resp. all) $y\in R(x,\bullet)$. Strong availability
corresponds to the _input-enabledness_ condition used in I/O-automata [25].

######  Definition 19 (partition-tolerance).

Let $f\overset{\sigma_{1}}{\Longrightarrow}g_{1}$ and
$f\overset{\sigma_{2}}{\Longrightarrow}g_{2}$. The implementation guarantee

$\\{X\subseteq\mathrm{Beh}(f)\mid\forall x_{1},x_{2}\in X\exists x\in
X\sigma_{1}(x)=\sigma_{1}(x_{1}),\sigma_{2}(x)=\sigma_{2}(x_{2})\\}$

is called _$(\sigma_{1},\sigma_{2})$ -partition-tolerance_.

Partition-tolerance states that every pair of realized behaviours of $g_{1}$
and $g_{2}$ can be _jointly_ realized. In other words, implemented behaviours
in $g_{1}$ never restrict implemented behaviours in $g_{2}$ and vice versa.

We now state and prove a formalised version of the CAP theorem.

######  Theorem 20 (generalized CAP theorem).

Let $f\overset{\sigma_{1}}{\Longrightarrow}g_{1}$ and
$f\overset{\sigma_{2}}{\Longrightarrow}g_{2}$. Let $C\subseteq\mathrm{Beh}(f)$
and $R,S\subseteq\mathrm{Beh}(f)^{2}$ satisfy the following
‘entanglement’-condition

$\displaystyle\forall w\in\mathrm{Beh}(f)\exists x\in R(w,\bullet)\cap
dom(S)\forall v\in S(x,\bullet)\forall y,z\in\mathrm{Beh}(f):$
$\displaystyle\sigma_{1}(y)=\sigma_{1}(z)=\sigma_{1}(v)\land\sigma_{2}(y)=\sigma_{2}(w)\land\sigma_{2}(z)=\sigma_{2}(x)$
$\displaystyle\Rightarrow y\notin C\lor z\notin C$ ($\ast$)

which is illustrated by the following picture:

${w}$${x}$${v}$${z}$${y}$$\scriptstyle{\exists R}$$\scriptstyle{\forall
S}$$\scriptstyle{=_{\sigma_{2}}}$$\scriptstyle{=_{\sigma_{1}}}$$\scriptstyle{=_{\sigma_{1}}}$$\scriptstyle{=_{\sigma_{2}}}$

Then every runnable implementation of $f$ must violate at least one of the
following guarantees:

  1. -

$C$-consistency

  2. -

strong $R$-availability and weak $S$-availability

  3. -

$(\sigma_{1},\sigma_{2})$-partition-tolerance

###### Proof.

Let $h\overset{\sigma}{\Longrightarrow}f$ be any implementation of $f$, and
assume that it satisfies (2) and (3). We show that
$\sigma\nvDash\text{$C$-consistency}$. Let $w\in\mathrm{Beh}(f)$ be any
behaviour realized by $\sigma$, and pick $x$ as in the entanglement condition.
By strong $R$-availability, $\sigma$ realizes $x$. By weak $S$-availability
and the fact that $x\in dom(S)$, $\sigma$ also realizes some $v\in
S(x,\bullet)$. By $(\sigma_{1},\sigma_{2})$-partion-tolerance $\sigma$ also
realizes behaviours $y,z$ such that
$\sigma_{1}(y)=\sigma_{1}(z)=\sigma_{1}(v)$ and $\sigma_{2}(y)=\sigma_{2}(w)$,
$\sigma_{2}(z)=\sigma_{2}(x)$. But then by entanglement, $\sigma$ realizes a
behaviour that is not in $C$, violating $C$-consistency. ∎

Of course the usual formulation of the CAP theorem (cf. [21]) does not involve
a complicated entanglement condition. This is because it deals with a
concretely given set of implementation guarantees. Our formulation on the
other hand starts from arbitrary guarantees derived from the sets $C$, $R$ and
$S$, none of which needs to be a ‘read’ and ‘write’ guarantee as in [21]. The
entanglement condition is a logical abstraction of the relation between read
and write guarantees in CAP that allows the proof to go through. To verify
that Theorem 20 is indeed a generalization of CAP, we show in A how to recover
a standard form of the CAP theorem from it.

##  4 Logic and local reasoning principles

We now describe a simple logic of systems, and use this logic to state some
local reasoning principles.

Our logic is one of system behaviours, asserting properties of behaviours
through a satisfaction relation between systems and formulae of the form

$f,\mathcal{V},x\models\phi$

where $f$ is a system, $x$ is a behaviour of $f$, and $\mathcal{V}$ is a
valuation. This relation will be defined formally below.

The idea of such a logic is related to logics of state in the sense of van
Benthem-Bergstra and Hennessy-Milner (commonly known as ‘Hennessy-Milner’
theorems) — see, for example, [35, 26, 33] — in which a process with state $E$
is judged to satisfy a property $\phi$, denoted $E\models\phi$. In this
setting, ‘action modalities’ such as $[a]\phi$, where $a$ denotes a basic
action, play a key role in connecting the processes and the logic:

$\begin{array}[]{rcl}E\models[a]\phi&\mbox{iff}&\mbox{for all evolutions
$E\stackrel{{\scriptstyle a}}{{\rightarrow}}E^{\prime}$,
$E^{\prime}\models\phi$}\end{array}$

The key result in such a setting is that bisimulation equivalence of processes
is equivalent to their logical equivalence.

In our setting, we establish what may be understood as a corresponding result
between systems with equivalent behaviours and their logical properties. Our
result does not, however, require the presence of action modalities.
Behaviours are a basic component of models and the formula $\Box\phi$ simply
characterizes all of the behaviours of the system. This is explained formally
in Section 4.2.

We employ also structural connectives to characterize the compositional
structure of systems and, through a key concept of _interface_ , how the
behaviour of one component of a system affects a component to which it is
connected. We introduce ‘local reasoning’ principles, borrowing the name from
Separation Logic [23, 31, 29], to characterize these ideas. Connectives of
this kind are also present in logics of state; see, for example, [11, 10, 9,
1]).

###  4.1 The elementary logic

For every basic component $c\in\mathbb{C}$, we assume a set $Var(c)$ of
variables. All of these sets are assumed to be disjoint. A _valuation_ is a
function $\mathcal{V}$ mapping each $p\in Var(c)$ to a subset of
$\mathrm{Beh}(c)$.

For $C\subseteq\mathbb{C}$, the _elementary $C$-logic_ $\mathcal{L}(C)$ is
built from variables in $\bigcup_{c\in C}V(c)$ and the boolean connectives
$\land$ and $\lnot$. It is interpreted over triples $(f,\mathcal{V},x)$ where
$f$ is a system with $\mathrm{Comp}(f)\supseteq C$ and $x\in\mathrm{Beh}(f)$
using the following clauses:

$\displaystyle f,\mathcal{V},x\models p$ $\displaystyle:\iff
f_{c}(x)\in\mathcal{V}(p)\qquad\qquad(p\in Var(c))$ $\displaystyle
f,\mathcal{V},x\models\varphi\land\psi$ $\displaystyle:\iff
f,\mathcal{V},x\models\varphi\text{ and }f,\mathcal{V},x\models\psi$
$\displaystyle f,\mathcal{V},x\models\lnot\varphi$ $\displaystyle:\iff
f,\mathcal{V},x\nvDash\varphi$

We write $f,\mathcal{V}\models\varphi$ if $f,\mathcal{V},x\models\varphi$ for
all $x\in\mathrm{Beh}(f)$. As usual, we can define further boolean connectives
$\varphi\lor\psi:=\lnot(\lnot\varphi\land\lnot\psi)$ and
$\varphi\to\psi:=\lnot\varphi\lor\psi$. We let
$\mathcal{L}:=\mathcal{L}(\mathbb{C})$ and
$\mathcal{L}(f):=\mathcal{L}(\mathrm{Comp}(f))$.

For example, for $p\in Var(c)$ and $q\in Var(d)$ we have $f,\mathcal{V}\models
p\to q$ iff $f_{d}(x)\in\mathcal{V}(q)$ whenever $f_{c}(x)\in\mathcal{V}(p)$.
In words: If some behaviour of $f$ locally satisfies $p$ at the component $c$,
then it locally satisfies $q$ at $d$.

######  Lemma 21 (absoluteness).

Assume $f\overset{\sigma}{\Longrightarrow}g$ and $\alpha\in\mathcal{L}(g)$.
Then for all $x\in\mathrm{Beh}(f)$,

$f,\mathcal{V},x\models\alpha\iff g,\mathcal{V},\sigma(x)\models\alpha$

###### Proof.

By induction on $\alpha$. We only show the case $\alpha=p_{c}$, which uses the
properties of implementations:

$f,\mathcal{V},x\models p_{c}\iff f_{c}(x)\in\mathcal{V}(p_{c})\iff
g_{c}(\sigma(x))\in\mathcal{V}(p_{c})\iff g,\mathcal{V},\sigma(x)\models
p_{c}\qed$

As a corollary, we can observe that $g,\mathcal{V}\models\alpha$ implies
$f,\mathcal{V}\models\alpha$ whenever $f\overset{\sigma}{\Longrightarrow}g$
and $\alpha\in\mathcal{L}(g)$. Thus properties of $g$ that are expressible in
$\mathcal{L}(g)$ are inherited by any system implementing $g$.

We can state a first simple local reasoning principle: In order to prove that
a system satisfies some $\mathcal{L}$-property $\beta$, it suffices to find
subsystems $g$ and $h$ of $f$ and a property $\alpha$ such that $g$ enforces
that $\alpha$ is true at the interface of $f$ and $g$, and $h$ satisfies
$\beta$ whenever it satisfies $\alpha$ at its interface.

######  Theorem 22 (Local reasoning I).

Let $g\overset{\sigma}{\Longleftarrow}f\overset{\pi}{\Longrightarrow}h$ and
$I=\mathsf{Int}(f,g)\neq\emptyset$. The rule

$f,\mathcal{V}\models\beta\lx@proof@logical@and g,\mathcal{V}\models\alpha
h,\mathcal{V}\models\alpha\rightarrow\beta$

is admissible for all $\alpha\in\mathcal{L}(I)$ and $\beta\in\mathcal{L}(h)$.

###### Proof.

Let $x\in\mathrm{Beh}(f)$. By assumption,
$g,\mathcal{V},\sigma(x)\models\alpha$. As $g$ implements the interface $I$
(seen as a system), Lemma 21 implies
$I,\mathcal{V},g_{I}(\sigma(x))\models\alpha$. Furthermore,
$g_{I}(\sigma(x))=h_{I}(\pi(x))$, so we have
$I,\mathcal{V},h_{I}(\pi(x))\models\alpha$. Another application of Lemma 21
yields $h,\mathcal{V},\pi(x)\models\alpha$. By assumption we have
$h,\mathcal{V},\pi(x)\models\alpha\rightarrow\beta$ and so
$h,\mathcal{V},\pi(x)\models\beta$ follows. Thus, by yet another application
of Lemma 21, $f,\mathcal{V},x\models\beta$ as desired. ∎

Note that this theorem applies in particular to $f=g\otimes h$ (see Def. 10).

######  Example 23.

Consider two components $c$ and $d$ with
$\mathrm{Beh}(c)=\mathrm{Beh}(d)=\mathbb{Q}$. Let $g$ be a system implementing
$c$ and having $d\notin\mathrm{Comp}(g)$. We think of $g$ as a system that,
among other things, records the temperature in Celsius in its component $c$.
Moreover let $h$ be a converter from Celsius to Fahrenheit, modelled as
follows: $\mathrm{Comp}(h)=\\{c,d\\}$,
$h=id:\mathrm{Beh}(h)\to\mathrm{Beh}(c)\times\mathrm{Beh}(d)$ where
$\mathrm{Beh}(h)=\\{(x,y)\in\mathbb{Q}\mid y=x*1.8+32\\}$. Let $p_{c}\in V(c)$
and $p_{d}\in V(d)$ be variables with $\mathcal{V}(p_{c})=[0,10]$ and
$\mathcal{V}(p_{d})=[32,50]$. Assume we know that $g\models p_{c}$, that is,
only temperatures between $0$ and $10$ degree Celsius are measured by $g$.
Then we can formally derive that $g\otimes h$ only records temperatures
between $32^{\circ}$ and $50^{\circ}$ Fahrenheit:

$g\otimes h,\mathcal{V}\models p_{d}\lx@proof@logical@and g,\mathcal{V}\models
p_{c}h,\mathcal{V}\models p_{c}\to p_{d}$

###  4.2 Adding a universal modality

A standard extension $\mathcal{L}(C)\subseteq\mathcal{L}(C)^{\Box}$ adds a
universal modal operator $\Box$ to the language, subject to the following
clause for satisfaction:

$f,\mathcal{V},x\models\Box\varphi:\iff f,\mathcal{V},y\models\varphi\text{
for all }y\in\mathrm{Beh}(f)$

$\Box\varphi$ therefore denotes a property $\varphi$ that holds for _all_
behaviours $x\in\mathrm{Beh}(f)$. This corresponds to the standard clause for
$\Box$ in modal logic in the case that the accessibility relation is
universal; that is, in which each element is related to every other element.
We therefore obtain a syntactic variant of the well-known modal logic
$\mathbf{S5}$.

In the presence of the modal operator $\Box$, Lemma 21 fails, but some
variants of it remain provable. Call a formula in $\mathcal{L}^{\Box}$
_positive_ (resp.  _negative_) if no $\Box$ appears in the scope of an odd
(resp. even) number of $\lnot$’s. By a simple induction we can show the
following:

######  Lemma 24 (directed absoluteness).

Assume $f\overset{\sigma}{\Longrightarrow}g$. Then for all
$x\in\mathrm{Beh}(f)$,

$\displaystyle g,\mathcal{V},\sigma(x)\models\alpha\text{ implies
}f,\mathcal{V},x\models\alpha\quad\text{for positive
}\alpha\in\mathcal{L}(g)^{\Box}$ and $\displaystyle
f,\mathcal{V},x\models\alpha\text{ implies
}g,\mathcal{V},\sigma(x)\models\alpha\quad\text{for negative
}\alpha\in\mathcal{L}(g)^{\Box}.$

By tracking the absoluteness properties used in the proof of Theorem 22, we
can generalize slightly:

######  Theorem 25 (Local reasoning II).

Let $g\overset{\sigma}{\Longleftarrow}f\overset{\pi}{\Longrightarrow}h$ and
$I=\mathsf{Int}(f,g)\neq\emptyset$. The rule

$f,\mathcal{V}\models\beta\lx@proof@logical@and g,\mathcal{V}\models\alpha
h,\mathcal{V}\models\alpha\rightarrow\beta$

is admissible for all $\alpha\in\mathcal{L}(I)$ and positive
$\beta\in\mathcal{L}(h)^{\Box}$.

The next local reasoning principle makes use of the notion of an input
(Definition 4).

######  Theorem 26 (Local reasoning III).

Assume $I=\mathsf{Int}(f,g)\neq\emptyset$ is an input to $g$. The rule

$f\otimes g,\mathcal{V}\nvDash\beta\lx@proof@logical@and
f,\mathcal{V}\nvDash\alpha
g,\mathcal{V}\models\lnot\alpha\rightarrow\lnot\beta$

is admissible for all $\alpha\in\mathcal{L}(I)$ and negative
$\beta\in\mathcal{L}(g)^{\Box}$.

###### Proof.

Pick some $x\in\mathrm{Beh}(f)$ such that $f,\mathcal{V},x\models\lnot\alpha$.
By absoluteness, we have $I,\mathcal{V},f_{I}(x)\models\lnot\alpha$. Since $I$
is an input to $g$, we can find $y\in\mathrm{Beh}(g)$ such that
$g_{I}(y)=f_{I}(x)$. Again by absoluteness we obtain
$g,\mathcal{V},y\models\lnot\alpha$ and hence
$g,\mathcal{V},y\models\lnot\beta$. As $\lnot\beta$ is positive it follows
that $f\otimes g,\mathcal{V},(x,y)\models\lnot\beta$. ∎

Thus to show that some negative $\beta$ fails in $f\otimes g$ where the
interface is an input to $g$, it suffices to show that $f$ fails some property
$\alpha$ at the interface and that this failure causes the failure of $\beta$
in $g$. This needs not be true if $f$ is not an input, as then the behaviour
failing $\alpha$ might not be realized in $f\otimes g$.

Finally, for systems with trivial interface we can show the following.

######  Theorem 27.

The rule

$g\otimes h,\mathcal{V}\models\beta h,\mathcal{V}\models\beta$

is admissible for all $\beta\in\mathcal{L}(h)^{\Box}$ given that
$\mathsf{Int}(g,h)=\emptyset$.

###### Proof.

It suffices to prove by induction over $\delta\in\mathcal{L}(h)^{\Box}$ that

$g\otimes h,\mathcal{V},(x,y)\models\delta\iff h,\mathcal{V},y\models\delta$

This follows from the fact that $\mathrm{Beh}(g\otimes
h)=\mathrm{Beh}(g)\times\mathrm{Beh}(h)$ whenever
$\mathsf{Int}(g,h)=\emptyset$. We illustrate one step of the induction:

$\displaystyle g\otimes h,\mathcal{V},(x,y)\models\Box\delta^{\prime}$
$\displaystyle\iff\forall x^{\prime}\in\mathrm{Beh}(g)\forall
y^{\prime}\in\mathrm{Beh}(h).\,\,g\otimes
h,\mathcal{V},(x^{\prime},y^{\prime})\models\delta^{\prime}$
$\displaystyle\overset{IH}{\iff}\forall x^{\prime}\in\mathrm{Beh}(g)\forall
y^{\prime}\in\mathrm{Beh}(h).\,\,h,\mathcal{V},y^{\prime}\models\delta^{\prime}$
$\displaystyle\iff\forall
y^{\prime}\in\mathrm{Beh}(h).\,\,h,\mathcal{V},y^{\prime}\models\delta^{\prime}$
$\displaystyle\iff h,\mathcal{V},y\models\Box\delta^{\prime}\qed$

Remark: If $\beta$ encodes a Hoare triple, then the above is a frame rule.

Finally, we state a Hennessy-Milner Theorem (see, e.g., Theorem 2.24 in [3])
for our logic. The usual reference to bisimulations can be avoided here as we
are working with the simple modal logic $\mathbf{S5}$; instead, we use the
notion of a _type_.

######  Definition 28.

For a system $f$ with $\mathrm{Comp}(f)=C$ and $x\in\mathrm{Beh}(f)$ we define
$\mathsf{tp}(x):=\\{p\in V(C)\mid f,x\models p\\}$. Moreover we define
$\mathsf{tps}(f):=\\{\mathsf{tp}(x)\mid x\in\mathrm{Beh}(f)\\}$.

######  Theorem 29.

Let $f,g$ be two systems with $\mathrm{Comp}(f)=\mathrm{Comp}(g)=:C$, and
assume $V(C)$ is finite.222For simplicity we here use this condition stronger
than _image-finiteness_ that appears in Hennessy-Milner theorems in modal
logic, see, for example, [33]. For any
$(x,y)\in\mathrm{Beh}(f)\times\mathrm{Beh}(g)$ the following are equivalent:

  1. 1.

$f,x\models\varphi\iff g,y\models\varphi$, for all $\varphi\in\mathcal{L}(C)$,
and

  2. 2.

$\mathsf{tp}(x)=\mathsf{tp}(y)$.

The following are equivalent as well:

  1. 1.

$f,x\models\varphi\iff g,y\models\varphi$, for all
$\varphi\in\mathcal{L}(C)^{\Box}$, and

  2. 2.

$\mathsf{tp}(x)=\mathsf{tp}(y)$ and $\mathsf{tps}(f)=\mathsf{tps}(g)$.

###### Proof.

We show only the second equivalence. For (1)$\Rightarrow$(2) argue as follows:
Let $D:=\mathsf{tp}(x)$, and define $\varphi_{D}:=\bigwedge\\{p\mid p\in
D\\}\land\bigwedge\\{\lnot p\mid p\in V(C)\setminus D\\}.$ Then
$f,x\models\varphi_{D}$ and so $g,y\models\varphi_{D}$ by assumption, which in
turn implies $\mathsf{tp}(y)=\mathsf{tp}(x)=D$. Now let $D\in\mathsf{tps}(f)$,
say $D=\mathsf{tp}(x^{\prime})$ for some $x^{\prime}\in\mathrm{Beh}(f)$. Then
$f,x\models\lnot\Box\lnot\varphi_{D}$, and so by assumption
$g,y\models\lnot\Box\lnot\varphi_{D}$. It follows that for some
$y^{\prime}\in\mathrm{Beh}(g)$, $g,y^{\prime}\models\varphi_{D}$ and so
$\mathsf{tp}(y^{\prime})=D$, which implies $D\in\mathsf{tps}(g)$. Hence
$\mathsf{tps}(f)\subseteq\mathsf{tps}(g)$, and by a symmetric argument we get
$\mathsf{tps}(g)\subseteq\mathsf{tps}(f)$.

(2)$\Rightarrow$(1) is by induction on $\varphi$; we only consider the case
that $\varphi=\Box\psi$. Assume towards a contradiction that
$f,x\models\Box\psi$ and $g,y\nvDash\Box\psi$. The latter means that
$g,y^{\prime}\nvDash\psi$ for some $y^{\prime}\in\mathrm{Beh}(g)$. By
assumption there is an $x^{\prime}\in\mathrm{Beh}(f)$ such that
$\mathsf{tp}(x^{\prime})=\mathsf{tp}(y^{\prime})$. Then by the induction
hypothesis, $f,x^{\prime}\nvDash\psi$, contradicting $f,x\models\Box\psi$.
Conversely, if $f,x\nvDash\Box\psi$ then $f,x^{\prime}\nvDash\psi$ for some
$x^{\prime}\in\mathrm{Beh}(f)$. Pick $y^{\prime}\in\mathrm{Beh}(g)$ with
$\mathsf{tp}(y^{\prime})=\mathsf{tp}(x^{\prime})$; by induction hypothesis
$g,y^{\prime}\nvDash\psi$ and so $g,y\nvDash\Box\psi$ follows. ∎

###  4.3 Adding structural connectives

We have discussed extensively the sense in which systems consist of
components, connected by interfaces. We have also established an elementary
logic of system behaviours and, while we have considered some basic notions of
local reasoning, we have not yet given a logical characterization of the
compositional structure of systems.

To this send, we now consider two ‘structural’ connectives that are closely
related to the multiplicative conjunction found in relevance and bunched
logics. In particular, their use to characterize system structure resembles
the use of such connectives in the family of ‘separation logics’ and related
ideas [23, 31, 14, 30].

We define the following ternary relation between system–behaviour pairs, which
syntactically overloads the $\otimes$-operator from Definition 10:

$\begin{array}[]{rcl}\mbox{`$(f,x)=(f_{1},x_{1})\otimes(f_{2},x_{2})$'}&:\iff&\mbox{$f\equiv
f_{1}\otimes f_{2}$ and $\forall i\in\\{1,2\\}$}\\\ &&\mbox{$\forall
c\in\mathrm{Comp}(f_{i}):f_{c}(x)=(f_{i})_{c}(x_{i})$}\\\
\mbox{`$(f,x)=(f_{1},x_{1})\overset{\rightarrow}{\otimes}(f_{2},x_{2})$'}&:\iff&\mbox{$(f,x)=(f_{1},x_{1})\otimes(f_{2},x_{2})$
and}\\\ &&\mbox{$\mathsf{Int}(f_{1},f_{2})$ is an input to
$f_{2}$}\end{array}$

The first clause uses the equivalence notion $\equiv$ from Definition 6.

We can now define a logic $\mathcal{L}^{*}(C)$ that extends $\mathcal{L}(C)$
with binary operators $\ast$ and $\overset{\rightarrow}{\ast}$, which are
interpreted as follows:

$\begin{array}[]{rcl}f,\mathcal{V},x\models\varphi\ast\psi&\iff&\mbox{$(f,x)=(f_{1},x_{1})\otimes(f_{2},x_{2})$
for some}\\\ &&\mbox{\rm$f_{1},\mathcal{V},x_{1}\models\varphi$ and
$f_{2},\mathcal{V},x_{2}\models\psi$}\\\
f,\mathcal{V},x\models\varphi\overset{\rightarrow}{\ast}\psi&\iff&\mbox{\rm$(f,x)=(f_{1},x_{1})\overset{\rightarrow}{\otimes}(f_{2},x_{2})$
for some}\\\ &&\mbox{\rm$f_{1},\mathcal{V},x_{1}\models\varphi$ and
$f_{2},\mathcal{V},x_{2}\models\psi$}\end{array}$

Evidently, $\ast$ and $\overset{\rightarrow}{\ast}$ are multiplicative
conjunctions. The first characterizes a simple (ordered) decomposition of a
system into two components. The second also does this, but, in addition,
identifies the interface that supports the output of the first component to be
the input to the second.

######  Theorem 30 (local-global).

The following is a theorem for all positive $\varphi$ in $\mathcal{L}^{\Box}$:

$\varphi\ast\top\rightarrow\varphi$

In words, if a positive formula $\varphi$ holds in a part of the system, then
it holds in the whole system.

###### Proof.

Assume $f,\mathcal{V},x\models\varphi\ast\top$, and let
$(f_{1},x_{1}),(f_{2},x_{2})$ be system-behaviour pairs as in the satisfaction
clause for $\ast$. Thus $f_{1},\mathcal{V},x_{1}\models\varphi$. As $f$
implements $f_{1}$ via an implementation $\sigma$ that satisfies
$\sigma(x)=x_{1}$ and $\varphi$ is positive, it follows from Lemma 24 that
$f,\mathcal{V},x\models\varphi$. ∎

######  Theorem 31 (global-local).

The following is a theorem for all negative $\varphi$ in $\mathcal{L}^{\Box}$:

$\varphi\rightarrow(\psi\ast\psi^{\prime}\rightarrow(\psi\land\varphi)\ast\psi^{\prime})$

In words, if a negative formula $\varphi$ holds globally and some formula
$\psi$ holds locally, then $\varphi$ holds at that location as well.

###### Proof.

Assume both $\varphi$ and $\psi\ast\psi^{\prime}$ hold in a system. Clearly we
must have at least $(\psi\land\varphi)\ast\psi^{\prime}$ or
$(\psi\land\lnot\varphi)\ast\psi^{\prime}$ in the same system, so it suffices
to show that $(\psi\land\lnot\varphi)\ast\psi^{\prime}$ cannot be the case.
Indeed, as $\lnot\varphi$ is positive we have
$(\lnot\varphi)\ast\top\to\lnot\varphi$, or equivalently
$\varphi\to\lnot(\lnot\varphi\ast\top)$, from Theorem 30. As we assume
$\varphi$ this implies $\lnot(\lnot\varphi\ast\top)$, which is stronger than
the required $\lnot((\psi\land\lnot\varphi)\ast\psi^{\prime})$. ∎

Just as in linear, bunched, and relevance logics, the multiplicative
conjunction $\ast$ gives rise to another connective $-\\!\\!\\!\ast$ called
the ‘magic wand’:

$\displaystyle f,\mathcal{V},x\models\varphi-\\!\\!\\!\ast\psi\iff$
$\displaystyle f\otimes g,\mathcal{V},(x,y)\models\psi$
$\displaystyle\text{whenever }g,\mathcal{V},y\models\varphi$

Using $-\\!\\!\\!\ast$, a system $f$ can reason about its place inside a
larger structure $f\otimes g$. More specifically, $f,\mathcal{V},x$ satisfies
$\varphi-\\!\\!\\!\ast\psi$ if, whenever ‘plugged into’ a system satisfying
$\varphi$, the combined system satisfies $\psi$. Using
$\overset{\rightarrow}{\otimes}$ instead of $\otimes$ in the clause above
defines a ‘directed magic wand’, which then specifies properties of combined
systems where $f$ acts as an input.

We finally mention one further variant of a multiplicative conjunction.
Defining

‘$(f,x)=(f_{1},x_{1})\otimes_{d}(f_{2},x_{2})$’ $\displaystyle:\iff$
$(f,x)=(f_{1},x_{1})\otimes(f_{2},x_{2})$ and
$\mathsf{Int}(f_{1},f_{2})=\emptyset$

we introduce $\ast_{d}$ via the clause

$\displaystyle f,\mathcal{V},x\models\varphi\ast_{d}\psi$ $\displaystyle\iff$
$(f,x)=(f_{1},x_{1})\otimes_{d}(f_{2},x_{2})$ for some
$f_{1},x_{1},\mathcal{V}\models\varphi$ and
$f_{2},x_{2},\mathcal{V}\models\psi$

This — very restrictive — conjunction corresponds exactly to the
multiplicative conjunction of Separation Logic [23, 31], where it is
stipulated that the heap is split into disjoint parts. In our context, this
means that the two subsystems $f_{1}$ and $f_{2}$ have no components in
common.

We leave a more systematic study of these structural connectives to further
work. In particular, we would like to explore extensions of the Hennessy-
Milner theorem (Theorem 29) for $\ast$ and $\overset{\rightarrow}{\ast}$.

##  5 Discussion

We have established a minimalistic, behaviour-based framework for systems
modelling. We have shown that it encompasses key ideas from systems theory and
have given a logical analysis that supports reasoning about compositional
structure. Moreover, we have shown that even a rather concrete property of
distributed system — namely the CAP theorem — is witnessed in the framework.

In Section 4, we have laid out a minimal logical theory that, in addition to
having the standard classical connectives, is sufficient to characterize basic
system evolution (through a modality) and compositional structure (through
multiplicative conjunctions). The latter come in two versions, $\ast$ and
$\stackrel{{\scriptstyle\rightarrow}}{{\ast}}$, conveying whether a system can
be split into subsystems satisfying certain properties, or extended to a
larger system.

These structural connectives, which are similar to those considered in logics
for process algebras (for example, [11, 1]) and Separation Logic (for example,
[23, 29]).

###  5.1 Time

In this section, we briefly sketch how to introduce an explicit notion of time
into our setup. There are several ways of achieving this. The obvious one
would be to abandon the principle that behaviours are ‘unstructured’ sets,
instead imposing that they carrier a partial order $<$ which is interpreted as
a ‘happens before’ relation. In the trace model, we could then state for
example that $\langle a,b\rangle<\langle a,b,c\rangle$; that is, the behaviour
$\langle a,b,c\rangle$ is a _continuation_ of the behaviour $\langle
a,b\rangle$.

It turns out that such a modification of the framework is not necessary by
adopting a different philosophy. Instead of treating time as something
inherent to a system, we think of it as being _observed_ from outside the
system. Thus in order to introduce time to a system $f$, we should look at a
larger system that includes an _observer_ of $f$.

######  Definition 32.

A _timed implementation for $f$_ is a composition of $f$ with some basic
component $c$, where $f$ is an input and $c\notin\mathrm{Comp}(f)$ is a basic
component whose behaviour set is a partial order.

Here we think of $\mathrm{Beh}(c)$ as some form of bookkeeping of the
behaviours of $f$: For $t,t^{\prime}\in\mathrm{Beh}(c)$, $t<t^{\prime}$ means
that $c$ may experience $t$ before $t^{\prime}$. Incompatible behaviours
denote observations in different histories of the observer.

Let the timed implementation be given as
$f\overset{\sigma}{\Longleftarrow}h\overset{\rho}{\Longrightarrow}c$. We can
then import this ordering of events into the behaviours $x,y$ of $f$ by
setting $x\leq y$ if whenever $\sigma(v)=x$ and $\sigma(w)=y$ for some
behaviours $v,w\in\mathrm{Beh}(h)$, then we have $\rho(v)\leq\rho(w)$. Thus
$x\leq y$ holds if $y$ can only be observed by $c$ after $x$. $\leq$-minimal
elements in $\mathrm{Beh}(f)$ can be identified with initial states of $f$.

###  5.2 Tableaux systems

A substantial and theoretically important development — beyond our present
scope — would be to provide a proof system for the logic, together with
associated meta-theoretical results. One approach would be to develop a
labelled tableaux system, along the lines of those developed for other logics
involving mixes of classical and substructural connectives and modalities —
see, for example, [18, 24, 30].

We discuss how such a system of labelled tableaux can be developed from
standard knowledge about tableaux (rules, branchs, closure) [16, 32] and from
previous works on labelled tableaux for BI logic and some extensions [19, 18,
24]. The main questions concern the definition of labels, of labelled
formulas, of sets of label constraints, in such a way one can define closure
conditions for a tableaux branch and also what is a tableaux proof for the
given logic. As the labels and constraints have to capture the semantics of
the logic then the main challenge in our setting is to use the structure of
the logic’s models — here our system models — to determine a system of labels
to be used to express the constraints one has to assert or to check when
tableaux rules are applied.

The set-up of the logic presented in Section 4 is more complicated than
previously studied logical set-ups, and providing a labelled tableaux system
for our new logic presents more challenges. It is necessary and non-trivial to
identify an appropriate algebra of labels that captures the semantics
specified by the satisfaction relation

$f,\mathcal{V},x\models\phi$

as defined in Section 4, where $f$ is a system, $\mathcal{V}$ is a valuation,
and $x\in\mathrm{Beh}(f)$. Unpacking this, we can see some of the challenges.
Recall that, for every basic component $c\in\mathbb{C}$, we assume a set
$Var(c)$ of variables, and a _valuation_ is a function $\mathcal{V}$ mapping
each $p\in Var(c)$ to a subset of $\mathrm{Beh}(c)$.

The tableaux rules for the $\wedge$ and $\vee$ connectives can have the
following form:

$\begin{array}[]{c@{\qquad}c}\dfrac{(\mathbb{T}(\phi\wedge\psi),l)}{\begin{array}[]{c}(\mathbb{T}(\phi),l)\\\
(\mathbb{T}(\psi),l)\end{array}}\;\mathbb{T}\wedge&\dfrac{(\mathbb{F}(\phi\wedge\psi),l)}{(\mathbb{F}(\phi),l)\mid(\mathbb{F}(\psi),l)}\;\mathbb{F}\wedge\end{array}$

$\begin{array}[]{c@{\qquad}c}\dfrac{(\mathbb{T}(\phi\vee\psi),l)}{(\mathbb{T}(\phi),l)\mid(\mathbb{T}(\psi),l)}\;\mathbb{T}\vee&\dfrac{(\mathbb{F}(\phi\vee\psi),l)}{\begin{array}[]{c}(\mathbb{F}(\phi),l)\\\
(\mathbb{F}(\psi),l)\end{array}}\;\mathbb{F}\vee\end{array}$

We observe that there is no change of label $l$ when rules are applied. If we
look at the semantics for these connectives we can propose to have $l$ being
of the form $(f,x)$.

Our structural connectives, such as our $\ast$ and
$\stackrel{{\scriptstyle\rightarrow}}{{\ast}}$, typically refer to labels that
correspond to components of decomposition of the systems that support the
conjunctions $\phi\ast\psi$ and
$\phi\stackrel{{\scriptstyle\rightarrow}}{{\ast}}\psi$ in Section 4.3.
Tableaux systems have been given for various versions of BI (e.g., [19, 14,
18]) dealing with the connectives $\ast$ and $-\\!\\!\\!\ast$ . In that
setting, the multiplicative conjunction, $\ast$, can have the following rules:

$\dfrac{\langle\mathbb{T}(\phi\ast\psi),l\rangle}{\begin{array}[]{c}\langle\mathbb{T}(\phi),l_{1}\rangle\\\
\langle\mathbb{T}(\phi),l_{2}\rangle\end{array}}\;S(l,l_{1},l_{2})\;\mathbb{T}\ast\quad\mbox{and}\quad\dfrac{\langle\mathbb{F}(\phi\ast\psi),l\rangle}{\langle\mathbb{F}(\phi),l_{1}\rangle\mid\langle\mathbb{F}(\psi),l_{2}\rangle}\;R(l,l_{1},l_{2})\;\mathbb{F}\ast$

Here the rule $\mathbb{T}\ast$ introduces new labels $l_{1}$ and $l_{2}$ and
the label constraint (or assertion) $S(l,l_{1},l_{2})$ that is satisfied and
the rule $\mathbb{F}\ast$ can be applied only if there exist $l_{1}$ and
$l_{2}$ among the existing labels that satisfy the label constraint (or
requirement) $R(l,l_{1},l_{2})$ from a specific closure of the set of
assertions. The labels, their composition (with and operator $\bullet$) and
the label constraints allows us to capture the relational semantics of $\ast$
(see [19, 15, 14]).

In order to consider $\ast$ in our logic, we can propose that $l=(f,x)$,
$l_{1}=(f_{1},x_{1})$ and $l_{2}=(f_{2},x_{2})$, and $S(l,l_{1},l_{2})$ and
$R(l,l_{1},l_{2})$ of the form $l\ =\ l_{1}\bullet l_{2}$. The conditions on
the $f_{i}$s in the definition of $\ast$ are essential local and then we can
expect to find a way to express the constraints and to reason on their
satisfaction and resolution.

The interface-mediated $\stackrel{{\scriptstyle\rightarrow}}{{\ast}}$ rule
requires that the labelling algebra maintain dependencies across different
branches of the tableau as specified by the condition that
‘$\mathsf{Int}(f_{1},f_{2})$ is an input to $f_{2}$’. This is a relatively
complex and delicate development of the underlying approach to defining
tableaux systems, which we defer to another occasion.

Finally modalities, such as our $\Box$, typically require a relationship on
labels that corresponds to an accessibility relation on worlds. In our case,
accessibility is generated by behaviours.

$\frac{\langle\mathbb{T}(\Box\phi),l\rangle}{\langle\mathbb{T}(\phi),m\rangle}\quad
S(l,m)\quad\mathbb{T}\Box\quad\mbox{and}\quad\frac{\langle\mathbb{F}(\Box\phi),l\rangle}{\langle\mathbb{F}(\phi),m\rangle}\quad
R(l,m)\quad\mathbb{F}\Box$

Here, if we look the semantics of our logic, we could consider $l\ =\ (f,x)$
and $m\ =\ (f,y)$ with respectively the assertion $S(l,m)$ and the requirement
$R(l,m)$ expressing a relation between $x$ and $y$ that corresponds to the
accessibility relation associated to our $\Box$.

All these points illustrate that the definition of labels and label
constraints, and their treatment and resolution during a tableau construction,
require a deeper analysis and a relatively complex and delicate development in
order to propose a tableaux calculus that will be proved sound and complete.
Such questions will be explored in future work.

###  5.3 Other

Other future work might include systematic approaches to extensions of the
theory, while staying true to the minimalistic spirit in which the present
work has been carried out. For example, two general notions, which have not
been discussed, are _abstraction_ and _refinement_ of systems [6] together
with _substitution_ (see, for example, [7]) of models. The theory needed to
support these ideas will necessarily require an extension of our Hennessy-
Milner theorem (Theorem 29) to include the structural connectives. The
development of such a theory is a substantial project for further work. More
applied work might consider the integration stochastic behaviours, execution
and simulations, and model-checking.

## Acknowledgements

This work has been partially supported by the UK EPSRC research grants
EP/S013008/1 and EP/R006865/1. The authors are grateful to Tristan Caulfield
for helpful discussions of the systems background to the ideas presented.

## References

  * [1] G. Anderson and D. Pym.  A calculus and logic of bunched resources and processes.  Theoretical Computer Science, 614:63–96, 2016.
  * [2] M. Bednarczyk, L. Bernardinello, B. Caillaud, W. Pawlowski, and L. Pomello.  Modular system development with pullbacks.  volume 2679, pages 140–160, 06 2003.
  * [3] P. Blackburn, M. de Rijke, and Y. Venema.  Modal Logic.  Cambridge University Press, 2001.
  * [4] E. Brewer.  Towards robust distributed systems (abstract).  In Proceedings of the Nineteenth Annual ACM Symposium on Principles of Distributed Computing, PODC ’00, page 7, New York, NY, USA, 2000\. Association for Computing Machinery.
  * [5] E. Brewer.  CAP twelve years later: How the ‘rules’ have changed.  Computer, 45(2):23–29, 2012.
  * [6] M. J. Butler.  Mastering system analysis and design through abstraction and refinement, 2013.  University of Southampton eprints: https://eprints.soton.ac.uk/349769/1/Butler.pdf. Accessed 22 March 2023\.
  * [7] T. Caulfield, M.-C. Ilau, and D. Pym.  Engineering ecosystem models: Semantics and pragmatics.  In International Conference on Simulation Tools and Techniques, pages 236–258. Springer, 2022.
  * [8] T. Caulfield and D. Pym.  Modelling and simulating systems security policy.  In Proc. SimuTools, 2015.
  * [9] M. Collinson, B. Monahan, and D. Pym.  A Discipline of Mathematical Systems Modelling.  College Publications, 2012.
  * [10] M. Collinson and D. Pym.  Algebra and logic for resource-based systems modelling.  Mathematical Structures in Computer Science, 19(5):959–1027, 2009\.
  * [11] M. Dam.  Relevance Logic and Concurrent Computation.  PhD thesis, University of Edinburgh, 1989.
  * [12] L. de Alfaro and T. Henzinger.  Interface automata.  In ESEC/FSE 2001, pages 109–120. ACM, 2001.
  * [13] L. de Alfaro and T. Henzinger.  Interface theories for component-based design.  In EMSOFT 2001, LNCS 2211, pages 148–165. Springer Verlag, 2001\.
  * [14] S. Docherty.  Bunched Logics: A Uniform Approach.  PhD thesis, University College London, 2019.
  * [15] S. Docherty and D. Pym.  Modular tableaux calculi for separation theories.  In Christel Baier and Ugo Dal Lago, editors, LNCS 10803, pages 441–458. Springer, 2018.
  * [16] M. Fitting.  First-order Logic and Automated Theorem Proving.  Texts and Monographs in Computer Science. Springer-Verlag, 1990.
  * [17] J. Forrester.  Counterintuitive behavior of social systems.  Technology Review, 73(3):52–68, 1971.
  * [18] D. Galmiche, P. Kimmel, and D. Pym.  A substructural epistemic resource logic: theory and modelling applications.  Journal of Logic and Computation, 29(8):1251–1287, 01 2020.
  * [19] D. Galmiche, D. Méry, and D. Pym.  The semantics of BI and resource tableaux.  Mathematical Structures in Computer Science, 15(6):1033–1088, 2005\.
  * [20] S. Gilbert and N. Lynch.  Brewer’s conjecture and the feasibility of consistent, available, partition-tolerant web services.  ACM SIGACT News, 33(2):51–59, 2002.
  * [21] S. Gilbert and N. Lynch.  Perspectives on the CAP Theorem.  IEEE Computer, 45:30–36, 02 2012.
  * [22] J. Hillston.  A Compositional Approach to Performance Modelling.  Cambridge University Press, 1996.
  * [23] S.. Ishtiaq and P. W. O’Hearn.  Bi as an assertion language for mutable data structures.  In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’01, page 14–26. Association for Computing Machinery, 2001.
  * [24] D. Larchey-Wendling.  The formal strong completeness of partial monoidal Boolean BI.  Journal of Logic and Computation, 26(2):605–640, 06 2014.
  * [25] N. Lynch and M. Tuttle.  An introduction to input/output automata.  Laboratory for Computer Science, Massachusetts Institute of Technology, 1988.
  * [26] R. Milner.  Communication and Concurrency.  Prentice-Hall, Inc., USA, 1989.
  * [27] R. Milner.  Bigraphs as a model for mobile interaction.  In ICGT 2002, LNCS 2505, pages 8–13. Springer Verlag, 2002.
  * [28] R. Milner.  Bigraphs and their algebra.  Electronic Notes in Theoretical Computer Science, 209:5–19, 2008\.
  * [29] P. O’Hearn.  Separation logic.  Communications of the ACM, 62(2):86–95, 2019.
  * [30] D. J. Pym.  Resource Semantics: Logic as a Modelling Technology.  ACM SIGLOG News, 6(2):5–41, 2019.
  * [31] J. C. Reynolds.  Separation Logic: A Logic for Shared Mutable Data Structures.  In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, LICS ’02, page 55–74, USA, 2002. IEEE Computer Society.
  * [32] R. M. Smullyan.  First-order Logic.  Dover, 1968.
  * [33] C. Stirling.  Modal and Temporal Properties of Processes.  Springer, 2001.
  * [34] S. Tripakis, B. Lickly, T. Henzinger, and E. Lee.  A theory of synchronous relational interfaces.  ACM Transactions on Programming Languages and Systems, 33(4):1–41, 2011.
  * [35] J. van Benthem and J. Bergstra.  Logic of transition systems.  Journal of Logic, Language, and Information, 3:247–283, 1994.

##  Appendix A Proof of recovering a standard form of the CAP theorem

We start with an informal presentation and proof of CAP. Consider the
situation where there are two replicated copies of a database. User 1 and 2
interact with their respective copy of the database by overwriting the
dataset, or by requesting to read the current value of the data. In this
scenario, the CAP guarantees can be formulated as follows:

  * -

_consistency_ : Any read returns the content of the latest write (by either
user) at time of the submission of the read request, or any later write.

  * -

_availability_ : Any read and write requests are eventually performed.

  * -

_partition-tolerance_ : The system tolerates arbitrary message loss between
the two databases.

A semi-formal proof that these guarantees cannot be satisfied simultaneously
runs as follows: the current value of the database, and assume the connection
between the two copies of the database breaks down. Now imagine user 2 writing
the data $\chi^{\prime}\neq\chi$ on the database, followed by user 1
requesting to read the data. By the availability and partition-tolerance
requirements, the system must eventually return an answer
$\chi^{\prime\prime}$ to user 1. Clearly, if
$\chi^{\prime\prime}\neq\chi^{\prime}$ then consistency is violated as the
return value is outdated. So assume $\chi^{\prime\prime}=\chi^{\prime}$. But
now, as the first copy of the database has lost its connection to the second
one, it cannot distinguish between the situation where the write of user 2 has
occurred and a situation where no such write occurred. Thus, $\chi^{\prime}$
will also be the return value for user 1 in case the write didn’t occur, and
in that situation $\chi^{\prime}$ would be an outdated value thus violating
consistency.

We now formalize this scenario to show that the impossibility result is an
instance of Theorem 20. In fact, by writing out the proof of Theorem 20 with
the formalization presented below one essentially obtains the proof in [20].
For $i=1,2$ consider a language $\Sigma_{i}$ that contains for every timestamp
$t\in\mathbb{Q}^{+}_{0}$ and string $s$ one of the atoms below left, with
their intended interpretation given on the right:

$t:rd^{i}?$ | $\ldots$ | at time $t$, user $i$ requests a read
---|---|---
$t:rd^{i}(s)$ | $\ldots$ | at time $t$, user $i$ reads value $s$
$t:wr^{i}(s)$ | $\ldots$ | at time $t$, user $i$ writes value $s$

A sequence in $(\Sigma_{1}\cup\Sigma_{2})^{*}$ is _well-formed_ if its
timestamps are strictly ascending. Let $\mathcal{S}$ denote the set of well-
formed sequences, and let $\mathcal{S}_{i}:=\mathcal{S}\cap\Sigma_{i}^{*}$.

We consider a composition
$g_{1}\overset{\sigma_{1}}{\Longleftarrow}f\overset{\sigma_{2}}{\Longrightarrow}g_{2}$
where the behaviour sets of $g_{1},g_{2}$ and $f$ are
$\mathcal{S}_{1},\mathcal{S}_{2}$ and $\mathcal{S}$ respectively. The
implementation $\sigma_{i}$ is the obvious projection function that removes
from a sequence in $\mathcal{S}$ all actions not initiated by the user $i$.
The _current value at $t$_ of a sequence in $\mathcal{S}$ is the value of the
latest write in it (by either user) with timestamp $\leq t$; if no such write
exists, the current value equals some fixed string $s_{0}$ that we call the
_initial value_. A sequence in $\mathcal{S}$ is _consistent_ if whenever
$t:rd^{i}?$ and $t^{\prime}:rd^{i}(s)$ are a pair of actions in the sequence
with $t<t^{\prime}$ and no read by $i$ in between, then $s$ coincides with the
current value at some timestamp $\geq t$ and $\leq t^{\prime}$. Let $C$ be the
set of all consistent sequences.

Define two binary relations on $\mathcal{S}$. $R$ relates any sequence to the
same sequence appended with $t:wr^{2}(s)$, for some string $s$ (and
sufficiently large $t$). $S$ relates a sequence to the same sequence appended
with $t:rd^{1}?$, a finite string of actions by user $2$, and a final
$t^{\prime}:rd^{1}(s)$, for some string $s$. So, if an implementation of $f$
satisfies strong $R$-availability, it allows user $2$ to write anything at any
time. If it satisfies weak $S$-satisfiability, it allows user $1$ to send a
request anytime and wait until it is answered.

So, clearly $C$-consistency, strong $R$-, and weak $S$-availability are are
required guarantees in the CAP scenario. We will now show that these are
incompatible with $(\sigma_{1},\sigma_{2})$-partition-tolerance. By Theorem
20, it suffices to demonstrate the entanglement condition. Indeed, let
$w\in\mathcal{L}$ and let $x\in R(w,\bullet)$ an extension of $w$ with
$t:wr^{2}(s)$ where $s$ is neither $s_{0}$ nor the value of any write in $w$.
Now consider any $v\in S(x,\bullet)$. Such $v$ is of the form
$v=w\smallfrown\langle
t:wr^{2}(s),t^{\prime}:rd^{1}?,\ldots,t^{\prime\prime}:rd^{1}(s^{\prime})\rangle$,
where the dotted part contains only actions by user $2$. Let
$y,z\in\mathcal{L}$ satisfy $\sigma_{1}(y)=\sigma_{1}(z)=\sigma_{1}(v)$,
$\sigma_{2}(y)=\sigma_{2}(w)$ and $\sigma_{2}(z)=\sigma_{2}(x)$. Therefore,
$y=w\smallfrown\langle
t^{\prime}:rd^{1}?,t^{\prime\prime}:rd^{1}(s^{\prime})\rangle$ and
$z=w\smallfrown\langle
t:wr^{2}(s),t^{\prime}:rd^{1}?,t^{\prime\prime}:rd^{1}(s^{\prime})\rangle$. We
have to show $y\notin C$ or $z\notin C$. Let us assume $z\in C$. Then
$s^{\prime}=s$. Since, by construction, $s$ is neither $s_{0}$ nor the value
of any write in $w$, it follows that $y\notin C$. This demonstrates the
entanglement condition.


14.22636pt=\int_{0}^{+\infty}\int_{\Omega_{1}}^{\Omega_{2}}\\!f_{ZY}(z,y)\,\mathrm{d}z\,\mathrm{d}y=\int_{0}^{+\infty}\int_{\Omega_{1}}^{\Omega_{2}}\\!f_{X}(zy)\cdot
f_{Y}(y)\,\mathrm{d}z\,\mathrm{d}y\\\ &\hskip
14.22636pt=\int_{0}^{+\infty}\left(\int_{\Omega_{1}}^{\Omega_{2}}\\!f_{X}(zy)\,\mathrm{d}z\right)f_{Y}(y)\,\mathrm{d}y=\int_{0}^{+\infty}\left(\int_{\Omega_{1}y}^{\Omega_{2}y}\\!\frac{1}{y}f_{X}(x)\,\mathrm{d}x\right)f_{Y}(y)\,\mathrm{d}y\\\
&\hskip
14.22636pt=\int_{0}^{+\infty}\left(\int_{\Omega_{1}y}^{\Omega_{2}y}\\!f_{X}(x)\,\mathrm{d}x\right)\frac{f_{Y}(y)}{y}\,\mathrm{d}y\\\
\end{split}$

The proof of the second result is completely analogous. $\Box$

Proof of Proposition 7
The results on $\text{{op}}^{G^{x}}_{x}(i)$ ($i\in\\{1,2\\}$) are direct
consequences of Proposition 3, the fact that $U(y,x,i)$ are normal random
variables as described in Table 3, and the independence/mutual exclusiveness
of the involved random variables (which allow us to use the restricted
disjunction/conjunction formulas from formula (4), Subsection 3.1).
For the case of $\text{{rom}}^{G^{x}}_{x}(\omega_{1},\omega_{2})$, applying
Corollary 1, we get that $\text{{rom}}^{G^{x}}_{x}(\omega_{1},\omega_{2})$ is
true if and only if:

$\displaystyle(\text{{ugain}}^{G^{x}}(x,1)>0)\bigwedge(\text{{ugain}}^{G^{x}}(x,2)<0)\bigwedge(\text{{ugain}}^{G^{x}}(\bar{x},1)<0)$
$\displaystyle\bigwedge(\text{{ugain}}^{G^{x}}(\bar{x},2)>0)\bigwedge\left(\omega_{1}<\frac{\text{{ugain}}^{G^{x}}(\bar{x},2)}{\text{{ugain}}^{G^{x}}(\bar{x},2)-\text{{ugain}}^{G^{x}}(\bar{x},1)}<\omega_{2}\right)$
$\displaystyle\bigvee$
$\displaystyle(\text{{ugain}}^{G^{x}}(x,1)<0)\bigwedge(\text{{ugain}}^{G^{x}}(x,2)>0)\bigwedge(\text{{ugain}}^{G^{x}}(\bar{x},1)>0)\bigwedge$
$\displaystyle(\text{{ugain}}^{G^{x}}(\bar{x},2)<0)\bigwedge\left(\omega_{1}<\frac{\text{{ugain}}^{G^{x}}(\bar{x},2)}{\text{{ugain}}^{G^{x}}(\bar{x},2)-\text{{ugain}}^{G^{x}}(\bar{x},1)}<\omega_{2}\right)$

Obviously, the above disjunction contains mutually exclusive events, so the
probability
${\mathcal{P}}\boldsymbol{\left[\right.}\text{{rom}}^{G^{x}}_{x}(\omega_{1},\omega_{2})\boldsymbol{\left.\right]}$
is the sum of the probability of each disjunct (by the restricted disjunctive
formula – see formula (4), Subsection 3.1). So, let us compute the probability
of the first disjunct.
We observe that the events $\text{{ugain}}^{G^{x}}(x,1)$,
$\text{{ugain}}^{G^{x}}(x,2)$ are independent to each other and also
independent to the other conjuncts. Moreover:

$\displaystyle\omega_{1}<\frac{\text{{ugain}}^{G^{x}}(\bar{x},2)}{\text{{ugain}}^{G^{x}}(\bar{x},2)-\text{{ugain}}^{G^{x}}(\bar{x},1)}<\omega_{2}$
$\displaystyle\Leftrightarrow\frac{\omega_{1}-1}{\omega_{1}}<\frac{\text{{ugain}}^{G^{x}}(\bar{x},1)}{\text{{ugain}}^{G^{x}}(\bar{x},2)}<\frac{\omega_{2}-1}{\omega_{2}}$

Thus, we can apply Lemma 1 for the last three conjuncts (for
$\Omega_{1}=\frac{\omega_{1}-1}{\omega_{1}}$,
$\Omega_{2}=\frac{\omega_{2}-1}{\omega_{2}}$), getting that the probability of
the first conjunction is equal to:

$\begin{split}&(1-F_{U(x,x,1)}(0))\cdot
F_{U(x,x,2)}(0)\cdot\int_{0}^{+\infty}\left(\int_{\Omega_{1}u_{2}}^{\Omega_{2}u_{2}}\\!f_{U(x,\bar{x},1)}(u_{1})\,\mathrm{d}u_{1}\right)\frac{f_{U(x,\bar{x},2)}(u_{2})}{u_{2}}\,\mathrm{d}u_{2}\\\
\end{split}$

Working analogously for the second disjunct, and summing the resulting
probability with the one above, we get the result.
For $\text{{rpm}}^{G^{x}}_{x}(\omega_{1},\omega_{2})$, we work analogously,
applying the second bullet of Corollary 1 as above.
For $\text{{in}}^{G^{x}}_{x}$, we observe that if $\text{{in}}^{G^{x}}_{x}$ is
true, then $G^{x}$ is degenerate, which has probability $0$. $\Box$

Proof of Theorem 8
The proof is direct from Proposition 4 (and the respective Table 2), combined
with the fact that the different cases in the disjunction are mutually
exclusive, so we can use the restricted disjunction formula of (4) in
Subsection 3.1. $\Box$

Proof of Theorem 9]
The proof is direct from Proposition 4 (and the respective Table 2), combined
with the fact that the different cases in the disjunction are mutually
exclusive, so we can use the restricted disjunction formula of (4) in
Subsection 3.1. $\Box$

###  A.4 Effect of modifying tolerance ($\varepsilon$)

Proof of Proposition 10
We first observe that, for any $x\in\\{r,c\\}$ and any $a,b,c$ such that:
$0\leq a\leq b\leq c\leq 1$, we have that:

$\displaystyle{\mathcal{P}}\boldsymbol{\left[\right.}\text{{rom}}^{G^{x}}_{x}(a,c)\boldsymbol{\left.\right]}={\mathcal{P}}\boldsymbol{\left[\right.}\text{{rom}}^{G^{x}}_{x}(a,b)\boldsymbol{\left.\right]}+{\mathcal{P}}\boldsymbol{\left[\right.}\text{{rom}}^{G^{x}}_{x}(b,c)\boldsymbol{\left.\right]}$
(ROM1)
$\displaystyle{\mathcal{P}}\boldsymbol{\left[\right.}\text{{rom}}^{G^{x}}_{x}(a,c)\boldsymbol{\left.\right]}=0\Leftrightarrow
a=c$ (ROM2)
$\displaystyle{\mathcal{P}}\boldsymbol{\left[\right.}\text{{rpm}}^{G^{x}}_{x}(a,c)\boldsymbol{\left.\right]}={\mathcal{P}}\boldsymbol{\left[\right.}\text{{rpm}}^{G^{x}}_{x}(a,b)\boldsymbol{\left.\right]}+{\mathcal{P}}\boldsymbol{\left[\right.}\text{{rpm}}^{G^{x}}_{x}(b,c)\boldsymbol{\left.\right]}$
(RPM1)
$\displaystyle{\mathcal{P}}\boldsymbol{\left[\right.}\text{{rpm}}^{G^{x}}_{x}(a,c)\boldsymbol{\left.\right]}=0\Leftrightarrow
a=c$ (RPM2)

From Theorem 8, and for $i=1,2$:

${\mathcal{P}}\boldsymbol{\left[\right.}mG\mathrel{\mathop{\mathchar
58\relax}}\varepsilon_{i}\text{-misinformed}\boldsymbol{\left.\right]}=P_{r,i}\cdot
P_{c,i},$

where $P_{r,i},P_{c,i}$ are determined by the second column of Table 5 for the
respective $\varepsilon_{i}$.
Similarly, from Theorem 9, and for $i=1,2$:

${\mathcal{P}}\boldsymbol{\left[\right.}mG\mathrel{\mathop{\mathchar
58\relax}}\text{inverse-}\varepsilon_{i}\text{-misinformed}\boldsymbol{\left.\right]}=P_{r,i}^{\prime}\cdot
P_{c,i}^{\prime},$

where $P_{r,i}^{\prime},P_{c,i}^{\prime}$ are determined by the third column
of Table 5 for the respective $\varepsilon_{i}$.
Now, let us focus on the first bullet of the proposition. By Tables 3, 4, 5,
it is easy to conclude that, for any $x\in\\{r,c\\}$, $i\in\\{1,2\\}$, the
computation of $P_{x,i},P_{x,i}^{\prime}$ is not affected by the value of
$\varepsilon_{i}$, and, thus: $P_{x,1}=P_{x,2}$,
$P_{x,1}^{\prime}=P_{x,2}^{\prime}$ for $x\in\\{r,c\\}$, which shows the
result.
Now, let us focus on the second bullet, and let us consider
$P_{r,i},P_{r,i}^{\prime}$ first. Set:

$\begin{split}&\omega_{1,1}=\max\\{0,p^{0}-\varepsilon_{1}\\},\;\;\omega_{2,1}=\min\\{1,p^{0}+\varepsilon_{1}\\},\\\
&\omega_{1,2}=\max\\{0,p^{0}-\varepsilon_{2}\\},\;\;\omega_{2,2}=\min\\{1,p^{0}+\varepsilon_{2}\\}\\\
\end{split}$

Since $0\leq\varepsilon_{1}<\varepsilon_{2}$, we get that:
$0\leq\omega_{1,2}\leq\omega_{1,1}\leq\omega_{2,1}\leq\omega_{2,2}\leq 1$.
Moreover, since $\varepsilon_{1}<\varepsilon_{2}$, it follows that:

$\begin{split}&\omega_{1,1}=\omega_{1,2}\Leftrightarrow\omega_{1,1}=\omega_{1,2}=0\Leftrightarrow\left(\begin{array}[]{c}p^{0}\leq\varepsilon_{1}\\\
\text{and}\\\ p^{0}\leq\varepsilon_{2}\end{array}\right)\Leftrightarrow
p^{0}\leq\varepsilon_{1}\end{split}$

Analogously:

$\begin{split}&\omega_{2,1}=\omega_{2,2}\Leftrightarrow\omega_{2,1}=\omega_{2,2}=1\Leftrightarrow\left(\begin{array}[]{c}1-p^{0}\leq\varepsilon_{1}\\\
\text{and}\\\ 1-p^{0}\leq\varepsilon_{2}\end{array}\right)\Leftrightarrow
1-p^{0}\leq\varepsilon_{1}\end{split}$

Using the order among $\omega_{i,j}$, and by applying (ROM1) twice, we get
that:

$\begin{split}{\mathcal{P}}\boldsymbol{\left[\right.}\text{{rom}}^{G^{r}}_{r}(\omega_{1,2},\omega_{2,2})\boldsymbol{\left.\right]}&={\mathcal{P}}\boldsymbol{\left[\right.}\text{{rom}}^{G^{r}}_{r}(\omega_{1,2},\omega_{1,1})\boldsymbol{\left.\right]}+{\mathcal{P}}\boldsymbol{\left[\right.}\text{{rom}}^{G^{r}}_{r}(\omega_{1,1},\omega_{2,1})\boldsymbol{\left.\right]}\\\
&\hskip
30.00005pt+{\mathcal{P}}\boldsymbol{\left[\right.}\text{{rom}}^{G^{r}}_{r}(\omega_{2,1},\omega_{2,2})\boldsymbol{\left.\right]}\\\
\end{split}$

Now given the fact that probabilities are non-negative, and (ROM2), we have:

$\begin{split}&{\mathcal{P}}\boldsymbol{\left[\right.}\text{{rom}}^{G^{r}}_{r}(\omega_{1,1},\omega_{2,1})\boldsymbol{\left.\right]}\leq{\mathcal{P}}\boldsymbol{\left[\right.}\text{{rom}}^{G^{r}}_{r}(\omega_{1,2},\omega_{2,2})\boldsymbol{\left.\right]}\text{
and: }\\\
&{\mathcal{P}}\boldsymbol{\left[\right.}\text{{rom}}^{G^{r}}_{r}(\omega_{1,1},\omega_{2,1})\boldsymbol{\left.\right]}={\mathcal{P}}\boldsymbol{\left[\right.}\text{{rom}}^{G^{r}}_{r}(\omega_{1,2},\omega_{2,2})\boldsymbol{\left.\right]}\Leftrightarrow\\\
&\hskip 48.36958pt\left(\omega_{1,1}=\omega_{1,2}\text{ and
}\omega_{2,1}=\omega_{2,2}\right)\end{split}$

Using analogous reasoning we get:

$\begin{split}&{\mathcal{P}}\boldsymbol{\left[\right.}\text{{rpm}}^{G^{r}}_{r}(\omega_{1,1},\omega_{2,1})\boldsymbol{\left.\right]}\leq{\mathcal{P}}\boldsymbol{\left[\right.}\text{{rpm}}^{G^{r}}_{r}(\omega_{1,2},\omega_{2,2})\boldsymbol{\left.\right]}\text{
and: }\\\
&{\mathcal{P}}\boldsymbol{\left[\right.}\text{{rpm}}^{G^{r}}_{r}(\omega_{1,1},\omega_{2,1})\boldsymbol{\left.\right]}={\mathcal{P}}\boldsymbol{\left[\right.}\text{{rpm}}^{G^{r}}_{r}(\omega_{1,2},\omega_{2,2})\boldsymbol{\left.\right]}\Leftrightarrow\\\
&\hskip 48.36958pt\left(\omega_{1,1}=\omega_{1,2}\text{ and
}\omega_{2,1}=\omega_{2,2}\right)\end{split}$

Using the above, and Tables 3, 4, 5, we can easily conclude that $P_{r,1}\leq
P_{r,2}$ and $P_{r,1}^{\prime}\leq P_{r,2}^{\prime}$. Moreover:

$\begin{split}&P_{r,1}=P_{r,2}\Leftrightarrow\left(\begin{array}[]{c}\omega_{1,1}=\omega_{1,2}\\\
\text{and}\\\
\omega_{2,1}=\omega_{2,2}\end{array}\right)\Leftrightarrow\left(\begin{array}[]{c}p^{0}\leq\varepsilon_{1}\\\
\text{and}\\\ 1-p^{0}\leq\varepsilon_{1}\end{array}\right)\end{split}$

Analogously:

$P_{r,1}^{\prime}=P_{r,2}^{\prime}\Leftrightarrow\left(\begin{array}[]{c}p^{0}\leq\varepsilon_{1}\\\
\text{and}\\\ 1-p^{0}\leq\varepsilon_{1}\end{array}\right)$

Reasoning analogously for the case of $P_{c,i},P_{c,i}^{\prime}$, we get:

$\text{For }P_{c,1}\leq P_{c,2}\text{ :
}P_{c,1}=P_{c,2}\Leftrightarrow\left(\begin{array}[]{c}q^{0}\leq\varepsilon_{1}\\\
\text{and}\\\ 1-q^{0}\leq\varepsilon_{1}\end{array}\right)$

$\text{For }P_{c,1}^{\prime}\leq P_{c,2}^{\prime}\text{ :
}P_{c,1}^{\prime}=P_{c,2}^{\prime}\Leftrightarrow\left(\begin{array}[]{c}q^{0}\leq\varepsilon_{1}\\\
\text{and}\\\ 1-q^{0}\leq\varepsilon_{1}\end{array}\right)$

By the hypothesis of the second bullet with regards to $NE(G^{0})$, Tables 3,
4, 5, and the above relations, the cases (2a), (2b) of the Theorem follow
easily.
Now let us focus on the third bullet. First, we observe that, by Table 5, the
result is obvious for the case of $\varepsilon$-misinformed, so let us focus
on the case of inverse-$\varepsilon$-misinformed. If $\varepsilon_{2}\leq
0.5$, then $\varepsilon_{1}\leq 0.5$, so the result is again obvious by Table
5. So let us focus on the scenario where $\varepsilon_{2}>0.5$.
To show the result for this case, we use an approach similar to the one
employed for the second bullet. In particular, we consider $P_{r,i}^{\prime}$
first. Set:

$\begin{split}&\omega_{1,1}^{\prime}=\max\\{0,1-\varepsilon_{1}\\},\;\;\omega_{2,1}^{\prime}=\min\\{1,\varepsilon_{1}\\},\\\
&\omega_{1,2}^{\prime}=\max\\{0,1-\varepsilon_{2}\\},\;\;\omega_{2,2}^{\prime}=\min\\{1,\varepsilon_{2}\\}\\\
\end{split}$

Using an analogous procedure (as in the second bullet), and the fact that
$0\leq\varepsilon_{1}<\varepsilon_{2}$, we conclude that:

$\displaystyle
0\leq\omega_{1,2}^{\prime}\leq\omega_{1,1}^{\prime}\leq\omega_{2,1}^{\prime}\leq\omega_{2,2}^{\prime}\leq
1$
$\displaystyle\omega_{1,1}^{\prime}=\omega_{1,2}^{\prime}\Leftrightarrow\varepsilon_{1}\leq
1$
$\displaystyle\omega_{2,1}^{\prime}=\omega_{2,2}^{\prime}\Leftrightarrow\varepsilon_{1}\leq
1$

Also, using (RPM1), (RPM2), and the fact that probabilities are non-negative,
we get, as in the second bullet:

$\begin{split}&{\mathcal{P}}\boldsymbol{\left[\right.}\text{{rpm}}^{G^{r}}_{r}(\omega_{1,1}^{\prime},\omega_{2,1}^{\prime})\boldsymbol{\left.\right]}\leq{\mathcal{P}}\boldsymbol{\left[\right.}\text{{rpm}}^{G^{r}}_{r}(\omega_{1,2}^{\prime},\omega_{2,2}^{\prime})\boldsymbol{\left.\right]}\\\
&{\mathcal{P}}\boldsymbol{\left[\right.}\text{{rpm}}^{G^{r}}_{r}(\omega_{1,1}^{\prime},\omega_{2,1}^{\prime})\boldsymbol{\left.\right]}={\mathcal{P}}\boldsymbol{\left[\right.}\text{{rpm}}^{G^{r}}_{r}(\omega_{1,2}^{\prime},\omega_{2,2}^{\prime})\boldsymbol{\left.\right]}\\\
&\hskip
34.14322pt\Leftrightarrow\left(\omega_{1,1}^{\prime}=\omega_{1,2}^{\prime}\text{
and }\omega_{2,1}^{\prime}=\omega_{2,2}^{\prime}\right)\\\ \end{split}$

Therefore, given that $\varepsilon_{1}>\varepsilon_{2}>0.5$:

$\left(P_{r,1}^{\prime}\leq P_{r,2}^{\prime}\text{ and
}P_{r,1}^{\prime}=P_{r,2}^{\prime}\right)\Leftrightarrow\varepsilon_{1}\leq
1\\\ $

Working analogously for $P_{c,i}^{\prime}$, we get:

$\left(P_{c,1}^{\prime}\leq P_{c,2}^{\prime}\text{ and
}P_{c,1}^{\prime}=P_{c,2}^{\prime}\right)\Leftrightarrow\varepsilon_{1}\leq
1\\\ $

By the hypothesis of the second bullet with regards to $NE(G^{0})$, Tables 3,
4, 5, and the above relations, the remaining subcases of (3a), (3b) of the
Theorem follow easily. $\Box$

###  A.5 Effect of changing the game ($G^{0}$) and the mean ($M$)

Proof of Proposition 11
From Table 3, we observe that, for the given $x$, and for any $i\in\\{1,2\\}$:

$\begin{split}\mu_{U(x,r,i)}&=(P^{0}_{r}[1,i]+M^{x}_{r}[1,i])-(P^{0}_{r}[2,i]+M^{x}_{r}[2,i])\\\
&=(\overline{P^{0}_{r}}[1,i]+\overline{M^{x}_{r}}[1,i]+a)-(\overline{P^{0}_{r}}[2,i]+\overline{M^{x}_{r}}[2,i]+a)\\\
&=\overline{\mu_{U(x,r,i)}}.\end{split}$

Analogously, we can show that $\mu_{U(x,c,i)}=\overline{\mu_{U(x,c,i)}}$ for
any $i\in\\{1,2\\}$. Also, it is clear that
$d_{U(x,y,i)}=\overline{d_{U(x,y,i)}}$ for any $y\in\\{r,c\\}$,
$i\in\\{1,2\\}$. Combining these two facts, the results are obvious. $\Box$

Proof of Proposition 12
Take any $x\in\\{r,c\\}$. Set $b_{x}=-a_{G}-a_{x}$. We observe that
$G^{0}+M^{x}=\overline{G^{0}}+\overline{M^{x}}+\boldsymbol{[b_{x}]}$. Thus, by
Proposition 11, we get, for $x\in\\{r,c\\}$:

  * •

For any $i\in\\{1,2\\}$,

${\mathcal{P}}\boldsymbol{\left[\right.}\text{{op}}^{G^{x}}_{x}(i)\boldsymbol{\left.\right]}={\mathcal{P}}\boldsymbol{\left[\right.}\text{{op}}^{\overline{G^{x}}}_{x}(i)\boldsymbol{\left.\right]}$

  * •

For any $0\leq\omega_{1}\leq\omega_{2}\leq 1$,

${\mathcal{P}}\boldsymbol{\left[\right.}\text{{rom}}^{G^{x}}_{x}(\omega_{1},\omega_{2})\boldsymbol{\left.\right]}={\mathcal{P}}\boldsymbol{\left[\right.}\text{{rom}}^{\overline{G^{x}}}_{x}(\omega_{1},\omega_{2})\boldsymbol{\left.\right]}$

  * •

For any $0\leq\omega_{1}\leq\omega_{2}\leq 1$,

${\mathcal{P}}\boldsymbol{\left[\right.}\text{{rpm}}^{G^{x}}_{x}(\omega_{1},\omega_{2})\boldsymbol{\left.\right]}={\mathcal{P}}\boldsymbol{\left[\right.}\text{{rpm}}^{\overline{G^{x}}}_{x}(\omega_{1},\omega_{2})\boldsymbol{\left.\right]}$

In addition, game theoretic results tell us that
$NE(G^{0})=NE(\overline{G^{0}})$. Combining the above with Theorems 8, 9 and
Table 5, the result follows directly. $\Box$

###  A.6 Effect of modifying noise intensity ($D$)

Proof of Proposition 13
Consider the family of random variables $\overline{U(y,x,i)}$ for
$\overline{mG}$. By the definition of $\overline{M},\overline{}D$ and by Table
3, it follows that, for any $x,y\in\\{r,c\\}$, and for any $i\in\\{1,2\\}$, it
holds that:

$\mu_{\overline{U(y,x,i)}}=\lambda\mu_{U(y,x,i)}\quad\text{ and }\quad
d_{\overline{U(y,x,i)}}=\lambda^{2}d_{U(y,x,i)}$

Therefore $\overline{U(y,x,i)}=\lambda U(y,x,i)$.
Using the latter relationship, we get, for any $x,y\in\\{r,c\\}$,
$i\in\\{1,2\\}$:

$\begin{split}F_{\overline{U(y,x,i)}}(0)&={\mathcal{P}}\boldsymbol{\left[\right.}\overline{U(y,x,i)}\leq
0\boldsymbol{\left.\right]}={\mathcal{P}}\boldsymbol{\left[\right.}\lambda\cdot
U(y,x,i)\leq
0\boldsymbol{\left.\right]}={\mathcal{P}}\boldsymbol{\left[\right.}U(y,x,i)\leq
0\boldsymbol{\left.\right]}=F_{U(y,x,i)}(0)\end{split}$

To simplify the equations in the following, let us set, for any
$x\in\\{r,c\\}$, $i\in\\{1,2\\}$:
$U_{i}=U(x,\bar{x},1)$, $\overline{U}_{i}=\overline{U(x,\bar{x},1)}$, and let
$f_{i},\overline{f}_{i}$ the respective cdfs for $U_{i},\overline{U}_{i}$.
Then, using Lemma 1, and the above notation, for any
$\omega_{1},\omega_{2}\in\mathbb{R}$ such that $0\leq\omega_{1}<\omega_{2}\leq
1$, it holds that:

$\begin{split}&\int_{0}^{+\infty}\left(\int_{\frac{\omega_{1}-1}{\omega_{1}}u_{2}}^{\frac{\omega_{2}-1}{\omega_{2}}u_{2}}\\!f_{\overline{U(x,\bar{x},1)}}(u_{1})\,\mathrm{d}u_{1}\right)\frac{f_{\overline{U(x,\bar{x},2)}}(u_{2})}{u_{2}}\,\mathrm{d}u_{2}\\\
&\hskip
56.9055pt=\int_{0}^{+\infty}\left(\int_{\frac{\omega_{1}-1}{\omega_{1}}u_{2}}^{\frac{\omega_{2}-1}{\omega_{2}}u_{2}}\\!\overline{f}_{1}(u_{1})\,\mathrm{d}u_{1}\right)\frac{\overline{f}_{2}(u_{2})}{u_{2}}\,\mathrm{d}u_{2}\\\
&\hskip
56.9055pt={\mathcal{P}}\boldsymbol{\left[\right.}\frac{\omega_{1}-1}{\omega_{1}}\leq\frac{\overline{U}_{1}}{\overline{U}_{2}}\leq\frac{\omega_{1}-1}{\omega_{1}},\overline{U}_{1}<0,\overline{U}_{2}>0\boldsymbol{\left.\right]}\\\
&\hskip
56.9055pt={\mathcal{P}}\boldsymbol{\left[\right.}\frac{\omega_{1}-1}{\omega_{1}}\leq\frac{\lambda\cdot
U_{1}}{\lambda\cdot U_{2}}\leq\frac{\omega_{1}-1}{\omega_{1}},\lambda\cdot
U_{1}<0,\lambda\cdot U_{2}>0\boldsymbol{\left.\right]}\\\ &\hskip
56.9055pt={\mathcal{P}}\boldsymbol{\left[\right.}\frac{\omega_{1}-1}{\omega_{1}}\leq\frac{U_{1}}{U_{2}}\leq\frac{\omega_{1}-1}{\omega_{1}},U_{1}<0,U_{2}>0\boldsymbol{\left.\right]}\\\
&\hskip
56.9055pt=\int_{0}^{+\infty}\left(\int_{\frac{\omega_{1}-1}{\omega_{1}}u_{2}}^{\frac{\omega_{2}-1}{\omega_{2}}u_{2}}\\!f_{1}(u_{1})\,\mathrm{d}u_{1}\right)\frac{f_{2}(u_{2})}{u_{2}}\,\mathrm{d}u_{2}\\\
&\hskip
56.9055pt=\int_{0}^{+\infty}\left(\int_{\frac{\omega_{1}-1}{\omega_{1}}u_{2}}^{\frac{\omega_{2}-1}{\omega_{2}}u_{2}}\\!f_{U(x,\bar{x},1)}(u_{1})\,\mathrm{d}u_{1}\right)\frac{f_{U(x,\bar{x},2)}(u_{2})}{u_{2}}\,\mathrm{d}u_{2}\end{split}$

Analogously, it can be shown that:

$\begin{split}&\int_{-\infty}^{0}\left(\int_{\frac{\omega_{1}-1}{\omega_{1}}u_{2}}^{\frac{\omega_{2}-1}{\omega_{2}}u_{2}}\\!f_{U(x,\bar{x},1)}(u_{1})\,\mathrm{d}u_{1}\right)\frac{f_{U(x,\bar{x},2)}(u_{2})}{u_{2}}\,\mathrm{d}u_{2}=\\\
&\hskip
85.35826pt\int_{-\infty}^{0}\left(\int_{\frac{\omega_{1}-1}{\omega_{1}}u_{2}}^{\frac{\omega_{2}-1}{\omega_{2}}u_{2}}\\!f_{\overline{U(x,\bar{x},1)}}(u_{1})\,\mathrm{d}u_{1}\right)\frac{f_{\overline{U(x,\bar{x},2)}}(u_{2})}{u_{2}}\,\mathrm{d}u_{2}\end{split}$

From the above equations, it is obvious that the respective probabilities in
Table 4 for $mG$ and $\overline{mG}$ are equal. Moreover, since
$\overline{G^{0}}=\lambda\cdot G^{0}$, it follows that the Nash equilibria of
$G^{0}$ and $\overline{G^{0}}$ are the same. Combining these facts with Table
5 and Theorems 8, 9, the result follows. $\Box$

## References

  * [1] Michele Aghassi and Dimitris Bertsimas.  Robust game theory.  Math. Program., 107(1-2):231–273, 2006.
  * [2] Shiryayev A.N.  Mathematical Foundations of Probability Theory.  Springer, New York, NY, 1984.
  * [3] David Avis, Gabriel Rosenberg, Rahul Savani, and Bernhard von Stengel.  Enumeration of nash equilibria for two-player games.  Economic Theory, 42:9–37, 2010.
  * [4] Maria-Florina Balcan, Avrim Blum, and Yishay Mansour.  The price of uncertainty.  In Proceedings of the 10th ACM Conference on Electronic Commerce (EC), 2009.
  * [5] Maria-Florina Balcan and Mark Braverman.  Nash equilibria in perturbation-stable games.  Theory of Computing, 13(1):1–31, 2017.
  * [6] Imre Bárány, Santosh S. Vempala, and Adrian Vetta.  Nash equilibria in random games.  Random Structures and Algorithms, 31:391–405, 2007.
  * [7] Peter G. Bennett.  Hypergames: Developing a model of conflict.  Futures, 12(6):489–507, 1980.
  * [8] Philip N. Brown, Holly P. Borowski, and Jason R. Marden.  Are multiagent systems resilient to communication failures?  CoRR, abs/1710.08500, 2017.
  * [9] Constantinos Daskalakis, Alexandros G. Dimakis, and Elchanan Mossel.  Connectivity and equilibrium in random games.  CoRR, abs/math/0703902, 2007.
  * [10] Melvin Dresher.  Probability of a pure equilibrium point in n-person games.  Journal of Combinatorial Theory, Series A, 8:134–145, 1970.
  * [11] Elias Koutsoupias and Christos Papadimitriou.  Worst-case equilibria.  In Proceedings of the 16th annual conference on Theoretical aspects of Computer Science (STACS), pages 404–413, 1999.
  * [12] R. Duncan Luce and Howard Raiffa.  Games and Decisions: Introduction and Critical Survey.  John Wiley and Sons, New York, 1957.
  * [13] Reshef Meir and David C. Parkes.  Congestion games with distance-based strict uncertainty.  In Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, pages 986–992, 2015.
  * [14] Reshef Meir and David C. Parkes.  Playing the wrong game: Smoothness bounds for congestion games with behavioral biases.  SIGMETRICS Performance Evaluation Review, 43(3):67–70, 2015.
  * [15] Reshef Meir and David C. Parkes.  Playing the wrong game: Bounding externalities in diverse populations of agents.  In Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems (AAMAS), pages 86–94, 2018.
  * [16] John F. Nash.  Non-cooperative games.  The Annals of Mathematics, 54(2):286–295, 1951.
  * [17] Noam Nisan, Tim Roughgarden, Eva Tardos, and Vijay V. Vazirani.  Algorithmic Game Theory.  Cambridge University Press, USA, 2007.
  * [18] Martin J. Osborne and Ariel Rubinstein.  A Course in Game Theory, volume 1 of MIT Press Books.  The MIT Press, August 1994.
  * [19] Merkouris Papamichail, Constantinos Varsos, and Giorgos Flouris.  Implementing adaptation procedure in misinformation games.  12th EETN Conference on Artificial Intelligence, 2022.
  * [20] Matteo Quattropani and Marco Scarsini.  Efficiency of equilibria in random binary games.  CoRR, abs/2007.08518, 2020.
  * [21] Yosef Rinott and Marco Scarsini.  On the number of pure strategy nash equilibria in random games.  Games Econ. Behav., 33(2):274–293, 2000.
  * [22] Burkhard C. Schipper.  Unawareness - A gentle introduction to both the literature and the special issue.  Mathematical Social Sciences, 70:1–9, 2014.
  * [23] William Stanford.  The limit distribution of pure strategy nash equilibria in symmetric bimatrix games.  Math. Oper. Res., 21(3):726–733, 1996.
  * [24] Satoru Takahashi.  The number of pure nash equilibria in a random game with nondecreasing best responses.  Games Econ. Behav., 63(1):328–340, 2008.
  * [25] Constantinos Varsos, Giorgos Flouris, Marina Bitsaki, and Michail Fasoulakis.  A study of misinformation games.  Proceedings 18th Pacific Rim International Conference on Artificial Intelligence, 2021.
  * [26] Shmuel Zamir.  Bayesian Games: Games with Incomplete Information, pages 426–441.  Springer New York, New York, NY, 2009.