diff --git a/report.tex b/report.tex index c0c41f7..d8bbfa4 100644 --- a/report.tex +++ b/report.tex @@ -46,6 +46,8 @@ structures} formalism to describe concurrent games, instead of the more traditional approach of \emph{tree-like games} (``Player plays $A$, then Opponent plays $B$, thus reaching the configuration $A \cdot B$''). +\subsection{Informal approach} + \subsection{Event structures} \begin{definition}[event structure] @@ -67,13 +69,18 @@ game. The consistency relation is often replaced by a weaker \emph{conflict} binary relation $\confl$ indicating that two events cannot occur together. +During this internship, my work was essentially carried on event structures +without conflicts. Thus, the consistency set is not relevant and will be +omitted in what follows, but one can refer to~\cite{castellan2016concurrent} +for the corresponding constructions with consistency sets. + Event structures are often represented as a directed acyclic graph (DAG) where the vertices are the elements of $E$ and the edges are the transitive reduction of $\leq_E$; onto which the conflict relation is superimposed. \begin{definition}[event structure with polarities] An \emph{event structure with polarities} (\textit{ESP}) is an event - structure $(E, \leq_E, \con_E, \rho)$, where $\rho : E \to \set{+,-}$ is a + structure $(E, \leq_E, \rho)$, where $\rho : E \to \set{+,-}$ is a function associating a \emph{polarity} to each event. \end{definition} @@ -81,7 +88,7 @@ In games theory, this is used to represent whether a move is to be played by Player or Opponent. \begin{definition}[configuration] - A \emph{configuration} of an ESP $A$ is a subset $X \subseteq \con_A$ + A \emph{configuration} of an ESP $A$ is a subset $X \subseteq A$ that is \emph{down-closed}, \ie{} $\forall x \in X, \forall e \in E_A, e \leq_A x \implies e \in X$. @@ -177,6 +184,24 @@ play one of its moves, while~(\ref{def:courteous}) states that unless a dependency relation is imposed by the games' rules, one can only make one of its moves depend on an Opponent move. +\subsection{Operations on games and strategies} + +\todo{intro} + +In this whole section, $E$ and $F$ denotes ESPs, $A$ and $B$ denotes games, +$\sigma: S \to A$ and $\tau: T \to B$ denotes strategies. + +\begin{definition}[Parallel composition] + The \emph{parallel composition} $E \parallel F$ of two ESPs is an ESP + whose events are $\left(\set{0} \times E\right) \cup \left(\set{1} \times + F\right)$ (the disjoint tagged union of the events of $E$ and $F$), and + whose partial order is $\leq_E$ on $E$ and $\leq_F$ on $F$, with no + relation between elements of $E$ and $F$. + + One can then naturally expand this definition to games (by preserving + polarities) and to strategies. +\end{definition} + %%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Implementation of deterministic concurrent games}