Negotiation Games
Philipp Hoffmann \institute{Fakult\"at f\"{u
Negotiations, a model of concurrency with multi party negotiation as primitive, have been recently introduced in \cite{negI,negII. We initiate the study of games for this model. We study {\em coalition problems: can a given coalition of agents force that a negotiation terminates (resp. block the negotiation so that it goes on forever)?; can the coalition force a given outcome of the negotiation? We show that for arbitrary negotiations the problems are EXPTIME-complete. Then we show that for sound and deterministic or even weakly deterministic negotiations the problems can be solved in PTIME. Notice that the input of the problems is a negotiation, which can be exponentially more compact than its state space.
0-includes.tex
\usepackage{negotiations}

\usepackage{graphicx}

\usepackage{enumerate}

\usepackage{amsthm}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{definition}[theorem]{Definition}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}




%%%%%%%%%%%%%%%%%% reftheorem

\newtheorem{theoremDummy}{Theorem}
\newenvironment{reftheorem}[1]
{\renewcommand{\thetheoremDummy}{\ref{#1}}\begin{theoremDummy}}
{\end{theoremDummy}}

\newtheorem{corollaryDummy}{Theorem}
\newenvironment{refcorollary}[1]
{\renewcommand{\thetheoremDummy}{\ref{#1}}\begin{corollaryDummy}}
{\end{corollaryDummy}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\pagestyle{headings}
1-introduction.tex
\section{Introduction}

In \cite{negI,negII}, the first author and J\"org Desel have introduced 
a model of concurrency with multi party negotiation as primitive. The model
allows one to describe distributed negotiations obtained by combining
``atomic'' multi party negotiations, or \emph{atoms}. Each atom has a number 
of \emph{parties} (the subset of agents involved), and a set  
of possible outcomes. The parties agree on an outcome, which
determines for each party the subset of atoms 
it is ready to engage in next.

Ill-designed negotiations may deadlock, or may contains useless 
atoms, i.e., atoms that can never be executed. The problem whether a 
negotiation is well designed or \emph{sound} was studied in \cite{negI,negII}. 
The main result was the identification of two classes,
called deterministic and acyclic weakly deterministic negotiations, for which the 
soundness problem is tractable: while the problem is PSPACE-complete for arbitrary 
negotiations, it becomes polynomial for these two classes.

In this paper we start the study of games on negotiations. As for games
played on pushdown automata \cite{DBLP:journals/iandc/Walukiewicz01},
vector addition systems with states (VASS) \cite{DBLP:conf/icalp/BrazdilJK10}, counter
machines \cite{DBLP:conf/rp/Kucera12}, or
asynchronous automata \cite{DBLP:conf/fsttcs/MohalikW03}, games on negotiations
can be translated into games played on the (reachable part of the) 
state space. However, the number of states of a negotiation may grow exponentially 
in the number of agents, and so the state space can be exponentially 
larger than the negotiation. We explore the complexity of solving games 
\emph{in the size of the negotiation}, not on the size of the state space. 
In particular, we are interested in finding negotiation classes for which the 
winner can be decided in polynomial time, thus solving the state space explosion problem. 

We study games formalizing the two most interesting questions related to a 
negotiation. First, can a given \emph{coalition} (i.e., a given subset of agents) 
force termination of the negotiation? (Negotiations may contain cycles.) Second, 
can the coalition force a given final outcome?

Our first results show that these two problems are EXPTIME-complete in the 
size of the negotiation. This is the case even if the negotiation is 
deterministic, and so it seems as if the tractability results of 
\cite{negI,negII} cannot be extended to games. But then, we are able to show that, very 
surprisingly, the problems are polynomial for deterministic (or even weakly 
deterministic) negotiations \emph{that are sound}. This is very satisfactory: 
since unsound negotiations are ill-designed, we are not interested in them anyway.
And, very unexpectedly, the restriction to sound negotiations has as collateral effect a
dramatic improvement in the complexity of the problem. Moreover, 
the restriction comes ``at no cost'', because deciding soundness
of deterministic negotiations is also decidable in polynomial time.

The full version of this paper including the appendix is available on arXiv.org.

\paragraph*{Related work.}
Our games can be seen as special cases of concurrent games 
\cite{DBLP:journals/jacm/AlurHK02,DBLP:journals/tcs/AlfaroHK07} in which 
the arena is succinctly represented as a negotiation. Explicit construction of the 
arena and application of the algorithms of 
\cite{DBLP:journals/jacm/AlurHK02,DBLP:journals/tcs/AlfaroHK07} yields an exponential algorithm, 
while we provide a polynomial one. 

Negotiations have the same expressive power as 1-safe Petri nets or 1-safe VASS, 
although they can be exponentially more compact (see \cite{negI,negII}). Games for
unrestricted VASS have been studied in \cite{DBLP:conf/icalp/BrazdilJK10}. 
However, in \cite{DBLP:conf/icalp/BrazdilJK10} the emphasis is on VASS with an 
infinite state space, while we concentrate on the 1-safe case.

The papers closer to ours are those studying games on asynchronous automata
(see e.g. \cite{DBLP:conf/fsttcs/MohalikW03,DBLP:journals/fmsd/GastinSZ09,DBLP:conf/icalp/GenestGMW13}). Like negotiations, asynchronous automata are a model of distributed computation
with a finite state space. These papers study algorithms for deciding the existence of 
distributed strategies for a game, i.e., local strategies for each agent based only on 
the information the agent has on the global system. Our results identify a special case 
with much lower complexity than the general one, in which local strategies are even memoryless.

Finally, economists have studied mathematical models of negotiation games,
but with different goals and techniques (see e.g. \cite{rubinstein1982perfect}). 
In our terminology, they typically consider negotiations 
in which all agents participate in all atomic negotiations. We focus on distributed
negotiations, where in particular atomic negotiations involving disjoint sets
of agents may occur concurrently. 




2-definitions.tex
\section{Negotiations: Syntax and Semantics}
Negotiations are introduced in \cite{negI}. We recall the main definitions.
We fix a finite set $\agents$ of \emph{agents} representing potential parties 
of negotiations. In \cite{negI,negII} each agent has an associated set of 
internal states. For the purpose of this paper the internal states are irrelevant, and so we omit them. 

\smallskip
\noindent \textbf{Atoms.} A \emph{negotiation atom}, or just an \emph{atom}, is a pair
$n=(P_n, \outc_n)$, where $P_n \subseteq \agents$ is a nonempty set of \emph{parties}, 
and $\outc_n$ is a finite, nonempty set of \emph{outcomes}.

\smallskip
\noindent \textbf{(Distributed) Negotiations.} A distributed negotiation is
a set of atoms together with a \emph{transition function} $\trans$ that assigns to every 
triple $(n,a,r)$ consisting of an atom $n$, a party $a$ of $n$, and an outcome $r$ of $n$ a set 
$\trans(n,a,r)$ of atoms. Intuitively, this is the set of atomic negotiations 
agent $a$ is ready to engage in after the atom $n$, if the outcome of $n$ is $r$. 

Formally, given a finite set of atoms $N$, let $T(N)$ denote the set of triples $(n, a, r)$ such that $n \in N$, $a\in P_n$, and $r \in \outc_n$. 
A \emph{negotiation} is a tuple $\N=(N, n_0, n_f, \trans)$, where 
$n_0, n_f \in N$ are the \emph{initial} and \emph{final} atoms, and  
$\trans \colon T(N) \rightarrow 2^N$ is the \emph{transition function}. Further, 
$\N$ satisfies the following properties: 
(1) every agent of $\agents$ participates in both $n_0$ and $n_f$; 
(2) for every $(n, a, r) \in T(N)$: $\trans(n, a, r)= \emptyset$ if{}f $n=n_f$.

\begin{figure}[bth]
\centering
\scalebox{0.8}{
\input{tikz/FDM_acyclic}
\hspace{1cm}
\input{tikz/FDM_cyclic}
}
\caption{An acyclic and a cyclic negotiation.}
\label{fig:dneg}
\end{figure}

\noindent \textbf{Graphical representation.} Negotiations are graphically represented as shown in Figure \ref{fig:dneg}. 
For each atom $n \in N$ we draw a black bar; for each party $a$ of $P_n$ we 
draw a white circle on the bar, called a \emph{port}. For each $(n,a,r) \in T(N)$, 
we draw a hyper-arc leading from the port of $a$ in $n$ to all the ports of $a$ in 
the atoms of $\trans(n,a,r)$, and label it by $r$. 
Figure \ref{fig:dneg} shows two Father-Daughter-Mother negotiations. On the left,
Daughter and Father negotiate with possible outcomes \texttt{yes} ($\texttt{y}$), 
\texttt{no} ($\texttt{n}$),
and \texttt{ask\_mother} ($\texttt{am}$). If the outcome is the latter, then Daughter and Mother negotiate
with outcomes \texttt{yes}, \texttt{no}. In the negotiation on the right,
Father, Daughter and Mother negotiate with outcomes \texttt{yes} and \texttt{no}.
If the outcome is \texttt{yes}, then Father and Daughter negotiate a return time  
(atom $n_1$) and propose it to Mother (atom $n_2$). 
If Mother approves (outcome \texttt{yes}), then the negotiation terminates, 
otherwise (outcome \texttt{r}) Daughter and Father renegotiate the return time. 

\smallskip
\noindent \textbf{Semantics. } A \emph{marking} of a negotiation $\N=(N, n_0, n_f, \trans)$ is a mapping 
$\vx \colon \agents \rightarrow 2^N$. Intuitively, $\vx(a)$ is the set of atoms that agent $a$ is currently ready to engage in next. 
The \emph{initial} and \emph{final} markings,  denoted by $\vx_0$ and $\vx_f$ respectively, are given by $\vx_0(a)=\{n_0\}$ and 
$\vx_f(a)=\emptyset$ for every $a \in \agents$. 

A marking $\vx$ \emph{enables} an atom $n$ if $n \in \vx(a)$ for every $a \in P_n$,
i.e., if every party of $n$ is currently ready to engage in it.
If $\vx$ enables $n$, then $n$ can take place and its parties
agree on an outcome $r$; we say that $(n,r)$ \emph{occurs}.
Abusing language, we will call this pair also an outcome.
The occurrence of $(n,r)$ produces a next marking $\vx'$ given by $\vx'(a) = \trans(n,a,r)$ for every $a \in P_n$, 
and $\vx'(a)=\vx(a)$ for every $a \in \agents \setminus P_n$. 
We write $\vx \by{(n,r)} \vx'$ to denote this. 

By this definition, $\vx (a)$ is always either $\{n_0\}$ or equals 
$\trans(n,a,r)$ for some atom $n$ and outcome $r$. 
The marking $\vx_f$ can only be reached by the occurrence of 
$(n_f, r)$ ($r$ being a possible outcome of $n_f$), 
and it does not enable any atom. Any other marking that does not enable 
any atom is a \emph{deadlock}.

Reachable markings are graphically represented by placing tokens (black dots) on the forking points of the hyper-arcs (or in the middle of an arc). Figure \ref{fig:dneg} shows on the right a marking in which \texttt{F} and \texttt{D} are ready to engaging $n_1$ and \texttt{M} is ready to engage in $n_2$.

We write $\vx_1 \by{\sigma}$ to denote that there is a sequence 
\begin{equation*}
\vx_1 \by{(n_1,r_1)} \vx_2 \by{(n_2,r_2)}\cdots \by{(n_{k-1},r_{k-1})} \vx_{k} \by{(n_k,r_k)} \vx_{k+1} \cdots
\end{equation*}
such that  $\sigma = (n_1, r_1) \ldots (n_{k}, r_{k}) \ldots$. If
$\vx_1 \by{\sigma}$, then $\sigma$ is an \emph{occurrence sequence} from the marking $\vx_1$, and $\vx_1$ enables $\sigma$.
If $\sigma$ is finite, then we write
$\vx_1 \by{\sigma} \vx_{k+1}$ and say that $\vx_{k+1}$ is \emph{reachable} from $\vx_1$. 

\smallskip
\noindent \textbf{Soundness. } A negotiation is \emph{sound} if \emph{(a)} every atom is enabled at some reachable marking, and \emph{(b)} every occurrence sequence from the initial marking 
either leads to the final marking $\vx_f$, or can be extended to an
occurrence sequence that leads to $\vx_f$.  

The negotiations of Figure \ref{fig:dneg} are sound. However, if we set in the left negotiation
$\trans(n_0,\texttt{M}, \texttt{st})= \{n_2\}$ instead of $\trans(n_0,\texttt{M}, \texttt{st})= \{n_2, n_f\}$, then the occurrence sequence $(n_0,\texttt{st}) (n_1, \texttt{yes})$
leads to a deadlock.

\smallskip
\noindent \textbf{Determinism and weak determinism. } An agent $a \in \agents$ is \emph{deterministic} if for every $(n,a,r) \in T(N)$ such that $n \neq n_f$ there exists an atom
$n'$ such that $\trans(n,a,r) = \{n'\}$. 
    
The negotiation $\N$  is \emph{weakly deterministic} if for every $(n,a,r) \in T(N)$ there is a deterministic
agent $b$ that is a party of every atom in $\trans(n,a,r)$, i.e., $b \in P_{n'}$ for every $n' \in \trans(n,a,r)$.
In particular, every reachable atom has a deterministic party.
It is \emph{deterministic} if all its agents are deterministic.

Graphically, an agent $a$ is deterministic if no proper hyper-arc leaves any port 
of $a$, and a negotiation is deterministic if there are no proper hyper-arcs.
The negotiation on the left of Figure \ref{fig:dneg} is not deterministic (it contains a proper hyper-arc for Mother), while the one on the right is deterministic. 

3-parties.tex
\section{Games on Negotiations}
\label{sec:games}

We study a setting that includes, as a special case, the questions about coalitions mentioned
in the introduction: Can a given coalition (subset of agents) force termination of the negotiation?
Can the coalition force a given concluding outcome?

In many negotiations, there are reachable markings that enable more than one atom. If two of those atoms share an agent, the occurrence of one might disable the other and they are not truly concurrent. For a game where we want to allow concurrent moves, we formalize this concept with the notion of an independent set of atoms.

\begin{definition}
A set of atoms $S$ is independent if no two distinct atoms of $S$ share an agent, i.e., $P_n \cap P_{n'} = \emptyset$
for every $n, n' \in S$, $n \neq n'$.
\end{definition}
It follows immediately from the semantics that if a marking $\vx$ enables all atoms of $S$ and we fix an outcome $\r_i$ for each $n_i \in S$,
then there is a unique marking $\vx'$ such that $\vx \by{\sigma} \vx'$ for every 
sequence $\sigma = (n_1,\r_1) \ldots (n_k,\r_k)$ such that each atom of $S$ appears exactly once in
$\sigma$. In other words, $\vx'$ depends only on the outcomes of the atoms, and not on the order in
which they occur.

A \emph{negotiation arena} is a negotiation whose set $N$ of atoms 
is partitioned into two sets $N_1$ and $N_2$. We consider  
concurrent games \cite{DBLP:journals/jacm/AlurHK02,DBLP:journals/tcs/AlfaroHK07} with three 
players called Player 1, Player 2, and Scheduler. At each step, Scheduler chooses a nonempty set
of independent atoms among the atoms enabled at the current marking of the negotiation arena. 
Then, Player 1 and Player 2, independently of each other, select an outcome 
for each atom in $S\cap N_1$ and $S\cap N_2$, respectively. Finally, 
these outcomes occur in any order, and the game moves to the unique marking 
$\vx'$ mentioned above. The game terminates if it reaches a marking enabling no atoms,
otherwise it continues forever. 

Formally, a partial play is a sequence of tuples $(S_i, F_{i,1}, F_{i,2})$ 
where each $S_i \subseteq N$ is a set of independent atoms and $F_{i,j}$ assigns to every 
$n \in S_i\cap N_j$ an outcome $\r \in R_n$. Furthermore it must hold that every atom $n \in S_i$ 
is enabled after all atoms in $S_0,...,S_{i-1}$ have occurred with the outcomes specified by $F_{0,1}, F_{0,2},...,F_{i-1,1}, F_{i-1,2}$. 
A play is a partial play that is either infinite or reaches a marking enabling no atoms.
For a play $\pi$ we denote by $\pi_i$ the partial play consisting of the first $i$ tuples of $\pi$.

We consider two different winning conditions. In the \emph{termination game}, 
Player 1 wins a play if the play ends with $n_f$ occurring, otherwise Player 2 wins. In the \emph{concluding-outcome game},
we select for each agent $a$ a set of outcomes $G_a$ such that $n_f \in \trans(n,a,r)$ for $r \in G_a$ (that is, after any outcome $\r \in G_a$, agent $a$ is ready to terminate). Player 1 wins if the the play ends with $n_f$ occurring, and for each agent $a$ the last outcome $(n, \r)$ of the play such that $a$ is a party of $n$ belongs to $G_a$. 

A strategy $\sigma$ for Player $j, j\in\{1, 2\}$ is a partial function that, given a partial play 
$\pi = (S_0, F_{0,1},F_{0,2}),..,$ $(S_i, F_{i,1},F_{i,2})$ and a set of atoms $S_{i+1}$ returns 
a function $F_{i+1,j}$ 
according to the constraints above. A play $\pi$ is said to be played according to a 
strategy $\sigma$ of Player $j$ 
if for all $i$, $\sigma(\pi_i, S_{i+1}) = F_{i+1,j}$. A strategy $\sigma$ is a winning 
strategy for Player $j$ if he 
wins every play that is played according to $\sigma$. Player $j$ is said to win
 the game if he has a winning strategy. Notice that if Player 1 has a winning strategy 
then he wins every play against any pair of strategies for Player 2 and Scheduler. 

\begin{definition}
Let $\N$ be a negotiation arena.
The termination (resp. concluding-outcome) problem for $\N$ consists of deciding whether Player 1 has a winning strategy for the termination game (concluding-outcome game).
\end{definition}

\begin{figure}[h]
\centering
\scalebox{1.1}{
\input{tikz/FDDM.tex}
}
\caption{Atom control and determinism}
\label{fddm}
\end{figure}

Assume we want to model the following situation: In a family with Father (F), Mother (M) and two Daughters (D$_1$ and D$_2$), Daughter D$_1$ wants to go to a party. She can talk to each parent individually, but can choose beforehand whether to take her sister D$_2$ with her or not. Figure \ref{fddm} models this negotiation. 
The solid edges for the daughters between $n_2$ and $n_3$ and
between $n_4$ and $n_5$ ``ask the other parent'' outcomes, while the dashed edges 
represent the ``yes'' and ``no'' outcomes. Assume the daughters work together to reach termination.
Then in $N_1 = \{ n_1, n_2, n_3 \}$ the daughters have 
a majority which we will interpret as ``they can choose which outcome is taken''. Can the daughters force termination?

At atom $n_1$ the daughters decide whether D$_2$ should participate in the conversation with the parents (outcome \texttt{t}) or not (outcome \texttt{s}). 
If the daughters choose outcome \texttt{s},
then Father and Mother can force an infinite loop between $n_4$ and $n_5$. On the contrary, if the daughters choose to stay together, then, 
since they control atom $n_2$, they can force a  ``yes'' or ``no'' outcome, and therefore termination. 

The questions whether a coalition ${\cal C}$ of agents can force termination or a 
certain outcome are special instances of the termination and concluding-outcome problems. 
In these instances, an atom $n$ belongs to $N_1$---the set 
of atoms controlled by Player 1--- if{}f a strict majority of the agents of $n$ 
are members of ${\cal C}$. 

\subsection{Coalitions}

Before we turn to the termination and concluding-outcome problems, we briefly study coalitions. Intuitively, a coalition controls all the atoms where it has strict majority. We show that while the definition of the partition of the atoms $N$ according to the participating agents may seem restricting, this is not the case: In all cases but the deterministic sound case, any partition can be reached, possibly by adding agents.

We define the partition of $N$ via a partition of the agents: Let the agents $A$ be partitioned into two sets $A_1$ and $A_2$. Define $N_1 = \{ n \in N : |P_n \cap A_1| > |P_n \cap A_2|\}$, $N_2 = N \backslash N_1$. Note that ties are controlled by $A_2$.

We first show that in the nondeterministic and weakly deterministic case, this definition is equivalent to one where we decide control for each atom and not for each agent.

\begin{figure}[h]
\centering
\scalebox{0.8}{
\input{tikz/det_control.tex}
\input{tikz/ndet_control.tex}
\input{tikz/ndet_control2.tex}
}
\caption{Atom control via additional agents}
\label{fig:control}
\end{figure}

Consider the example given in Figure \ref{fig:control}. On the left a deterministic negotiation with two agents is given. Assume the coalitions are $A_1 = \{A\}$ and $A_2 = \{B\}$. By the definition above, $N_2 = N$, thus coalition $A_2$ controls every atom. We want to change control of $n_1$ so that $A_1$ controls $n_1$, changing the negotiation to a weakly deterministic one on the way. We add an additional agent $a$ that participates in $n_0, n_1, n_f$ as shown in Figure \ref{fig:control} in the middle and set $A_1 = \{A,a\}$. Now $A_1$ controls $n_1$ but also $n_0$ and $n_f$. We therefore add another agent $b$ that participates in $n_0,n_f$ as shown in Figure \ref{fig:control} on the right. Now the partition of atoms is exactly $N_1 = \{n_1\}$ and $N_2 = \{n_0,n_2,n_f\}$, as desired.
In general, by adding nondeterministic agents to the negotiation, we can change the control for each atom individually. For each atom $n$ whose control we wish to change, we add a number of agents to that atom, the initial atom $n_0$ and final atom $n_f$. We add nondeterministic edges for these agent from $n_0$ to $\{n, n_f\}$ for each outcome of $n_0$ and from  $n$ to $\{n, n_f\}$ for each outcome of $n$. It may be necessary to add more agents to $n_0$ that move to $n_f$ in order to preserve the control of $n_0$ or $n_f$. This procedure changes the control of $n$ while preserving soundness and weak determinism.

We proceed by showing that in the deterministic case, we cannot generate any atom control by adding more agents. 


\begin{lemma}
We cannot add deterministic agents to the negotiation on the loft of Figure \ref{fig:control} in a manner, such that soundness is preserved and Player 1 controls $n_1$, Player 2 controls $n_2$.
\end{lemma}

\begin{proof}
Consider again the deterministic negotiation game on the left of Figure \ref{fig:control}. Assume we have added deterministic agents such that Player 1 controls $n_1$. After the occurring sequence $\vx_0 \by{(n_0,\text{a})} \vx_1 \by{(n_1,\text{a})} \vx_2$, those additional agents have moved deterministically, either to $n_1$ or $n_f$. \footnote{Moving to $n_2$ would change the control there, thus additional agents have to be added to $n_2$, we then can use a similar argument as follows by exchanging the roles of $n_1$ and $n_2$.} 

If any agent remains in $n_1$, choosing outcome $b$ in $n_2$ leads to a deadlock, otherwise, choosing $a$ leads to a deadlock. Thus the negotiation is no longer sound.
\end{proof}


4-reduction.tex
\section{The Termination Problem}
\label{sec:complexity}

We turn to the general complexity of the problem. It is easy to see that
the termination problem can be solved in exponential time.

\begin{theorem}
\label{thm:membership}
The termination problem is in EXPTIME.
\end{theorem}
\begin{proof}
Sketch. (See the appendix for details.) We construct a concurrent reachability 
game on a graph such that Player 1 wins the negotiation game if{}f she wins this new game. 
The game has single exponential size in the size of the negotiation arena.  

The nodes of the graph are either
markings $\vx$ of the negotiation, or pairs $(\vx, N_{\vx})$, where $\vx$ is a marking
and $N_{\vx}$ is an independent set of atoms enabled at $\vx$. Nodes $\vx$ belong to Scheduler,
who chooses a set $N_{\vx}$, after which the play moves to $(\vx, N_{\vx})$. At nodes 
$(\vx, N_{\vx})$ Players 1 and 2 concurrently select outcomes for their atoms in $N_{\vx}$, and depending
on their choice the play moves to a new marking. Player 1 wins if the play reaches the 
final marking $\vx_f$. Since the winner of a concurrent game with reachability objectives
played on a graph can be determined in polynomial time (see e.g. \cite{DBLP:journals/jacm/AlurHK02}), 
the result follows.
\end{proof}

Unfortunately, there is a matching lower bound.

\begin{theorem}
\label{thm:hard}
The termination problem is EXPTIME-hard even for negotiations 
in which every reachable marking enables at most one atom.
\end{theorem}
\begin{proof}
Sketch. (See the appendix for details.)
The proof is by reduction from the acceptance problem 
for alternating, linearly-bounded Turing machines (TM)\cite{DBLP:journals/jacm/ChandraKS81}. Let 
$M$ be such a TM with transition relation $\delta$, and let $x$ be an input of length $n$. 

We define a negotiation with an agent $I$ modeling the internal state of $M$,
an agent $P$ modeling the position of the head, and one agent $C_i$ 
for each $1 \leq i \leq n$ modeling the $i$-th cell of the tape. 
The set of atoms contains one atom $n_{q,\alpha,k}$ for each triple 
$(q, \alpha, k)$, where $q$ is a state of $M$, $k$ is the current position of the 
head, and $\alpha$ is the current symbol in the $k$-th tape cell. 

The parties of the atom $n_{q, \alpha, k}$ are $I$, $P$ and $C_k$, in particular,
 $I$ and $P$ are agents of all atoms.
The atom $n_{q, \alpha, k}$ has one outcome 
$\r_\tau$ for each element $\tau \in \delta(q,\alpha)$, where $\tau$ 
is a triple consisting of a new state, a new tape symbol, and a direction 
for the head. We informally define the function $\trans(n_{q, \alpha, k},C_k, \r_\tau)$ 
by means of an example. Assume that, for 
instance, $\tau = (q', \beta, R)$, i.e., at control state $q$ and with the head reading 
$\alpha$, the machine can go to control state $q'$, write $\beta$, and move the head to 
the right. Then we have:  (i) $\trans(n_{q, \alpha, k},I,\r_\tau)$ contains all atoms of the form
$n_{q', \_, \_}$ (where $\_$ stands for a wildcard); (ii) $\trans(n_{q, \alpha, k},P,\r)$ 
contains the atoms $n_{\_, \_, k+1}$; and (iii) $\trans(n_{q, \alpha, k},C_k,\r_\tau)$ 
contains all atoms $n_{\_, \beta, \_}$. If atom $n_{q, \alpha, k}$ is 
the only one enabled and the outcome $\r_\tau$ occurs, then clearly in the new marking
the only atom enabled is $n_{q', \beta, k+1}$. So every reachable marking enables at most one atom.

Finally, the negotiation also has an initial atom that, loosely speaking, takes care of modeling the initial configuration.

The partition of the atoms is: an atom $n_{q, \alpha, k}$ belongs to $N_1$ if
$q$ is an existential state of $M$, and to $N_2$ if it is universal. It is easy to see that $M$ accepts $x$
if{}f Player 1 has a winning strategy.
\end{proof}

Notice that if no reachable marking enables two or more atoms, 
Scheduler never has any choice. Therefore, the termination problem is EXPTIME-hard
even if the strategy for Scheduler is fixed. 

A look at points (i)-(iii) in the proof sketch of this theorem shows that 
the negotiations obtained by the reduction are highly nondeterministic. 
In principle we could expect a lower complexity in the deterministic case.
However, this is not the case.

\begin{theorem}
\label{thm:hard2}
The termination problem is EXPTIME-hard even for deterministic negotiations 
in which every reachable marking enables at most one atom.
\end{theorem}
\begin{proof}
Sketch. (See the appendix for details.) We modify the 
construction of Theorem \ref{thm:hard} so that it yields 
a deterministic negotiation. The old construction has an atom
$n_{q, \alpha, k}$ for each state $q$, tape symbol $\alpha$, 
and cell index $k$, with $I$, $P$, and $C_k$ as parties. 

The new construction adds atoms $n_{q, k}$, with $I$ and $P$ as parties,
and $n_{\alpha, k}$, with $P$ and $C_k$ as parties. Atoms $n_{q, k}$ have an outcome 
for each tape symbol $\alpha$, and atoms $n_{\alpha, k}$ have an outcome for each state $q$. 
New atoms are controlled by Player 1. 

In the new construction, after the outcome of $n_{q, \alpha, k}$ for transition 
$(q',\beta,R) \in \delta(q,\alpha)$, agent $C_k$ moves to $n_{\beta, k}$, and agents 
$I$ and $P$ move to $n_{q', k+1}$. Intuitively, $C_k$ waits for the head to return to cell $k$, 
while agents $I$ and $P$ proceed. Atom $n_{q', k+1}$ has an outcome for every tape symbol $\gamma$. 
Intuitively, at this atom Player 1 guesses the current tape symbol in cell $k+1$;
the winning strategy corresponds to guessing right. After guessing, say, symbol $\gamma$,
agent $I$ moves directly to $n_{q',\gamma, k+1}$, while $P$ moves to $n_{\gamma, k+1}$.
Atom $n_{\gamma, k+1}$ has one outcome for every state of $M$. Intuitively, Player 1 now
guesses the current control state $q'$, after which both $P$ and  $C_{k+1}$ 
move to $n_{q',\gamma, k+1}$. Notice that all moves are now deterministic. 

If Player 1 follows the winning strategy, then the plays mimic those of the old construction:
a step like $(n_{q, \alpha, k}, (q',\beta,R))$ in the old construction, played when the current symbol
in cell $k+1$ is $\gamma$, is mimicked by a sequence 
$(n_{q, \alpha, k}, (q',\beta,R))$ $(n_{q',k+1}, \gamma)$ $(n_{\gamma, k+1}, q')$ of moves
in the new construction.

\end{proof}

5-poly.tex
\section{Termination in Sound Deterministic Negotiations}
\label{sec:soundDet}

In \cite{negI,negII} it was shown that the soundness problem 
(deciding whether a negotiation is sound) can be solved in polynomial time 
for deterministic negotiations and
acyclic, weakly deterministic negotiations (the case of cyclic weakly 
deterministic negotiations is open), while the problem is PSPACE-complete for
arbitrary negotiations. Apparently, Theorem \ref{thm:hard2} proves that 
the tractability of deter\-mi\-nis\-tic negotiations stops at game problems. 
We show that this is not the case. Well-designed negotiations are sound, 
since otherwise they contain atoms that can never occur (and can therefore be removed),
or a deadlock is reachable. Therefore, we are only interested
in the termination problem for sound negotiations. We prove that for sound deterministic negotiations
(in fact, even for the larger class of weakly deterministic type 2 negotiations) the 
termination and concluding-outcome problems are solvable in polynomial time. For this, we show that the 
well-known attractor construction for reachability games played on graphs as arenas can be ``lifted'' 
to sound and weakly deterministic type 2 negotiation arenas.

\begin{definition}
Let $\N$ be a negotiation arena with a set of atoms $N=N_1 \cup N_2$. Given $n \in N$, let $P_{n,det}$ 
be the set of deterministic agents participating in $n$.

The attractor of the final atom $n_f$ is $\mathcal{A} = \bigcup\limits_{k=0}^\infty \mathcal{A}_{k}$, where $\mathcal{A}_{0}  =  \{ n_f \}$ and 
\begin{equation*}
\begin{array}[t]{rl} 
\mathcal{A}_{k+1}  =  \mathcal{A}_{k} \;
 \cup & \{ n \in N_1 : \exists \r \in R_n \forall a \in P_{n,det} : \; \mathcal{X}(n,a,\r) \in \mathcal{A}_{k} \} \\
 \cup & \{ n \in N_2 : \forall \r \in R_n \forall a \in P_{n,det}: \; \mathcal{X}(n,a,\r) \in \mathcal{A}_{k}\}
\end{array}
\end{equation*}

Given a marking $\vx \neq \vx_f$ of $\N$ and a deterministic agent $a$, 
the attractor position of $a$ at $\vx$ is the smallest $k$ such that 
$\vx(a) \in \mathcal{A}_k$, or $\infty$ if $\vx(a) \notin \mathcal{A}$. 
Let $a_1, \ldots, a_k$ be the deterministic agents of $\N$.
The (attractor) position vector of $\vx$ is the tuple $(p_1, ..., p_k)$ where $p_i$ is the attractor position of $a_i$.
\end{definition}

\begin{theorem}
\label{thm:attract}
Let $\N$ be a sound, weakly deterministic type 2 negotiation arena. Player 1 has a winning strategy in the 
termination game iff $n_0 \in \mathcal{A}$.
\end{theorem}
\begin{proof}
We start with an observation: If all deterministic agents are ready to take part in $n_f$, 
then $n_f$ and only $n_f$ is enabled. 
Indeed, since deterministic agents are only ready to engage in at most one atom, the only atom
with a deterministic party that can be enabled is $n_f$. Moreover, by weak determinism type 2 every atom has 
a deterministic party, and so no atom other than $n_f$ can be enabled. Finally, by soundness at least
one atom is enabled, and so $n_f$ is the only enabled atom. 

\noindent ($\Leftarrow)$: Assume that $n_0 \in \mathcal{A}$. We fix the \emph{attractor strategy} for Player 1.
We define the attractor index of an atom $n \in \mathcal{A}$ as the smallest $k$ such that 
$n \in \mathcal{A}_k$. The strategy for an atom $n \in N_1 \cap \mathcal{A}$ 
is to choose any outcome such that all deterministic parties of $n$ move to an atom 
of smaller attractor index; formally, we choose any outcome $\r$ such that 
for every deterministic party $a$ the singular atom in $\trans(n,a,\r)$ has smaller attractor index than $n$. 
Such an outcome exists by construction of $\mathcal{A}$. For atoms $n \in N_1 \setminus \mathcal{A}$ 
we choose an arbitrary atom. Notice that this strategy is not only memoryless,
but also independent of the current marking. 

We show that the attractor strategy is winning. By the definition of the game, 
we have to prove that every play following the strategy ends with $n_f$ occurring.
By the observation above, it suffices to prove that the play reaches a marking at which
every deterministic agent is ready to engage in $n_f$. 

Assume there is a play $\pi$ where Player 1 plays according to the attractor strategy, which 
never reaches such a marking. Then the play never reaches the final marking $\vx_f$ either.
We claim that at all markings reached along $\pi$, the deterministic agents are only
ready to engage in atoms of $\mathcal{A}$. We first observe that, initially, all deterministic agents 
are ready to engage in $n_0$, and $n_0 \in \mathcal{A}$. Now,
assume that in some marking reached along $\pi$ the deterministic agents are only
ready to engage in atoms of $\mathcal{A}$. Then, by weak determinism type 2, all enabled atoms
belong to $\mathcal{A}$, and therefore also the atoms chosen by Scheduler.
By the definition of $\mathcal{A}$, after an atom of $N_2 \cap \mathcal{A}$ occurs, the
deterministic agents are ready to engage in atoms of $\mathcal{A}$ only; by the definition
of the attractor strategy, the same holds for atoms of $N_1 \cap \mathcal{A}$. This concludes 
the proof of the claim.

Since all markings $\vx$ reached along $\pi$ satisfy $\vx \neq \vx_f$ and 
$\vx(a) \in \mathcal{A}$ for every deterministic agent $a$, they all
have an associated attractor position vector whose components are natural numbers.
Let $P_k$ denote the position vector of the marking reached after $k \geq 0$ steps
in $\pi$. Initially only the initial atom $n_0$ is enabled, and so 
$P_0 = (k_0, k_0, \ldots, k_0)$, where $k_0$ is the attractor position of $n_0$. 
We have $k_0 < |N|$, the number of atoms of the negotiation arena $\N$. 
Given two position vectors $P= (p_1, ..., p_k)$ and $P'=(p_1', ..., p_k')$, we say $P \prec P'$ if
$p_i \leq p_i'$ for every $1 \leq i \leq k$, and $p_i < p_i'$ for at least one $1 \leq i \leq k$.
By the definition of the attractor strategy, the sequence $P_0, P_1, ...$ of attractor positions 
satisfies $P_{i+1} \prec P_i$ for every $i$. Since $\prec$ is a well-founded order, 
the sequence is finite, i.e., the game terminates. By the definition of the game, it terminates
at a marking that does not enable any atom. Since, by assumption, 
the play never reaches the final marking $\vx_f$, this marking is a deadlock, which contradicts the 
soundness of $\N$.

\noindent ($\Rightarrow$): As this part is dual to part $\Leftarrow$, we only sketch the idea. The complete proof can be found in the appendix.

Let $\mathcal{B} = N \setminus  \mathcal{A}$, and 
assume $n_0 \in \mathcal{B}$. 
A winning strategy for Player 2 is to choose for an atom $n \in N_2 \cap \mathcal{B}$ any outcome $r$ such that at least one deterministic agent
moves to an atom not in $\mathcal{A}$. Such an outcome exists by construction of $\mathcal{A}$. For atoms in $N_2 \setminus \mathcal{B}$
we chose an arbitrary outcome.

This strategy achieves the following invariant: If at some marking $\vx$ reached along a play according to this strategy, there is a deterministic agent $a$ that satisfies $\vx(a)=n$ and $n \in \mathcal{B}$, then the same holds after one more step of the play. We then conclude that since $n_0 \in \mathcal{B}$ this invariant holds in every step of the play. Therefore $n_f$, in which all deterministic agents participate and which is not in $\mathcal{B}$, can never be enabled. Finally, because of soundness a play cannot end in a deadlock and thus every play will be of infinite length.
\end{proof}

\begin{corollary}
\label{cor:poly}
For the termination game over sound and weakly deterministic type 2 negotiations, the following holds:
\begin{enumerate}[(a)]
\item The game collapses to a two-player game.
\item Memoryless strategies suffice for both players.
\item The winner and the winning strategy can be computed in $O(|\outc| \ast |\agents|)$ time, where 
$A$ is the set of agents and $|\outc|$ the total number of outcomes of the negotiation.
\end{enumerate}
\end{corollary}

\begin{proof}
(a) and (b): The attractor computation and the strategies used in the proof of Theorem \ref{thm:attract} are independent of the choices of Scheduler; the strategies are memoryless. \\
(c) An algorithm achieving this complexity can be found in the appendix.
\end{proof}

We still have to consider the possibility that requiring soundness alone, without the addition of
weak determinism type 2, already reduces the complexity of the termination problem. The following theorem shows that this is not the case, and concludes our study. The proof is again an adaption of the reduction from turing machines and can be found in the appendix.

\begin{theorem}
\label{thm:hard3}
The termination problem is EXPTIME-hard for sound negotiation arenas.
\end{theorem}


\section{The Concluding-Outcome Problem}

We demonstrate that the algorithm can also be used to solve the concluding-outcome problem. Remember that for each agent $a$ we have selected a set $G_a$ of outcomes that lead to the final atom and that we want occur. The key idea is to modify the negotiation in the following way: We add two atoms per agent, say \emph{good$_a$} and \emph{bad$_a$}, and redirect the outcomes of that agent that lead to the final atom to \emph{good$_a$} if they are in $G_a$ and to \emph{bad$_a$} otherwise. We illustrate this approach by example.

We slightly change the setting of Father, Mother and two Daughters such that both daughters want to go to the party. In the negotiation, that results in two additional atoms where D$_2$ talks alone with each parent. Figure \ref{extFDDM} shows the new negotiation omitting all edges of father and mother to simplify the representation. They both have a nondeterministic edge from each of their ports leading to all of their respective ports.

Imagine the goal 
of Daughter D$_1$ is to get a ``yes'' answer for herself, but a `no'' answer for D$_2$,
who always spoils the fun. Will a coalition with one parent suffice to achieve the goal?
To answer this question, we modify the negotiation before applying the construction as shown in 
Figure \ref{extFDDM}. We introduce dummy atoms \emph{good$_i$} and \emph{bad$_i$} for each Daughter $i$, and
we redirect ``yes'' transitions leading to $n_f$ to \emph{good$_1$} and \emph{bad$_2$} (these transitions are represented as dashed lines), analogously we redirect ``no'' transitions to \emph{bad$_1$} and \emph{good$_2$} (represented as dotted lines).

We apply the algorithm with a slight alteration: Instead of starting from $n_f$, we initially add all newly introduced good atoms to the attractor.
Applying the algorithm for the coalition Father-D$_1$ 
yields $\{$\emph{good$_1$},\emph{bad$_2$},$n_4\}$ as attractor; for Mother-D$_1$
we get $\{$\emph{good$_1$},\emph{bad$_2$},$n_5\}$. So neither parent has enough influence to 
achieve the desired outcome.

\begin{figure}
\centering
\scalebox{0.8}{
\input{tikz/FDDM_extended.tex}
}
\caption{Applying the algorithm to the final-outcome problem. Father and mother edges omitted.}
\label{extFDDM}
\end{figure}


6-conclusion.tex
\section{Conclusions and Related Work}

We have started the study of games in the negotiation model 
introduced in \cite{negI,negII}. Our results confirm the low computational complexity 
of deterministic negotiations, however with an important twist: while even 
the simplest games are EXPTIME-hard for arbitrary deterministic negotiations, they become polynomial in the  \emph{sound} case. So soundness, a necessary feature of a well designed negotiation, also turns out to have a drastic beneficial effect on the complexity of the games.

We have shown that our games are also polynomial for sound and weakly deterministic negotiations. However, the complexity of deciding soundness for this case is unknown. We conjecture that it is also polynomial, as for the deterministic case. 

The objectives we have considered so far are qualitative: Either a coalition can reach termination or not, either it can enforce a concluding outcome or not. A possibility for future studies would be to look at quantitative objectives.

We have only considered 2-player games, since in our settings the behavior of the third player (the Scheduler) is either irrelevant, or is controlled by one of the other two players. We intend to study the extension to a proper 3-player game, or to a multi player game. Combined with qualitative objectives, this allows for multiple interesting questions: Which coalition of three agents can reach the best payoff? Which two agents should a given agent side with to maximize his payoff? Are there ``stable'' coalitions, that means, no agents can change to the opposing coalition and improve his payoff?


eptcsdata.tex
\providecommand{\firstpage}{31}
\providecommand{\publicationstatus}{J. Esparza, E. Tronci (Eds.): Games, Automata,\\ 
Logics and Formal Verification 2015 (GandALF'15)\\
EPTCS 193, 2015, pp.\ \pageref*{FirstPage}--\pageref{LastPage},
doi:\href{http://dx.doi.org/10.4204/EPTCS.193.3}{10.4204/EPTCS.193.3}}

Reachability.tex
\documentclass[copyright,creativecommons]{eptcs}
\providecommand{\event}{GandALF 2015} % Name of the event you are submitting to
%\usepackage{breakurl}             % Not needed if you use pdflatex only.

\input{0-includes}

\begin{document}


\title{Negotiation Games}
\author{Philipp Hoffmann
\institute{Fakult\"at f\"{u}r Informatik\\
Technische Universit\"{a}t M\"{u}nchen\\
Germany}
\email{ph.hoffmann@tum.de}
}
\newcommand{\titlerunning}{Negotiation Games}
\newcommand{\authorrunning}{Philipp Hoffmann}
\maketitle


\begin{abstract}
Negotiations, a model of concurrency with multi party negotiation as primitive,
have been recently introduced in \cite{negI,negII}. We initiate the study of games for 
this model. We study {\em coalition problems}: can a given coalition of agents 
force that a negotiation terminates (resp. block the negotiation so that it goes 
on forever)?; can the coalition force a given outcome of the negotiation? We show
that for arbitrary negotiations the problems are EXPTIME-complete. 
Then we show that for sound and deterministic or even weakly deterministic
negotiations the problems can be solved in PTIME. Notice that the 
input of the problems is a negotiation, which can be exponentially more compact 
than its state space.
\end{abstract}

\input{1-introduction}
\input{2-definitions}
\input{3-parties}
\input{4-reduction}
\input{5-poly}
\input{6-conclusion}

\bibliographystyle{eptcs}
\bibliography{references}

%\appendix

%\input{7-appendix}
\end{document}

FDDM.tex
\tikz{
\nego[text={F\space\space M},id=n0,spacing=2]{0,1}
\node at (n0-P1) {D$_1$};
\node at (n0-P2) {D$_2$};
\node[left = 0cm of n0-P0, font=\large] {$n_0$};
\nego[text={\space\space },id=n1,spacing=2]{2,0}
\node at (n1-P0) {D$_1$};
\node at (n1-P1) {D$_2$};
\node[left = 0cm of n1-P0, font=\large] {$n_1$};
\nego[text={F\space\space },id=n2]{0,-3}
\node at (n2-P1) {D$_1$};
\node at (n2-P2) {D$_2$};
\node[above left = -0.1cm and 0cm of n2-P0, font=\large] {$n_2$};
\nego[text={\space\space M},id=n3]{1,-4}
\node at (n3-P0) {D$_1$};
\node at (n3-P1) {D$_2$};
\node[above right = -0.25cm and 0.1cm of n3-P2, font=\large] {$n_3$};
\nego[text={F\space },id=n4]{5,-3}
\node at (n4-P1) {D$_1$};
\node[above right = 0cm and -0.2cm of n4-P1, font=\large] {$n_4$};
\nego[text={\space M},id=n5]{6,-4}
\node at (n5-P0) {D$_1$};
\node[above right = -0.2 cm and  0cm of n5-P1, font=\large] {$n_5$};
\nego[text={F\space\space M},id=nf,spacing=2]{0,-6}
\node at (nf-P1) {D$_1$};
\node at (nf-P2) {D$_2$};
\node[left = 0cm of nf-P0, font=\large] {$n_f$};
\pgfsetarrowsend{latex}
\draw (n0-P0) -- (n2-P0);
\draw (n0-P0) -- +(0,-2) -- (n4-P0);
\draw (n0-P1) -- (n1-P0);
\draw (n0-P2) -- (n1-P1);
\draw (n0-P3) -- +(0,-2) -- (n3-P2);
\draw (n0-P3) -- +(0,-2) -- (n5-P1);
\draw (n1-P0) -- (n2-P1);
\draw (n1-P0) -- (n4-P1);
\draw (n1-P1) -- (n2-P2);
\draw (n1-P1) -- (nf-P2);
%Father
\draw (n2-P0) -- (nf-P0);
\draw (n2-P0) -- +(0,-1)  to [out=180,in=180,out looseness=2] (n2-P0);
\draw (n4-P0) -- +(0,-2) -- (nf-P0);
\draw (n4-P0) -- +(0,-1)  to [out=180,in=180,out looseness=2] (n4-P0);
%Mother
\draw (n5-P1) -- +(0,-1) -- (nf-P3);
\draw (n5-P1) -- +(0,-1)  to [out=0,in=0,out looseness=2] (n5-P1);
\draw (n3-P2) -- +(0,-1) -- (nf-P3);
\draw (n3-P2) -- +(0,-1)  to [out=0,in=0,out looseness=2] (n3-P2);
%Daughters
%n2 n3
\draw (n2-P1) to [out=-120,in=120] (n3-P0);
\draw (n3-P0) to [out=60,in=-60] (n2-P1);
\draw (n2-P2) to [out=-120,in=120] (n3-P1);
\draw (n3-P1) to [out=60,in=-60] (n2-P2);
\draw[dashed] (n2-P1) -- +(-0.5,-0.5) -- +(-0.5,-2) -- (nf-P1);
\draw[dashed] (n2-P2) -- +(-0.5,-0.5) -- +(-0.5,-2) -- (nf-P2);
\draw[dashed] (n3-P0) -- +(0,-1) -- (nf-P1);
\draw[dashed] (n3-P1) -- +(0,-1) -- (nf-P2);
%n4 n5
\draw (n4-P1) to [out=-120,in=120] (n5-P0);
\draw (n5-P0) to [out=60,in=-60] (n4-P1);
\draw[dashed] (n4-P1) -- +(-0.5,-0.5) -- +(-0.5,-2) -- (nf-P1);
\draw[dashed] (n5-P0) -- +(0,-1) -- (nf-P1);
%labels
\node[anchor=south] at ($(n1-P0)+(-0.3,-0.7)$) {t};
\node[anchor=south] at ($(n1-P1)+(-0.5,-0.7)$) {t};
\node[anchor=south] at ($(n1-P0)+(+0.85,-0.7)$) {s};
\node[anchor=south] at ($(n1-P1)+(+0.2,-0.7)$) {s};
%\labelEdge[start=n1-P0,end=n2-P1,dist=0.5,shift={-0.15,0}]{t}
%\labelEdge[start=n1-P1,end=n2-P2,dist=0.5,shift={-0.1,0}]{t}
%\labelEdge[start=n1-P0,end=n4-P1,dist=0.5,shift={0.15,0}]{s}
%\labelEdge[start=n1-P1,end=nf-P2,dist=0.5,shift={0.15,0}]{s}
}
FDDM_extended.tex
\tikz{
%n0
\nego[text={F\space\space M},id=n0,spacing=2]{0,1}
\node at (n0-P1) {D$_1$};
\node at (n0-P2) {D$_2$};
\node[left = 0cm of n0-P0,font=\large] {$n_0$};
%n1
\nego[text={\space\space},id=n1,spacing=2]{2,0}
\node at (n1-P0) {D$_1$};
\node at (n1-P1) {D$_2$};
\node[left = 0cm of n1-P0, font=\large] {$n_1$};
%n2
\nego[text={F\space\space},id=n2]{-2,-3}
\node at (n2-P1) {D$_1$};
\node at (n2-P2) {D$_2$};
\node[left = 0cm of n2-P0, font=\large] {$n_2$};
%n3
\nego[text={\space\space M},id=n3]{-1,-4}
\node at (n3-P0) {D$_1$};
\node at (n3-P1) {D$_2$};
\node[right = 0cm of n3-P2, font=\large] {$n_3$};
%n4
\nego[text={F\space},id=n4]{2,-3}
\node at (n4-P1) {D$_1$};
\node[above right = -0.1cm and 0cm of n4-P1, font=\large] {$n_4$};
%n5
\nego[text={\space M},id=n5]{3,-4}
\node at (n5-P0) {D$_2$};
\node[right = 0cm of n5-P1, font=\large] {$n_5$};
%n6
\nego[text={\space M},id=n6]{7,-3}
\node at (n6-P0) {D$_1$};
\node[left = 0cm of n6-P0, font=\large] {$n_6$};
%n7
\nego[text={F\space},id=n7]{6,-4}
\node at (n7-P1) {D$_2$};
\node[left = 0cm of n7-P0, font=\large] {$n_7$};
%nf
\nego[text={F\space\space M},id=nf,spacing=2]{0,-7}
\node at (nf-P1) {D$_1$};
\node at (nf-P2) {D$_2$};
%nyes nno
\nego[ports=1,id=nyes1]{1,-6}
\node at (nyes1-P0) {D$_1$};
\node[below left = -0.15cm and -0.05cm of nyes1-P0, font=\large] {good$_1$};
\nego[ports=1,id=nno1]{2,-6}
\node at (nno1-P0) {D$_1$};
\node[below right = -0.15cm and -0.15cm of nno1-P0, font=\large] {bad$_1$};
\nego[ports=1,id=nyes2]{4,-6}
\node at (nyes2-P0) {D$_2$};
\node[below left = -0.15cm and -0.25cm of nyes2-P0, font=\large] {bad$_2$};
\nego[ports=1,id=nno2]{5,-6}
\node at (nno2-P0) {D$_2$};
\node[below right = -0.15cm and -0.05cm of nno2-P0, font=\large] {good$_2$};
\pgfsetarrowsend{latex}
\draw (n0-P1) -- (n1-P0);
\draw (n0-P2) -- (n1-P1);
\draw (n1-P0) -- (n2-P1);
\draw (n1-P0) -- (n4-P1);
\draw (n1-P1) -- (n2-P2);
\draw (n1-P1) -- (n6-P0);
% %Father
% \draw (n0-P0) -- +(0,-1) -- +(-0.2,-1.3);
% \draw (n0-P0) -- +(0,-1) -- +(0.2,-1.3);
% \draw (n0-P0) -- +(0,-1) -- +(0.45,-1.3);
% %Mother
% \draw (n0-P3) -- +(0,-1) -- +(-0.375,-1.3);
% \draw (n0-P3) -- +(0,-1) -- +(-0.15,-1.3);
% \draw (n0-P3) -- +(0,-1) -- +(0.2,-1.3);
%Daughters
%n2 n3
\draw (n2-P1) to [out=-120,in=120] (n3-P0);
\draw (n3-P0) to [out=60,in=-60] (n2-P1);
\draw (n2-P2) to [out=-120,in=120] (n3-P1);
\draw (n3-P1) to [out=60,in=-60] (n2-P2);
\draw[dashed] (n2-P1) -- +(-0.4,-0.5) -- +(-0.4,-2) -- (nyes1-P0);
\draw[densely dotted] (n2-P1) -- +(0.4,-0.5) -- +(0.4,-2) -- (nno1-P0);
\draw[dashed] (n2-P2) -- +(-0.4,-0.5) -- +(-0.4,-1.5) -- (nyes2-P0);
\draw[densely dotted] (n2-P2) -- +(0.4,-0.5) -- +(0.4,-1.5) -- (nno2-P0);
\draw[dashed] (n3-P0) -- +(-0,-1) -- (nyes1-P0);
\draw[densely dotted] (n3-P0) -- +(0.2,-1) -- (nno1-P0);
\draw[dashed] (n3-P1) -- +(-0.1,-0.5) -- (nyes2-P0);
\draw[densely dotted] (n3-P1) -- +(0.1,-0.5) -- (nno2-P0);
%n4 n5
\draw (n4-P1) to [out=-120,in=120] (n5-P0);
%\draw (n4-P1)-- (n5-P0);
\draw (n5-P0) to [out=60,in=-60] (n4-P1);
\draw[dashed] (n4-P1) -- +(-1.5,-1.5) -- (nyes1-P0);
\draw[densely dotted] (n4-P1) -- +(-1,-1.5) -- (nno1-P0);
\draw[dashed] (n5-P0) -- +(-0.2,-1) -- (nyes1-P0);
\draw[densely dotted] (n5-P0) -- +(0,-1) -- (nno1-P0);
%n6 n7
\draw (n6-P0) to [out=-120,in=120] (n7-P1);
\draw (n7-P1) to [out=60,in=-60] (n6-P0);
\draw[dashed] (n6-P0) -- +(-0.5,-0.5) -- +(-0.5,-2) -- (nyes2-P0);
\draw[densely dotted] (n6-P0) -- +(0.5,-0.5) -- +(0.5,-2) -- (nno2-P0);
\draw[dashed] (n7-P1) -- +(-0.2,-1) -- (nyes2-P0);
\draw[densely dotted] (n7-P1) -- +(0,-1) -- (nno2-P0);
\node[anchor=south] at ($(n1-P0)+(-0.3,-0.7)$) {t};
\node[anchor=south] at ($(n1-P1)+(-0.35,-0.7)$) {t};
\node[anchor=south] at ($(n1-P0)+(+0.3,-0.7)$) {s};
\node[anchor=south] at ($(n1-P1)+(+0.25,-0.7)$) {s};
%\labelEdge[start=n1-P0,end=n2-P1,dist=0.5,shift={0.3,0}]{t}
%\labelEdge[start=n1-P1,end=n2-P2,dist=0.5,shift={0.35,0}]{t}
%\labelEdge[start=n1-P0,end=n4-P1,dist=0.5,shift={-0.12,0}]{s}
%\labelEdge[start=n1-P1,end=n6-P0,dist=0.5,shift={-0.25,0}]{s}
%nYes nNo
\draw (nyes1-P0) -- (nf-P1);
\draw (nno1-P0) -- (nf-P1);
\draw (nyes2-P0) -- (nf-P2);
\draw (nno2-P0) -- (nf-P2);
}
FDM_acyclic.tex
\begin{tikzpicture}
\nego[text=FDM,id=n0,spacing=2]{0,0}
\node[left = 0cm of n0-P0, font=\large] {$n_0$};
\nego[text=FD,id=n1]{0,-2}
\node[left = 0cm of n1-P0, font=\large] {$n_1$};
\nego[text=DM,id=n2]{3,-4}
\node[left = 0cm of n2-P0, font=\large] {$n_2$};
\nego[text=FDM,id=nf,spacing=2]{0,-6}
\node[left = 0cm of nf-P0, font=\large] {$n_f$};
\pgfsetarrowsend{latex}
\draw (n0-P0) -- (n1-P0);
\node[anchor=south] at ($(n0-P0)+(-0.25,-0.8)$) {st};
%\labelEdge[start=n0-P0,end=n1-P0,dist=0.7,shift={-0.3,0}]{st}
\draw (n0-P1) -- (n1-P1);
\node[anchor=south] at ($(n0-P1)+(-0.55,-0.8)$) {st};
%\labelEdge[start=n0-P1,end=n1-P1,dist=0.7,shift={-0.4,0}]{st}
\draw (n0-P2) -- (n2-P1);
\node[anchor=south] at ($(n0-P2)+(-0.25,-0.8)$) {st};
%\labelEdge[start=n0-P2,end=n2-P1,dist=0.7,shift={0.3,0}]{st}
\draw (4,-1) -- (4.5,-1.5) -- (4.5,-5.5) -- (nf-P2);
\draw (n1-P0) -- (nf-P0);
\node[anchor=south] at ($(n1-P0)+(-0.55,-1.8)$) {y,n,am};
%\labelEdge[start=n1-P0,end=nf-P0,dist=1.5,shift={-0.6,0}]{y,n,am}
\draw (n1-P1) -- (n2-P0);
\node[anchor=south] at ($(n1-P1)+(+1.35,-1.2)$) {am};
%\labelEdge[start=n1-P1,end=n2-P0,dist=0.5,shift={0.5,0}]{am}
\draw (n1-P1) -- (nf-P1);
\node[anchor=south] at ($(n1-P1)+(+0.05,-1.8)$) {y,n};
%\labelEdge[start=n1-P1,end=nf-P1,dist=1.3,shift={0.3,0}]{y,n}
\draw (n2-P0) -- (nf-P1);
\node[anchor=south] at ($(n2-P0)+(-0.55,-0.8)$) {y,n};
%\labelEdge[start=n2-P0,end=nf-P1,dist=0.5,shift={-0.3,0}]{y,n}
\draw (n2-P1) -- (nf-P2);
\node[anchor=south] at ($(n2-P1)+(-0.30,-0.8)$) {y,n};
%\labelEdge[start=n2-P1,end=nf-P2,dist=0.5,shift={-0.35,0}]{y,n}
\end{tikzpicture}
FDM_cyclic.tex
\begin{tikzpicture}
\nego[text=FDM,id=n0,spacing=2]{0,0}
\node[left = 0cm of n0-P0, font=\large] {$n_0$};
\nego[text=FD,id=n1,spacing=2]{0,-2}
\node[left = 0cm of n1-P0, font=\large] {$n_1$};
\nego[text=FDM,id=n2,spacing=2]{0,-4}
\node[left = 0cm of n2-P0, font=\large] {$n_2$};
\nego[text=FDM,id=nf,spacing=2]{0,-6}
\node[left = 0cm of nf-P0, font=\large] {$n_f$};
\pgfsetarrowsend{latex}
\draw (n0-P0) -- (n1-P0);
\node[anchor=south] at ($(n0-P0)+(+0.25,-1.3)$) {y};
%\labelEdge[start=n0-P0,end=n1-P0,dist=1,shift={0.2,0}]{y}
\draw (n0-P1) -- (n1-P1);
\node[anchor=south] at ($(n0-P1)+(-0.25,-1.3)$) {y};
%\labelEdge[start=n0-P1,end=n1-P1,dist=1,shift={-0.2,0}]{y}
\draw (n0-P2) -- (n2-P2);
\node[anchor=south] at ($(n0-P2)+(-0.25,-1.3)$) {y};
%\labelEdge[start=n0-P2,end=n2-P2,dist=1,shift={-0.2,0}]{y}
\draw (n1-P0) -- (n2-P0);
\node[anchor=south] at ($(n1-P0)+(+0.25,-1.3)$) {tm};
%\labelEdge[start=n1-P0,end=n2-P0,dist=1,shift={0.3,0}]{tm}
\draw (n1-P1) -- (n2-P1);
\node[anchor=south] at ($(n1-P1)+(-0.25,-1.3)$) {tm};
%\labelEdge[start=n1-P1,end=n2-P1,dist=1,shift={-0.3,0}]{tm}
\draw (n2-P0) -- (nf-P0);
\node[anchor=south] at ($(n2-P0)+(+0.25,-1.3)$) {y};
%\labelEdge[start=n2-P0,end=nf-P0,dist=1,shift={0.2,0}]{y}
\draw (n2-P1) -- (nf-P1);
\node[anchor=south] at ($(n2-P1)+(-0.25,-1.3)$) {y};
%\labelEdge[start=n2-P1,end=nf-P1,dist=1,shift={-0.2,0}]{y}
\draw (n2-P2) -- (nf-P2);
\node[anchor=south] at ($(n2-P2)+(-0.25,-1.3)$) {y};
%\labelEdge[start=n2-P2,end=nf-P2,dist=1,shift={-0.2,0}]{y}
\draw (n0-P0) to [out=225,in=90] node [at end,auto,swap] {n} (-1.3cm,-3cm) to [out=-90,in=135] (nf-P0);
\draw (n0-P1) to [out=-45,in=90] node [at end,auto] {n} (+3.3cm,-3cm) to [out=-90,in=45] (nf-P1);
\draw (n0-P2) to [out=-45,in=90] node [at end,auto] {n} (+5.3cm,-3cm) to [out=-90,in=45] (nf-P2);
\draw (n2-P0) to [out=135,in=-90] node [near end,auto] {r}  (-0.5cm,-3cm) to [out=90,in=-135] (n1-P0);
\draw (n2-P1) to [out=45,in=-90] node [near end,auto,swap] {r}  (+2.5cm,-3cm) to [out=90,in=-45] (n1-P1);
\draw (n2-P2) to [out=-45,in=-90,in looseness=2] node [near end, auto, swap] {r} (+4.8cm,-4cm) to [out=90,in=45,out looseness=2] (n2-P2);
\token[color=black]{-0.5,-3}
\token[color=black]{2.5,-3}
\token[color=black]{4.8,-4}
\end{tikzpicture}

det_control.tex
\tikz{
\nego[text={$A$}{$B$},id=n0]{0,0}
\node[left = 0cm of n0-P0, font=\large] {$n_0$};
\nego[text={$A$}{$B$},id=n1]{0,-1.5}
\node[left = 0cm of n1-P0, font=\large] {$n_1$};
\nego[text={$A$}{$B$},id=n2]{0,-3}
\node[left = 0.3cm of n2-P0, font=\large] {$n_2$};
\nego[text={$A$}{$B$},id=nf]{0,-4.5}
\node[left = 0cm of nf-P0, font=\large] {$n_f$};
\pgfsetarrowsend{latex}
\draw (n0-P0) -- (n1-P0);
\draw (n0-P1) -- (n1-P1);
\draw (n1-P0) to[out=-110,in=110] (n2-P0);
\draw (n1-P1) to[out=-110,in=110] (n2-P1);
\draw (n2-P0) to[out=70,in=-70] (n1-P0);
\draw (n2-P1) to[out=70,in=-70] (n1-P1);
\draw (n2-P0) -- (nf-P0);
\draw (n2-P1) -- (nf-P1);
\draw (n1-P0) to[out=-120,in=120] (nf-P0);
\draw (n1-P1) to[out=-60,in=60] (nf-P1);
\node[anchor=south] at ($(n0-P0)+(-0.15,-0.9)$) {a};
\node[anchor=south] at ($(n0-P1)+(-0.15,-0.9)$) {a};
\node[anchor=south] at ($(n1-P0)+(-0.05,-0.7)$) {a};
\node[anchor=south] at ($(n1-P1)+(-0.05,-0.7)$) {a};
\node[anchor=south] at ($(n2-P0)+(0.05,0.3)$) {a};
\node[anchor=south] at ($(n2-P1)+(0.05,0.3)$) {a};
\node[anchor=south] at ($(n2-P0)+(-0.15,-0.9)$) {b};
\node[anchor=south] at ($(n2-P1)+(-0.15,-0.9)$) {b};
\node[anchor=south] at ($(n1-P0)+(-0.45,-0.7)$) {b};
\node[anchor=south] at ($(n1-P1)+(0.45,-0.7)$) {b};
%n0 n1
%\labelEdge[start=n0-P0,end=n1-P0,dist=0.75,shift={-0.15,0}]{a}
%\labelEdge[start=n0-P1,end=n1-P1,dist=0.75,shift={-0.15,0}]{a}
%n1 n2
%\labelEdge[start=n1-P0,end=n2-P0,dist=0.5,shift={-0.05,0}]{a}
%\labelEdge[start=n1-P1,end=n2-P1,dist=0.5,shift={-0.05,0}]{a}
%n2 n1
%\labelEdge[start=n2-P0,end=n1-P0,dist=0.5,shift={0.05,0}]{a}
%\labelEdge[start=n2-P1,end=n1-P1,dist=0.5,shift={0.05,0}]{a}
%n1 nf
%\labelEdge[start=n1-P0,end=nf-P0,dist=0.5,shift={-0.4,0}]{b}
%\labelEdge[start=n1-P1,end=nf-P1,dist=0.5,shift={0.4,0}]{b}
%n2 nf
%\labelEdge[start=n2-P0,end=nf-P0,dist=0.75,shift={-0.15,0}]{b}
%\labelEdge[start=n2-P1,end=nf-P1,dist=0.75,shift={-0.15,0}]{b}
}
ndet_control.tex
\tikz{
\nego[text={$A$}{$B$}{$a$},id=n0]{0,0}
\node[left = 0cm of n0-P0, font=\large] {$n_0$};
\nego[text={$A$}{$B$}{$a$},id=n1]{0,-1.5}
\node[left = 0cm of n1-P0, font=\large] {$n_1$};
\nego[text={$A$}{$B$},id=n2]{0,-3}
\node[left = 0.3cm of n2-P0, font=\large] {$n_2$};
\nego[text={$A$}{$B$}{$a$},id=nf]{0,-4.5}
\node[left = 0cm of nf-P0, font=\large] {$n_f$};
\pgfsetarrowsend{latex}
\draw (n0-P0) -- (n1-P0);
\draw (n0-P1) -- (n1-P1);
\draw (n0-P2) -- (n1-P2);
\draw (n1-P0) to[out=-110,in=110] (n2-P0);
\draw (n1-P1) to[out=-110,in=110] (n2-P1);
\draw (n1-P0) to[out=-120,in=120] (nf-P0);
\draw (n1-P1) to[out=-60,in=60] (nf-P1);
\draw (n1-P2) -- (nf-P2);
\draw (n1-P2) + (0,-1) to [out=0,in=0,out looseness = 2,in looseness=2] (n1-P2);
\draw (n2-P0) to[out=70,in=-70] (n1-P0);
\draw (n2-P1) to[out=70,in=-70] (n1-P1);
\draw (n2-P0) -- (nf-P0);
\draw (n2-P1) -- (nf-P1);
\node[anchor=south] at ($(n1-P2)+(0.25,-0.8)$) {a,b};
%\labelEdge[start=n1-P2,end=nf-P2,dist=0.65,shift={0.25,0}]{a,b}
}
ndet_control2.tex
\tikz{
\nego[text={$A$}{$B$}{$a$}{$b$},id=n0]{0,0}
\node[left = 0cm of n0-P0, font=\large] {$n_0$};
\nego[text={$A$}{$B$}{$a$},id=n1]{0,-1.5}
\node[left = 0cm of n1-P0, font=\large] {$n_1$};
\nego[text={$A$}{$B$},id=n2]{0,-3}
\node[left = 0.3cm of n2-P0, font=\large] {$n_2$};
\nego[text={$A$}{$B$}{$a$}{$b$},id=nf]{0,-4.5}
\node[left = 0cm of nf-P0, font=\large] {$n_f$};
\pgfsetarrowsend{latex}
\draw (n0-P0) -- (n1-P0);
\draw (n0-P1) -- (n1-P1);
\draw (n0-P2) -- (n1-P2);
\draw (n0-P3) -- (nf-P3);
\draw (n0-P3) + (0,-1) to [out=0,in=0,out looseness = 2,in looseness=2] (n0-P3);
\draw (n1-P0) to[out=-110,in=110] (n2-P0);
\draw (n1-P1) to[out=-110,in=110] (n2-P1);
\draw (n1-P0) to[out=-120,in=120] (nf-P0);
\draw (n1-P1) to[out=-60,in=60] (nf-P1);
\draw (n1-P2) -- (nf-P2);
\draw (n1-P2) + (0,-1) to [out=0,in=0,out looseness = 2,in looseness=2] (n1-P2);
\draw (n2-P0) to[out=70,in=-70] (n1-P0);
\draw (n2-P1) to[out=70,in=-70] (n1-P1);
\draw (n2-P0) -- (nf-P0);
\draw (n2-P1) -- (nf-P1);
\node[anchor=south] at ($(n0-P3)+(-0.15,-0.9)$) {a};
%\labelEdge[start=n0-P3,end=nf-P3,dist=0.75,shift={-0.15,0}]{a}
}
Reachability.bbl
\newcommand{\noopsort}[1]{} \newcommand{\singleletter}[1]{#1}
\begin{thebibliography}{10}
\providecommand{\bibitemdeclare}[2]{}
\providecommand{\surnamestart}{}
\providecommand{\surnameend}{}
\providecommand{\urlprefix}{Available at }
\providecommand{\url}[1]{\texttt{#1}}
\providecommand{\href}[2]{\texttt{#2}}
\providecommand{\urlalt}[2]{\href{#1}{#2}}
\providecommand{\doi}[1]{doi:\urlalt{http://dx.doi.org/#1}{#1}}
\providecommand{\bibinfo}[2]{#2}

\bibitemdeclare{article}{DBLP:journals/tcs/AlfaroHK07}
\bibitem{DBLP:journals/tcs/AlfaroHK07}
\bibinfo{author}{Luca \surnamestart de~Alfaro\surnameend},
  \bibinfo{author}{Thomas~A. \surnamestart Henzinger\surnameend} \&
  \bibinfo{author}{Orna \surnamestart Kupferman\surnameend}
  (\bibinfo{year}{2007}): \emph{\bibinfo{title}{Concurrent reachability
  games}}.
\newblock {\sl \bibinfo{journal}{Theor. Comput. Sci.}}
  \bibinfo{volume}{386}(\bibinfo{number}{3}), pp. \bibinfo{pages}{188--217}.
\newblock \urlprefix\url{http://dx.doi.org/10.1016/j.tcs.2007.07.008}.

\bibitemdeclare{article}{DBLP:journals/jacm/AlurHK02}
\bibitem{DBLP:journals/jacm/AlurHK02}
\bibinfo{author}{Rajeev \surnamestart Alur\surnameend},
  \bibinfo{author}{Thomas~A. \surnamestart Henzinger\surnameend} \&
  \bibinfo{author}{Orna \surnamestart Kupferman\surnameend}
  (\bibinfo{year}{2002}): \emph{\bibinfo{title}{Alternating-time temporal
  logic}}.
\newblock {\sl \bibinfo{journal}{J. ACM}}
  \bibinfo{volume}{49}(\bibinfo{number}{5}), pp. \bibinfo{pages}{672--713}.
\newblock \urlprefix\url{http://doi.acm.org/10.1145/585265.585270}.

\bibitemdeclare{inproceedings}{DBLP:conf/icalp/BrazdilJK10}
\bibitem{DBLP:conf/icalp/BrazdilJK10}
\bibinfo{author}{Tom{\'a}s \surnamestart Br{\'a}zdil\surnameend},
  \bibinfo{author}{Petr \surnamestart Jancar\surnameend} \&
  \bibinfo{author}{Anton\'{\i}n \surnamestart Kucera\surnameend}
  (\bibinfo{year}{2010}): \emph{\bibinfo{title}{Reachability Games on Extended
  Vector Addition Systems with States}}.
\newblock In \bibinfo{editor}{Samson \surnamestart Abramsky\surnameend},
  \bibinfo{editor}{Cyril \surnamestart Gavoille\surnameend},
  \bibinfo{editor}{Claude \surnamestart Kirchner\surnameend},
  \bibinfo{editor}{Friedhelm \surnamestart {Meyer auf der Heide}\surnameend} \&
  \bibinfo{editor}{Paul~G. \surnamestart Spirakis\surnameend}, editors: {\sl
  \bibinfo{booktitle}{ICALP (2)}}, {\sl \bibinfo{series}{Lecture Notes in
  Computer Science}} \bibinfo{volume}{6199}, \bibinfo{publisher}{Springer}, pp.
  \bibinfo{pages}{478--489}.
\newblock \urlprefix\url{http://dx.doi.org/10.1007/978-3-642-14162-1_40}.

\bibitemdeclare{article}{DBLP:journals/jacm/ChandraKS81}
\bibitem{DBLP:journals/jacm/ChandraKS81}
\bibinfo{author}{Ashok~K. \surnamestart Chandra\surnameend},
  \bibinfo{author}{Dexter \surnamestart Kozen\surnameend} \&
  \bibinfo{author}{Larry~J. \surnamestart Stockmeyer\surnameend}
  (\bibinfo{year}{1981}): \emph{\bibinfo{title}{Alternation}}.
\newblock {\sl \bibinfo{journal}{J. {ACM}}}
  \bibinfo{volume}{28}(\bibinfo{number}{1}), pp. \bibinfo{pages}{114--133},
  \doi{10.1145/322234.322243}.

\bibitemdeclare{inproceedings}{negI}
\bibitem{negI}
\bibinfo{author}{Javier \surnamestart Esparza\surnameend} \&
  \bibinfo{author}{J{\"o}rg \surnamestart Desel\surnameend}
  (\bibinfo{year}{2013}): \emph{\bibinfo{title}{On Negotiation as Concurrency
  Primitive}}.
\newblock In \bibinfo{editor}{Pedro~R. \surnamestart D'Argenio\surnameend} \&
  \bibinfo{editor}{Hern{\'a}n~C. \surnamestart Melgratti\surnameend}, editors:
  {\sl \bibinfo{booktitle}{CONCUR}}, {\sl \bibinfo{series}{Lecture Notes in
  Computer Science}} \bibinfo{volume}{8052}, \bibinfo{publisher}{Springer}, pp.
  \bibinfo{pages}{440--454}.
\newblock \urlprefix\url{http://dx.doi.org/10.1007/978-3-642-40184-8_31}.

\bibitemdeclare{inproceedings}{negII}
\bibitem{negII}
\bibinfo{author}{Javier \surnamestart Esparza\surnameend} \&
  \bibinfo{author}{J{\"o}rg \surnamestart Desel\surnameend}
  (\bibinfo{year}{2014}): \emph{\bibinfo{title}{On Negotiation as Concurrency
  Primitive II: Deterministic Cyclic Negotiations}}.
\newblock In \bibinfo{editor}{Anca \surnamestart Muscholl\surnameend}, editor:
  {\sl \bibinfo{booktitle}{FoSSaCS}}, {\sl \bibinfo{series}{Lecture Notes in
  Computer Science}} \bibinfo{volume}{8412}, \bibinfo{publisher}{Springer}, pp.
  \bibinfo{pages}{258--273}.
\newblock \urlprefix\url{http://dx.doi.org/10.1007/978-3-642-54830-7_17}.

\bibitemdeclare{article}{DBLP:journals/fmsd/GastinSZ09}
\bibitem{DBLP:journals/fmsd/GastinSZ09}
\bibinfo{author}{Paul \surnamestart Gastin\surnameend},
  \bibinfo{author}{Nathalie \surnamestart Sznajder\surnameend} \&
  \bibinfo{author}{Marc \surnamestart Zeitoun\surnameend}
  (\bibinfo{year}{2009}): \emph{\bibinfo{title}{Distributed synthesis for
  well-connected architectures}}.
\newblock {\sl \bibinfo{journal}{Formal Methods in System Design}}
  \bibinfo{volume}{34}(\bibinfo{number}{3}), pp. \bibinfo{pages}{215--237}.
\newblock \urlprefix\url{http://dx.doi.org/10.1007/s10703-008-0064-7}.

\bibitemdeclare{inproceedings}{DBLP:conf/icalp/GenestGMW13}
\bibitem{DBLP:conf/icalp/GenestGMW13}
\bibinfo{author}{Blaise \surnamestart Genest\surnameend}, \bibinfo{author}{Hugo
  \surnamestart Gimbert\surnameend}, \bibinfo{author}{Anca \surnamestart
  Muscholl\surnameend} \& \bibinfo{author}{Igor \surnamestart
  Walukiewicz\surnameend} (\bibinfo{year}{2013}):
  \emph{\bibinfo{title}{Asynchronous Games over Tree Architectures}}.
\newblock In \bibinfo{editor}{Fedor~V. \surnamestart Fomin\surnameend},
  \bibinfo{editor}{Rusins \surnamestart Freivalds\surnameend},
  \bibinfo{editor}{Marta~Z. \surnamestart Kwiatkowska\surnameend} \&
  \bibinfo{editor}{David \surnamestart Peleg\surnameend}, editors: {\sl
  \bibinfo{booktitle}{ICALP (2)}}, {\sl \bibinfo{series}{Lecture Notes in
  Computer Science}} \bibinfo{volume}{7966}, \bibinfo{publisher}{Springer}, pp.
  \bibinfo{pages}{275--286}.
\newblock \urlprefix\url{http://dx.doi.org/10.1007/978-3-642-39212-2_26}.

\bibitemdeclare{inproceedings}{DBLP:conf/rp/Kucera12}
\bibitem{DBLP:conf/rp/Kucera12}
\bibinfo{author}{Anton\'{\i}n \surnamestart Kucera\surnameend}
  (\bibinfo{year}{2012}): \emph{\bibinfo{title}{Playing Games with Counter
  Automata}}.
\newblock In \bibinfo{editor}{Alain \surnamestart Finkel\surnameend},
  \bibinfo{editor}{J{\'e}r{\^o}me \surnamestart Leroux\surnameend} \&
  \bibinfo{editor}{Igor \surnamestart Potapov\surnameend}, editors: {\sl
  \bibinfo{booktitle}{RP}}, {\sl \bibinfo{series}{Lecture Notes in Computer
  Science}} \bibinfo{volume}{7550}, \bibinfo{publisher}{Springer}, pp.
  \bibinfo{pages}{29--41}.
\newblock \urlprefix\url{http://dx.doi.org/10.1007/978-3-642-33512-9_4}.

\bibitemdeclare{inproceedings}{DBLP:conf/fsttcs/MohalikW03}
\bibitem{DBLP:conf/fsttcs/MohalikW03}
\bibinfo{author}{Swarup \surnamestart Mohalik\surnameend} \&
  \bibinfo{author}{Igor \surnamestart Walukiewicz\surnameend}
  (\bibinfo{year}{2003}): \emph{\bibinfo{title}{Distributed Games}}.
\newblock In \bibinfo{editor}{Paritosh~K. \surnamestart Pandya\surnameend} \&
  \bibinfo{editor}{Jaikumar \surnamestart Radhakrishnan\surnameend}, editors:
  {\sl \bibinfo{booktitle}{FSTTCS}}, {\sl \bibinfo{series}{Lecture Notes in
  Computer Science}} \bibinfo{volume}{2914}, \bibinfo{publisher}{Springer}, pp.
  \bibinfo{pages}{338--351}.
\newblock \urlprefix\url{http://dx.doi.org/10.1007/978-3-540-24597-1_29}.

\bibitemdeclare{article}{rubinstein1982perfect}
\bibitem{rubinstein1982perfect}
\bibinfo{author}{Ariel \surnamestart Rubinstein\surnameend}
  (\bibinfo{year}{1982}): \emph{\bibinfo{title}{Perfect equilibrium in a
  bargaining model}}.
\newblock {\sl \bibinfo{journal}{Econometrica}}
  \bibinfo{volume}{50}(\bibinfo{number}{1}), pp. \bibinfo{pages}{97--109},
  \doi{10.2307/1912531}.

\bibitemdeclare{article}{DBLP:journals/iandc/Walukiewicz01}
\bibitem{DBLP:journals/iandc/Walukiewicz01}
\bibinfo{author}{Igor \surnamestart Walukiewicz\surnameend}
  (\bibinfo{year}{2001}): \emph{\bibinfo{title}{Pushdown Processes: Games and
  Model-Checking}}.
\newblock {\sl \bibinfo{journal}{Inf. Comput.}}
  \bibinfo{volume}{164}(\bibinfo{number}{2}), pp. \bibinfo{pages}{234--263}.
\newblock \urlprefix\url{http://dx.doi.org/10.1006/inco.2000.2894}.

\end{thebibliography}
