Few more lines

This commit is contained in:
Théophile Bastian 2016-07-19 23:26:19 +01:00
parent 7738081f2a
commit df1e931494

View file

@ -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 traditional approach of \emph{tree-like games} (``Player plays $A$, then
Opponent plays $B$, thus reaching the configuration $A \cdot B$''). Opponent plays $B$, thus reaching the configuration $A \cdot B$'').
\subsection{Informal approach}
\subsection{Event structures} \subsection{Event structures}
\begin{definition}[event structure] \begin{definition}[event structure]
@ -67,13 +69,18 @@ game.
The consistency relation is often replaced by a weaker \emph{conflict} binary The consistency relation is often replaced by a weaker \emph{conflict} binary
relation $\confl$ indicating that two events cannot occur together. 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) 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 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. reduction of $\leq_E$; onto which the conflict relation is superimposed.
\begin{definition}[event structure with polarities] \begin{definition}[event structure with polarities]
An \emph{event structure with polarities} (\textit{ESP}) is an event 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. function associating a \emph{polarity} to each event.
\end{definition} \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. Player or Opponent.
\begin{definition}[configuration] \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, that is \emph{down-closed}, \ie{} $\forall x \in X, \forall e \in E_A,
e \leq_A x \implies e \in X$. 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 dependency relation is imposed by the games' rules, one can only make one of
its moves depend on an Opponent move. 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} \section{Implementation of deterministic concurrent games}