text:
\section{Introduction\label{sec:introduction}}
Temporal logics~\cite{EAE:90}, such as Linear Temporal Logic (LTL) and Computation Tree Logic (CTL), are traditionally used for verification of non-deterministic and probabilistic systems~\cite{CB-JPK:08}.
Even though temporal logics are suitable for specifying complex missions for control systems, they did not gain popularity in the control community until recently~\cite{PT-GJP:06, MK-CB:10, TW-UT-RMM:10}.

The existing works on control synthesis focus on specifications given in linear time temporal logic.
The systems, which sometimes are obtained through an additional abstraction process \cite{PT-GJP:06,TuYoBeCeBa-CDC10}, have finitely many states.
With few exceptions \cite{Chatterjee2012}, their states are fully observable.
For such systems, control strategies can be synthesized through exhaustive search of the state space.
If the system is deterministic, model checking tools can be easily adapted to generate control strategies~\cite{MK-CB:10}.
If the system is non-deterministic, the control problem can be mapped to the solution of a Rabin game~\cite{WT:02,TuYoBeCeBa-CDC10}, or a simpler B\"uchi \cite{KlBe-HSCC08-book} or GR(1) game~\cite{HKG-GF-GFP:07}, if the specification is restricted to fragments of LTL.
For probabilistic systems, the LTL control synthesis problem reduces to computing a control policy for a Markov Decision Process (MDP)~\cite{AB-LDA:95,MK-GN-DP:02,DiSmBeRu-CDC-2011}.

In this work, we consider mission specifications expressed as syntactically co-safe LTL formulas \cite{OK-MYV:01}.
We focus on a particular type of a multi-agent system formed by a deterministically controlled plant and a set of independent, probabilistic, uncontrollable agents, operating on a common, graph-like environment.
An illustrative example is a car (plant) approaching a pedestrian crossing, while there are some pedestrians (agents) waiting to cross or already crossing the road.
As the state space of the system grows exponentially with the number of pedestrians, one may not be able to utilize any of the existing approaches under computational resource constraints when there is a large number of pedestrians.

We partially address this problem by proposing an incremental control synthesis method that exploits the independence between the components of the system, {\it i.e.},\; the plant modeled as a deterministic transition system and the agents, modeled as Markov chains, and the fact that verification is computationally cheaper than synthesis.
We aim to synthesize a plant control strategy that maximize the probability of satisfying a mission specification given as a syntactically co-safe LTL formula.
Our method initially considers a considerably smaller agent subset and synthesizes a control policy that maximizes the probability of satisfying the mission specification for the subsystem formed by the plant and this subset.
This control policy is then verified against the remaining agents.
At each iteration, we remove transitions and states that are not needed in subsequent iterations. This leads to a significant reduction in computation time and memory usage.
It is important to note that our method does not need to run to completion.
A sub-optimal control policy can be obtained by forcing termination at a given iteration if the computation is performed under stringent resource constraints.
It must also be noted that our framework easily extends to the case when the plant is a Markov Decision Process, and we consider a deterministic plant only for simplicity of presentation.
We experimentally evaluate the performance of our approach and show that our method clearly outperforms existing non-incremental approaches.
Various methods that also use verification during incremental synthesis have been previously proposed in \cite{SJ-SG-SS-AT:2010,SG-SJ-SS-AT-RV:2011}.
However, the approach that we present in this paper is, to the best of our knowledge, the first use of verification guided incremental synthesis in the context of probabilistic systems.

The rest of the paper is organized as follows:
In Sec.~\ref{sec:preliminaries}, we give necessary definitions and some preliminaries in formal methods. The control synthesis problem is formally stated in Sec.~\ref{sec:problem} and the solution is presented in Sec.~\ref{sec:sol}.
Experimental results are included in Sec.~\ref{sec:impl}.
We conclude with final remarks in Sec.~\ref{sec:conclusions}.

\section{Preliminaries \label{sec:preliminaries}}

For a set $\Sigma$, we use $|\Sigma|$ and $2^\Sigma$ to denote its cardinality and power set, respectively.
A (finite) word $\omega$ over a set $\Sigma$ is a sequence of symbols $\omega = \omega^0\ldots\omega^l$ such that $\omega^i \in \Sigma\;\forall i = 0,\ldots,l$.

\begin{definition}[\bf Transition System]
\label{def:TS}
A transition system (TS) is a tuple $\mathbf{T} := (\mathcal{Q}_\mathrm{T}, q_\mathrm{T}^0, \mathcal{A}_\mathrm{T}, \alpha_\mathrm{T}, \delta_\mathrm{T}, \Pi_\mathrm{T}, \mathcal{L}_\mathrm{T})$, where
\begin{itemize}
\item $\mathcal{Q}_\mathrm{T}$ is a finite set of states; %
\item $q_\mathrm{T}^0 \in \mathcal{Q}_\mathrm{T}$ is the initial state; %
\item $\mathcal{A}_\mathrm{T}$ is a finite set of actions; %
\item $\alpha_\mathrm{T}: \mathcal{Q}_\mathrm{T} \to 2^{\mathcal{A}_\mathrm{T}}$ is a map giving the set of actions available at a state;%
\item $\delta_\mathrm{T} \subseteq \mathcal{Q}_\mathrm{T} \times \mathcal{A}_\mathrm{T} \times \mathcal{Q}_\mathrm{T}$ is the transition relation; %
\item $\Pi_\mathrm{T}$ is a finite set of atomic propositions; %
\item $\mathcal{L}_\mathrm{T}:\mathcal{Q}_\mathrm{T}\to 2^{\Pi_\mathrm{T}}$ is a satisfaction map giving the set of atomic propositions satisfied at a state.%
\end{itemize}
\end{definition}

\begin{definition}[\bf Markov Chain]
\label{def:MC}
A (discrete-time, labelled) Markov chain (MC) is a tuple $\mathbf{M} := (\mathcal{Q}_\mathrm{M}, q_\mathrm{M}^0, \delta_\mathrm{M}, \Pi_\mathrm{M}, \mathcal{L}_\mathrm{M})$, where $\mathcal{Q}_\mathrm{M}$, $\Pi_\mathrm{M}$, and $\mathcal{L}_\mathrm{M}$ are the set of states, the set of atomic propositions, and the satisfaction map, respectively, as in Def.~\ref{def:TS}, and
\begin{itemize}
\item $q_\mathrm{M}^0 \in \mathcal{Q}_\mathrm{M}$ is the initial state; %
\item $\delta_\mathrm{M}: \mathcal{Q}_\mathrm{M} \times \mathcal{Q}_\mathrm{M} \to [0,1]$ is the transition probability function that satisfies $\sum_{q'\in\mathcal{Q}_\mathrm{M}} \delta(q,q') = 1\; \forall q\in\mathcal{Q}_\mathrm{M}$. %
\end{itemize}
\end{definition}

In this paper, we are interested in temporal logic missions over a finite time horizon and we use syntactically co-safe LTL formulas~\cite{AB-LEK-MYV:10} to specify them.
Informally, a syntactically co-safe LTL formula over the set $\Pi$ of atomic propositions comprises boolean operators $\neg$ (negation), $\vee$ (disjunction) and $\wedge$ (conjunction), and temporal operators $\mathbf{X}$ (next), $\mathcal{U}$ (until) and $\mathbf{F}$ (eventually).
Any syntactically co-safe LTL formula can be written in positive normal form, where the negation operator $\neg$ occurs only in front of atomic propositions.
For instance, $\mathbf{X}\,\mathtt{p}$ states that at the next position of the word, proposition $\mathtt{p}$ is true.
The formula $\mathtt{p}_1\,\mathcal{U}\,\mathtt{p}_2$ states that there is a future position of the word when proposition $\mathtt{p}_2$ is true, and proposition $\mathtt{p}_1$ is true at least until $\mathtt{p}_2$ is true.
For any syntactically co-safe LTL formula $\phi$ over a set $\Pi$, one can construct a FSA with input alphabet $2^{\Pi}$ accepting all and only finite words over $2^\Pi$ that satisfy $\phi$, which is defined next.

\begin{definition}[\bf Finite State Automaton]
\label{def:buchi}
A (deterministic) finite state automaton (FSA) is a tuple $\mathbf{F} := (\mathcal{Q}_\mathrm{F},q_\mathrm{F}^0,\Sigma_\mathrm{F},\delta_\mathrm{F},\mathcal{F}_\mathrm{F})$, where %
\begin{itemize}
\item $\mathcal{Q}_\mathrm{F}$ is a finite set of states; %
\item $q_\mathrm{F}^0 \in \mathcal{Q}_\mathrm{F}$ is the initial state; %
\item $\Sigma_\mathrm{F}$ is an input alphabet; %
\item $\delta_\mathrm{F}: \mathcal{Q}_\mathrm{F} \times \Sigma_\mathrm{F} \times \mathcal{Q}_\mathrm{F}$ is a deterministic transition relation; %
\item $\mathcal{F}_\mathrm{F}\subseteq \mathcal{Q}_\mathrm{F}$ is a set of accepting (final) states.
\end{itemize}
\end{definition}
A \emph{run} of $\mathbf{F}$ over an input word $\omega=\omega^0\omega^1\ldots\omega^l$ where $\omega^i\in\Sigma_\mathrm{F}\;\forall i=0\ldots l$ is a sequence $r_\mathrm{F}=q^0 q^1\ldots q^lq^{l+1}$, such that $(q^i,\omega^i,q^{i+1}) \in \delta_\mathrm{F}\;\forall i=0\ldots l$ and $q^0=q^0_\mathrm{F}$.
An FSA $\mathbf{F}$ accepts a word over $\Sigma_\mathrm{F}$ if and only the corresponding run ends in some $q \in \mathcal{F}_\mathrm{F}$.

\begin{definition}[\bf Markov Decision Process]
\label{def:MDP}
A Markov decision process (MDP) is a tuple $\mathbf{P} := (\mathcal{Q}_\mathrm{P}, q_\mathrm{P}^0, \mathcal{A}_\mathrm{P}, \alpha_\mathrm{P}, \delta_\mathrm{P}, \Pi_\mathrm{P}, \mathcal{L}_\mathrm{P})$, where
\begin{itemize}
\item $\mathcal{Q}_\mathrm{P}$ is a finite set of states; %
\item $q_\mathrm{P}^0 \in \mathcal{Q}_\mathrm{P}$ is the initial state; %
\item $\mathcal{A}_\mathrm{P}$ is a finite set of actions; %
\item $\alpha_\mathrm{P}: \mathcal{Q}_\mathrm{P} \to 2^{\mathcal{A}_\mathrm{P}}$ is a map giving the set of actions available at a state;%
\item $\delta_\mathrm{P}: \mathcal{Q}_\mathrm{P} \times \mathcal{A}_\mathrm{P} \times \mathcal{Q}_\mathrm{P} \to [0,1]$ is the transition probability function that satisfies $\sum_{q'\in\mathcal{Q}_\mathrm{P}} \delta(q,a,q') = 1\; \forall q\in\mathcal{Q}_\mathrm{P}, a\in\alpha_\mathrm{P}(q)$ and $\sum_{q'\in\mathcal{Q}_\mathrm{P}} \delta(q,a,q') = 0\; \forall q\in\mathcal{Q}_\mathrm{P}, a\not\in\alpha_\mathrm{P}(q)$.%
\item $\Pi_\mathrm{P}$ is a finite set of atomic propositions; %
\item $\mathcal{L}_\mathrm{P}:\mathcal{Q}_\mathrm{P}\to 2^{\Pi_\mathrm{P}}$ is a map giving the set of atomic propositions satisfied in a state.%
\end{itemize}
\end{definition}
For an MDP $\mathbf{P}$, we define a stationary policy $\mu_\mathrm{P}: \mathcal{Q}_\mathrm{P} \to \mathcal{A}_\mathrm{P}$ such that for a state $q \in \mathcal{Q}_\mathrm{P}$, $\mu_\mathrm{P}(q) \in \alpha_\mathrm{P}(q)$.
This stationary policy can then be used to resolve all nondeterministic choices in $\mathbf{P}$ by applying action $\mu(q)$ at each $q \in \mathcal{Q}_\mathrm{P}$.
A path of $\mathbf{P}$ under policy $\mu_\mathrm{P}$ is a finite sequence of states $r_\mathrm{P}^{\mu_\mathrm{P}} = q^0q^1\ldots q^l$ such that $l\geq0$, $q^0 = q^0_\mathrm{P}$ and $\delta_\mathrm{P}(q^{k-1},\mu_\mathrm{P}(q^{k-1}),q^{k})>0$ $\forall k\in [1,l]$.
A path $r_\mathrm{P}^{\mu_\mathrm{P}}$ generates a finite word $\mathcal{L}_\mathrm{P}(r_\mathrm{P}^{\mu_\mathrm{P}}) = \mathcal{L}_\mathrm{P}(q^0)\mathcal{L}_\mathrm{P}(q^1)\ldots\mathcal{L}_\mathrm{P}(q^l)$ where $\mathcal{L}_\mathrm{P}(q^k)$ is the set of atomic propositions satisfied at state $q^k$.
Next, we use $Paths_\mathrm{P}^{\mu_\mathrm{P}}$ to denote the set of all paths of $\mathbf{P}$ under a policy $\mu_\mathrm{P}$.
Finally, we define $P^{\mu_\mathrm{P}}(\phi)$ as the probability of satisfying $\phi$ under policy $\mu_\mathrm{P}$.
\begin{remark}
Syntactically co-safe LTL formulas have infinite time semantics, thus they are actually interpreted over infinite words~\cite{AB-LEK-MYV:10}.
Measurability of languages satisfying LTL formulas is also defined for infinite words generated by infinite paths~\cite{CB-JPK:08}.
However, one can determine whether a given infinite word satisfies a syntactically co-safe LTL formula by considering only a finite prefix of it.
It can be easily shown that our above definition of $Paths^{\mu_\mathrm{P}}_\mathrm{P}$ inherits the same measurability property given in~\cite{CB-JPK:08}.
\end{remark}

\section{Problem Formulation and Approach \label{sec:problem}}

In this section we introduce the control synthesis problem with temporal constraints for a system that models a plant operating in the presence of probabilistic independent agents.

\subsection{System Model}

Consider a system consisting of a deterministic plant that we can control ({\it e.g.},\; a robot) and $n$ agents operating in an environment modeled by a graph $\mathcal{E} = (V, \rightarrow_\mathcal{E},\mathcal{L}_\mathcal{E},\Pi_\mathcal{E})$, where $V$ is the set of vertices, $\rightarrow_\mathcal{E} \subseteq V\times V$ is the set of edges, and $\mathcal{L}_\mathcal{E}$ is the labeling function that maps each vertex to a proposition in $\Pi_\mathcal{E}$.
For example, $\mathcal{E}$ can be the quotient graph of a partitioned environment, where $V$ is a set of labels for the regions in the partition and $\rightarrow_\mathcal{E}$ is the corresponding adjacency relation (see Figs.~\ref{fig:drawing},~\ref{fig:simple_models}).
Agent $i$ is modeled as an MC $\mathbf{M}_i = (\mathcal{Q}_i, q_i^0, \delta_i, \Pi_i, \mathcal{L}_i)$, with  $\mathcal{Q}_i\subseteq V$ and $\delta_i\subseteq\rightarrow_\mathcal{E}$, $i=1,\ldots,n$.
The plant is assumed to be a deterministic transition system TS $\mathbf{T} = (\mathcal{Q}_\mathrm{T},q_\mathrm{T}^0,\mathcal{A}_\mathrm{T},\alpha_\mathrm{T},\delta_\mathrm{T},\Pi_\mathrm{T},\mathcal{L}_\mathrm{T})$, where $\mathcal{Q}_\mathrm{T}\subseteq V$ and $\delta_t\subseteq\rightarrow_\mathcal{E}$.
We assume that all components of the system (the plant and the agents) make transitions synchronously by picking edges of the graph.
We also assume that the state of the system is perfectly known at any given instant and we can control the plant but we have no control over the agents.

\begin{figure}
\centering
	\includegraphics{crossing}
   \caption{A partitioned road environment, where a car (plant) is required to reach $c_4$ without colliding with any of the pedestrians (agents).}
   \label{fig:drawing}
\end{figure}

We define the sets of propositions and labeling functions of the individual components of the system such that they inherit the propositions of their current vertex from the graph while preserving their own identities. Formally, we have $\Pi_\mathrm{T}=\{(\mathrm{T},\mathcal{L}_\mathcal{E}(q)) | q\in \mathcal{Q}_\mathrm{T}\}$ and $\mathcal{L}_\mathrm{T}(q)=(\mathrm{T},\mathcal{L}_\mathcal{E}(q))$ for the plant, and $\Pi_i=\{(i,\mathcal{L}_\mathcal{E}(q))|q\in \mathcal{Q}_i\}$ and $\mathcal{L}_i(q)=(i,\mathcal{L}_\mathcal{E}(q))$ for agent $i$.
Finally, we define the set $\Pi$ of propositions as $\Pi=\Pi_\mathrm{T}\cup\Pi_i\cup\ldots\cup\Pi_n\subseteq\{(i,p) | i = \{\mathrm{T},0,\ldots,n\}, p\in\Pi_\mathcal{E}\}$.

\subsection{Problem Formulation\label{sec:sub:prob}}

As it will become clear in Sec. \ref{sec:sub:syn}, the joint behavior of the plant and agents in the graph environment can be modeled by the parallel composition of the TS and MC models described above, which takes the form of an MDP (see Def. \ref{def:MDP}).
Given a syntactically co-safe LTL formula $\phi$ over $\Pi$, our goal is to synthesize a policy for this MDP, which we will simply refer to as the {\it system}, such that the probability of satisfying $\phi$ is either maximized or above a given threshold.
Since we assume perfect state information, the plant can implement a control policy computed for the system, i.e,  based on
its state and the state of all the other agents. As a result, we will not distinguish between a control policy for the plant and a control policy for the system, and we will refer to it simply as {\em control policy}.
We can now formulate the main problem considered in this paper:

\begin{problem}
\label{prb:problem}
Given a system described by a plant $\mathbf{T}$ and a set of agents $\mathbf{M}_1,\ldots,\mathbf{M}_n$ operating on a graph $\mathcal{E}$, and given a specification in the form of a syntactically co-safe LTL formula $\phi$ over $\Pi$, synthesize a control policy $\mu^\star$ that satisfies the following objective: (a) If a probability threshold $p_{thr}$ is given, the probability that the system satisfies $\phi$ under $\mu^\star$ exceeds $p_{thr}$. (b) Otherwise, $\mu^\star$ maximizes the probability that the system satisfies $\phi$.
If no such policy exists, report failure.
\end{problem}

As will be shown in Sec.~\ref{sec:sub:comp}, the parallel composition of MDP and MC models also takes the form of an MDP.
Hence, our approach can easily accommodate the case where the plant is a Markov Decision Process.
We consider a deterministic plant only for simplicity of presentation.

\begin{example}
\label{exp:simple}
Fig.~\ref{fig:drawing} illustrates a car in a 5-cell environment with 5 pedestrians, where $\mathcal{L}_\mathcal{E}(v)=v$ for $v\in\{c_0,\ldots,c_4\}$.
Fig.~\ref{fig:simple_models} illustrates the TS $\mathbf{T}$ and the MCs $\mathbf{M}_1,\ldots,\mathbf{M}_5$ that model the car and the pedestrians.
The car is required to reach the end of the crossing ($c_4$) without colliding with any of the pedestrians.
To enforce this behavior, we write our specification as
\begin{equation}
\label{eqn:phi}
\phi := \left(\neg \bigvee_{i=1\ldots5,j=0\ldots4} ((\mathrm{T},c_j)\wedge (i,c_j)) \right) \,\mathcal{U}\,(\mathrm{T},c_4).
\end{equation}
The deterministic FSA that corresponds to $\phi$ is given in Fig.~\ref{fig:simple_fsa}, where $\mathtt{col}=\bigvee_{i=1\ldots5,j=0\ldots4} ((\mathrm{T},c_j)\wedge (i,c_j))$ and $\mathtt{end} = (\mathrm{T},c_4)$.
\end{example}

\begin{figure}
\subfigure{
	\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2cm]
	  \tikzstyle{every state}=[circle,thick,draw=blue!75,minimum size=6mm]

	  \node [initial,initial text=,state] (c0) at (0,2.4) {$c_0$};
	   \node [state] (c2) at (0,1.2){$c_2$};
	   \node [state,label=left:$\mathtt{end}$,label=below:$\mathbf{T}$] (c4) at (0,0) {$c_4$};

	   \path (c0) edge [loop right] node {wait} (c0)
	                     edge node [] {go} (c2)
	             (c2) edge [loop right] node {wait} (c2)
	                     edge node [] {go} (c4)
						 (c4) edge [loop right] node {wait} (c4);
	\end{tikzpicture}
}%
\subfigure{
	\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2cm]
	  \tikzstyle{every state}=[circle,thick,draw=blue!75,minimum size=6mm]

	   \node [initial,initial text=,state] (c1) at (0,2.4) {$c_1$};
	   \node [state] (c2) at (0,1.2){$c_2$};
	   \node [state,label=below:$\mathbf{M}_1 \ldots \mathbf{M}_4$] (c3) at (0,0) {$c_3$};

	   \path (c1) edge [loop right] node {$0.6$} (c1)
	                     edge node [] {$0.4$} (c2)
	             (c2) edge [loop right] node {$0.2$} (c2)
	                     edge node [] {$0.8$} (c3)
	             (c3) edge [loop right] node {$1$} (c3);
	\end{tikzpicture}
}%
\subfigure{
	\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2cm]
	  \tikzstyle{every state}=[circle,thick,draw=blue!75,minimum size=6mm]

	   \node [initial,initial text=,state] (c1) at (0,2.4) {$c_1$};
	   \node [state] (c2) at (0,1.2){$c_2$};
	   \node [state,label=below:$\mathbf{M}_5$] (c3) at (0,0) {$c_3$};

	   \path (c1) edge [loop right] node {$0.6$} (c1)
	                     edge [bend left] node {$0.4$} (c2)
	             (c2) edge [loop right] node {$0.2$} (c2)
	                     edge [bend left]  node{$0.4$} (c3)
	                     edge [bend left] node {$0.4$} (c1)
	             (c3) edge [loop right] node {$0.6$} (c3)
	                     edge [bend left] node {$0.4$} (c2);
	\end{tikzpicture}
}
   \caption{TS $\mathbf{T}$ and MCs $\mathbf{M}_1\ldots\mathbf{M}_5$ that model the car and the pedestrians.}
   \label{fig:simple_models}
\end{figure}

\begin{figure}
\centering
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2cm]
  \tikzstyle{every state}=[circle,thick,draw=blue!75,minimum size=6mm]

   \node [initial,initial text=,state,label=above:$\mathbf{F}$] (q0) at (0,0) {$q_0$};
   \node [state, double, ] (q1) at (2,0){$q_1$};
   \node [state] (q2) at (4,0) {$q_2$};

   \path (q0) edge [loop below] node {$\neg \mathtt{col} \wedge \neg \mathtt{end}$} (q0)
              edge node {$\mathtt{end}$} (q1)
			  edge [bend left] node {$\mathtt{col} \wedge \neg \mathtt{end}$} (q2)
             (q1) edge [loop below] node {$\top$} (q1)
             (q2) edge [loop below] node {$\top$} (q2);
\end{tikzpicture}
	\caption{Deterministic FSA $\mathbf{F}$ that corresponds to $\phi=\neg \mathtt{col}\,\mathcal{U}\,\mathtt{end}$ where $\mathtt{col}=\bigvee_{i=1\ldots5,j=0\ldots4} (c^\mathrm{T}_j\wedge c^i_j)$ and $\mathtt{end} = c^\mathrm{T}_4$. $q_0$ and $q_1$ are initial and final states, respectively.}
   \label{fig:simple_fsa}
\end{figure}

\subsection{Solution Outline\label{sec:sub:sol}}

One can directly solve Prob.~\ref{prb:problem} by reducing it to a Maximal Reachability Probability (MRP) problem on the MDP modeling the overall system~\cite{LDA:97}.
This approach, however, is very resource demanding as it scales exponentially with the number agents.
As a result, the environment size and the number of agents that can be handled in a reasonable time frame and with limited memory are small.
To address this issue, we propose a highly efficient incremental control synthesis method that exploits the independence between the system components and the fact that verification is less demanding than synthesis.
At each iteration $i$, our method will involve the following steps: synthesis of an optimal control policy considering only some of the agents (Sec.~\ref{sec:sub:syn}), verification of this control policy with respect to the complete system (Sec.~\ref{sec:sub:ver}) and minimization of the system model under the guidance of this policy (Sec.~\ref{sec:sub:min}).

\section{Problem Solution \label{sec:sol}}

Our solution to Prob.~\ref{prb:problem} is given in the form of Alg.~\ref{alg:ics}.
In the rest of this section, we explain each of its steps in detail.

\setlength{\algomargin}{1.5em}
\begin{algorithm}[h]
\DontPrintSemicolon
\SetInd{0.5em}{0.5em}
\KwIn{$\mathbf{T},\mathbf{M}_1,\ldots,\mathbf{M}_n, \phi, (p_{thr}).$}
\KwOut{$\mu^\star$ s.t. $P^{\mu^\star}(\phi) \geq P^{\mu}(\phi)\,\forall \mu$ if $p_{thr}$ is not given, otherwise $P^{\mu^\star}(\phi) > p_{thr}$.}
$\mathcal{M} \leftarrow \{\mathbf{M}_1,\ldots,\mathbf{M}_n\}$.\;
Construct FSA $\mathbf{F}$ corresponding to $\phi$.\;
$\mu^\star\leftarrow\emptyset,\,P_\mathcal{M}^{\mu^\star}(\phi)\leftarrow 0,\,\mathcal{M}_0 \leftarrow \emptyset,\,\mathbf{A}_0 \leftarrow \mathbf{T},\,i\leftarrow 1$.\;
Process $\phi$ to form $\mathcal{M}_i^{new}$.\;
\While{True} {
$\mathcal{M}_i \leftarrow \mathcal{M}_{i-1} \cup \mathcal{M}_i^{new}$.\;
$\mathbf{A}_i \leftarrow \mathbf{A}_{i-1} \otimes \mathcal{M}_i^{new}$.\;
$\mathbf{P}_i \leftarrow \mathbf{A}_i \otimes \mathbf{F}$.\;
Synthesize $\mu_i$ that maximizes $P^{\mu_i}_{\mathcal{M}_i}(\phi)$ using $\mathbf{P}_i$.\;
\If{$p_{thr}$ given}{
\If{$P^{\mu_i}_{\mathcal{M}_i}(\phi) < p_{thr}$}
{Fail: $\nexists \mu$ such that $P^{\mu}(\phi) \geq p_{thr}$.}
\ElseIf{$\mathcal{M}_i = \mathcal{M}$}
{Success: $\mu^\star \leftarrow \mu_i$, Return $\mu^\star$.}
\Else{Continue with verification on line 20.}
}
\ElseIf{$\mathcal{M}_i = \mathcal{M}$} {
{Success: $\mu^\star \leftarrow \mu_i$, Return $\mu^\star$.}
}
\Else{
Obtain the MC $\mathbf{M}^{\mu_i}_{\mathcal{M}_i}$ induced on $\mathbf{P}_i$ by $\mu_i$.\;
$\overline{\mathcal{M}_i} \leftarrow \mathcal{M} \setminus \mathcal{M}_i$.\;
$\mathbf{M}^{\mu_i}_{\mathcal{M}} \leftarrow \mathbf{M}^{\mu_i}_{\mathcal{M}_i}\otimes \overline{\mathcal{M}}_i$.\;
$\mathbf{V}_i \leftarrow \mathbf{M}^{\mu_i}_{\mathcal{M}}\otimes\mathbf{F}$.\;
Compute $P^{\mu_i}_\mathcal{M}(\phi)$ using $\mathbf{V}_i$.\;
\If{$P^{\mu_i}_\mathcal{M}(\phi) > P^{\mu^\star}_\mathcal{M}(\phi)$}{
$\mu^\star \leftarrow \mu_i,\,P^{\mu^\star}_\mathcal{M}(\phi)\leftarrow P^{\mu_i}_\mathcal{M}(\phi)$.
}
\If{$p_{thr}$ given and $P_\mathcal{M}^{\mu^\star}(\phi)>p_{thr}$} {
	Success: Return $\mu^\star$.
}
\Else{
	Set $\mathcal{M}_{i+1}^{new}$ to some agent $\mathbf{M}_j \in \overline{\mathcal{M}_i}$.\;
	Minimize $\mathbf{A}_i$.\;
	Increment $i$.\;
}
}
}
\caption{{\sc Incremental-Control-Synthesis}\label{alg:ics}}
\end{algorithm}

\subsection{Parallel Composition of System Components\label{sec:sub:comp}}

Given the set $\mathcal{M}=\{\mathbf{M}_1,\ldots,\mathbf{M}_n\}$ of all agents, we use $\mathcal{M}_i\subseteq\mathcal{M}$ to denote its subset used at iteration $i$.
Then, we define the synchronous parallel composition $\mathbf{T}\otimes\mathcal{M}_i$ of $\mathbf{T}$ and agents in $\mathcal{M}_i=\{\mathbf{M}_{i1},\ldots,\mathbf{M}_{ij}\}$ for different types of $\mathbf{T}$ as follows.

If $\mathbf{T}$ is a TS, then we define $\mathbf{T}\otimes\mathcal{M}_i$ as the MDP $\mathbf{A} = (\mathcal{Q}_\mathrm{A}, q_\mathrm{A}^0, \mathcal{A}_\mathrm{A}, \alpha_\mathrm{A}, \delta_\mathrm{A}, \Pi_\mathrm{A}, \mathcal{L}_\mathrm{A}) = \mathbf{T} \otimes \mathcal{M}_i$, such that
\begin{itemize}
\item $\mathcal{Q}_\mathrm{A} \subseteq \mathcal{Q}_\mathrm{T} \times \mathcal{Q}_{i1} \times \ldots \times \mathcal{Q}_{ij}$ such that a state $q=\langle q_\mathrm{T},q_{i1},\ldots,q_{ij}\rangle$ exists iff it is reachable from the initial states;
\item $q_\mathrm{A}^0 = \langle q_\mathrm{T}^0, q_{i1}^0, \ldots,q_{ij}^0\rangle$;
\item $\mathcal{A}_\mathrm{A} = \mathcal{A}_\mathrm{T}$;
\item $\alpha_\mathrm{A}(q) = \alpha_\mathrm{T}(q_\mathrm{T})$, where $q_\mathrm{T}$ is the element of $q$ that corresponds to the state of $\mathbf{T}$;
\item $\Pi_\mathrm{A} = \Pi_\mathrm{T}\cup\Pi_{i1}\cup\ldots\cup\Pi_{ij}$;
\item $\mathcal{L}_\mathrm{A}(q) = \mathcal{L}_\mathrm{T}(q_\mathrm{T}) \cup \mathcal{L}_{i1}(q_{i1}) \cup \ldots\cup \mathcal{L}_{ij}(q_{ij})$;
\item $\delta_\mathrm{A}(q=\langle q_\mathrm{T},q_{i1},\ldots,q_{ij}\rangle,a,q'=\langle q_\mathrm{T}',q_{i1}',\ldots,q_{ij}'\rangle) = 1\{(q_\mathrm{T},a,q_\mathrm{T}') \in \delta_T\}\times\delta(q_{i1},q_{i1}')\times\ldots\times\delta(q_{ij},q_{ij}')$,
\end{itemize}
where $1\{\cdot\}$ is the indicator function.

If $\mathbf{T}$ is an MDP, then we define $\mathbf{T}\otimes\mathcal{M}_i$ as the MDP $\mathbf{A} = (\mathcal{Q}_\mathrm{A}, q_\mathrm{A}^0, \mathcal{A}_\mathrm{A}, \alpha_\mathrm{A}, \delta_\mathrm{A}, \Pi_\mathrm{A}, \mathcal{L}_\mathrm{A}) = \mathbf{T} \otimes \mathcal{M}_i$, such that $\mathcal{Q}_\mathrm{A}$, $q_\mathrm{A}^0$, $\mathcal{A}_\mathrm{A}$, $\alpha_\mathrm{A}$, $\Pi_\mathrm{A}$, and $\mathcal{L}_\mathrm{A}$ are as given in the case where $\mathbf{T}$ is a TS and
\begin{itemize}
	\item $\delta_\mathrm{A}(q=\langle q_\mathrm{T},q_{i1},\ldots,q_{ij}\rangle,a,q'=\langle q_\mathrm{T}',q_{i1}',\ldots,q_{ij}'\rangle) = \delta_\mathrm{T}(q_\mathrm{T},a,q_\mathrm{T}')\times\delta_{i1}(q_{i1},q_{i1}')\times\ldots\times\delta_{ij}(q_{ij},q_{ij}')$.
\end{itemize}

Finally if $\mathbf{T}$ is an MC, then we define $\mathbf{T}\otimes\mathcal{M}_i$ as the MC $\mathbf{A} = (\mathcal{Q}_\mathrm{A}, q_\mathrm{A}^0, \delta_\mathrm{A}, \Pi_\mathrm{A}, \mathcal{L}_\mathrm{A}) = \mathbf{T} \otimes \mathcal{M}_i$ where $\mathcal{Q}_\mathrm{A}$, $q_\mathrm{A}^0$, $\Pi_\mathrm{A}$, $\mathcal{L}_\mathrm{A}$ are as given in the case where $\mathbf{T}$ is a TS and
\begin{itemize}
	\item $\delta_\mathrm{A}(q=\langle q_\mathrm{T},q_{i1},\ldots,q_{ij}\rangle,q'=\langle q_\mathrm{T}',q_{i1}',\ldots,q_{ij}'\rangle) = \delta_\mathrm{T}(q_\mathrm{T},q_\mathrm{T}')\times\delta_{i1}(q_{i1},q_{i1}')\times\ldots\times\delta_{ij}(q_{ij},q_{ij}')$.
\end{itemize}

\subsection{Product MDP and Product MC\label{sec:sub:prod}}

Given the deterministic FSA $\mathbf{F}$ that recognizes all and only the finite words that satisfy $\phi$, we define the product of $\mathbf{M}\otimes\mathbf{F}$ for different types of $\mathbf{M}$ as follows.

If $\mathbf{M}$ is an MDP, we define $\mathbf{M}\otimes\mathbf{F}$ as the product MDP $\mathbf{P} = (\mathcal{Q}_\mathrm{P}, q_\mathrm{P}^0, \mathcal{A}_\mathrm{P}, \alpha_\mathrm{P}, \delta_\mathrm{P}, \Pi_\mathrm{P}, \mathcal{L}_\mathrm{P}) = \mathbf{M} \otimes \mathbf{F}$, where
\begin{itemize}
\item $\mathcal{Q}_\mathrm{P} \subseteq \mathcal{Q}_\mathrm{M} \times \mathcal{Q}_\mathrm{F}$ such that a state $q$ exists iff it is reachable from the initial states;
\item $q_\mathrm{P}^0 = \langle q_\mathrm{M}^0,q_\mathrm{F}\rangle$ such that $(q_\mathrm{F}^0,\mathcal{L}_\mathrm{M}(q_\mathrm{M}),q_\mathrm{F})\in\delta_\mathrm{F}$;
\item $\mathcal{A}_\mathrm{P} = \mathcal{A}_\mathrm{M}$;
\item $\alpha_\mathrm{P}(\langle q_\mathrm{M},q_\mathrm{F}\rangle) = \alpha_\mathrm{M}(q_\mathrm{M})$;
\item $\Pi_\mathrm{P} = \Pi_\mathrm{M}$;
\item $\mathcal{L}_\mathrm{P}(\langle q_\mathrm{M},q_\mathrm{F}\rangle) = \mathcal{L}_\mathrm{M}(q_\mathrm{M})$;
\item $\delta_\mathrm{P}(\langle q_\mathrm{M},q_\mathrm{F}\rangle,a,\langle q_\mathrm{M}',q'_\mathrm{F}\rangle) = 1\{(q_\mathrm{F},\mathcal{L}_\mathrm{M}(q_\mathrm{M}'),q_\mathrm{F}')\in\delta_\mathrm{F}\}$ $\times \delta_\mathrm{M}(q_\mathrm{M},a,q_\mathrm{M}')$,
\end{itemize}
where $1\{\cdot\}$ is the indicator function.
In this product MDP, we also define the set $\mathcal{F}_\mathrm{P}$ of final states such that a state $q=\langle q_\mathrm{M},q_\mathrm{F}\rangle \in \mathcal{F}_\mathrm{P}$ iff $q_\mathrm{F} \in \mathcal{F}_\mathrm{F}$, where $\mathcal{F}_\mathrm{F}$ is the set of final states of $\mathbf{F}$.

If $\mathbf{M}$ is an MC, we define $\mathbf{M}\otimes\mathbf{F}$ as the product MC $\mathbf{P} = (\mathcal{Q}_\mathrm{P}, q_\mathrm{P}^0, \delta_\mathrm{P}, \Pi_\mathrm{P}, \mathcal{L}_\mathrm{P}) = \mathbf{M} \otimes \mathbf{F}$ where $\mathcal{Q}_\mathrm{P}$, $q_\mathrm{P}^0$, $\Pi_\mathrm{P}$, $\mathcal{L}_\mathrm{P}$ are as given in the case where $\mathbf{M}$ is an MDP and
\begin{itemize}
	\item $\delta_\mathrm{P}(\langle q_\mathrm{M},q_\mathrm{F}\rangle,\langle q_\mathrm{M}',q'_\mathrm{F}\rangle) = 1\{(q_\mathrm{F},\mathcal{L}_\mathrm{M}(q_\mathrm{M}'),q_\mathrm{F}')\in\delta_\mathrm{F}\}\times\delta_\mathrm{M}(q_\mathrm{M},q_\mathrm{M}')$.
\end{itemize}
In this product MC, we also define the set $\mathcal{F}_\mathrm{P}$ of final states as given above.

\subsection{Initialization\label{sec:sub:init}}

Lines 1 to 4 of Alg.~\ref{alg:ics} correspond to the initialization procedure of our algorithm.
First, we form the set $\mathcal{M}=\{\mathbf{M}_1,\ldots,\mathbf{M}_n\}$ of all agents and construct the FSA $\mathbf{F}$ that corresponds to $\phi$.
Such $\mathbf{F}$ can be automatically constructed using existing tools, {\it e.g.},\; \cite{Latvala:EMC2003}.
Since we have not synthesized any control policies so far, we reset the variable $\mu^\star$ that holds the best policy at any given iteration and set the probability $P^{\mu^\star}_\mathcal{M}(\phi)$ of satisfying $\phi$ under policy $\mu^\star$ in the presence of agents in $\mathcal{M}$ to 0.
As we have not considered any agents so far, we set the subset $\mathcal{M}_0$ to be an empty set.
We then set $\mathbf{A}_0$, which stands for the parallel composition of the plant $\mathbf{T}$ and the agents in $\mathcal{M}_0$, to $\mathbf{T}$.
We also initialize the iteration counter $i$ to 1.

Line 4 of Alg.~\ref{alg:ics} initializes the set $\mathcal{M}_1^{new}$ of agents that will be considered in the synthesis step of the first iteration of our algorithm.
In order to be able to guarantee completeness, we require this set to be the maximal set of agents that satisfy the mission, {\it i.e.},\; the agent subset that can satisfy $\phi$ but not strictly needed to satisfy $\phi$.
To form $\mathcal{M}_1^{new}$, we first rewrite $\phi$ in positive normal form to obtain $\phi_{pnf}$, where the negation operator $\neg$ occurs only in front of atomic propositions.
Conversion of $\phi$ to $\phi_{pnf}$ can be performed automatically using De Morgan's laws and equivalences for temporal operators as given in \cite{CB-JPK:08}.
Then, using this fact, we include an agent $\mathbf{M}_i\in\mathcal{M}$ in $\mathcal{M}_1^{new}$ if any of its corresponding propositions of the form $(i,p),p \in \Pi_i$ appears non-negated in $\phi_{pnf}$.
For instance, given $\phi := \neg ((3,\mathtt{p3})\wedge(\mathrm{T},\mathtt{p3}))\,\mathcal{U}\,((1,\mathtt{p1}) \vee (2,\mathtt{p2}))$, either one of agents $\mathbf{M}_1$ and $\mathbf{M}_2$ can satisfy the formula, whereas agent $\mathbf{M}_3$ can only violate it.
Therefore, for this example we set $\mathcal{M}_1^{new} = \{\mathbf{M}_1,\mathbf{M}_2\}$.
In case $\mathcal{M}_1^{new}=\emptyset$ after this procedure, we form $\mathcal{M}_1^{new}$ arbitrarily by including some agents from $\mathcal{M}$ and proceed with the synthesis step of our approach.

\subsection{Synthesis\label{sec:sub:syn}}
Lines 6 to 19 of Alg.~\ref{alg:ics} correspond to the synthesis step of our algorithm.
At the $i^{th}$ iteration, the agent subset that we consider is given by $\mathcal{M}_i = \mathcal{M}_{i-1} \cup \mathcal{M}_i^{new}$ where $\mathcal{M}_i^{new}$ contains the agents that will be newly considered as provided by the previous iteration's verification stage or by the initialization procedure given in Sec.~\ref{sec:sub:init} if $i$ is 1.
First, we construct the parallel composition $\mathbf{A}_i = \mathbf{A}_{i-1} \otimes \mathcal{M}_i^{new}$ of our plant and the agents in $\mathcal{M}_i$ as described in Sec.~\ref{sec:sub:comp}.
Notice that, we use $\mathbf{A}_{i-1}$ to save from computation time and memory as $\mathbf{A}_{i-1} \otimes \mathcal{M}_i^{new}$ is typically smaller than $\mathbf{T} \otimes \mathcal{M}_i$ due to the minimization procedure explained in Sec.~\ref{sec:sub:min}.
Next, we construct the product MDP $\mathbf{P}_i = \mathbf{A}_i \otimes \mathbf{F}$ as explained in Sec.~\ref{sec:sub:prod}.
Then, our control synthesis problem can be solved by solving a maximal reachability probability (MRP) problem on $\mathbf{P}_i$ where one computes the maximum probability of reaching the set $\mathcal{F}_\mathrm{P}$ from the initial state $q_\mathrm{P}^0$~\cite{LDA:97}, after which the corresponding optimal control policy $\mu_i$ can be recovered as given in \cite{CB-JPK:08,DiSmBeRu-CDC-2011}.
Consequently, at line 9 of Alg.~\ref{alg:ics} we solve the MRP problem on $\mathbf{P}_i$ using value iteration to obtain optimal policy $\mu_i$ that maximizes the probability of satisfaction of $\phi$ in the presence of the agents in $\mathcal{M}_i$.
We denote this probability by $P_{\mathcal{M}_i}^{\mu_i}(\phi)$, whereas $P^{\mu}(\phi)$ stands for the probability that the complete system satisfies $\phi$ under policy $\mu$.

The steps that we take at the end of the synthesis, {\it i.e.},\; lines 10 to 19 of Alg.~\ref{alg:ics}, depends on whether $p_{thr}$ is given or not.
At any iteration $i$, if $p_{thr}$ is given and $P^{\mu_i}_{\mathcal{M}_i}(\phi) < p_{thr}$, we terminate by reporting that there exists no control policy $\mu : P^\mu(\phi) \geq p_{thr}$ which is a direct consequence of Prop.~\ref{prp:syn}.
If $p_{thr}$ is given and $P^{\mu_i}_{\mathcal{M}_i}(\phi)\geq p_{thr}$, we consider the following cases.
If $\mathcal{M}_i=\mathcal{M}$, we set $\mu^\star$ to $\mu_i$ and return $\mu^\star$ as it satisfies the probability threshold.
Otherwise, we proceed with the verification of $\mu_i$ as there are remaining agents that were not considered during synthesis and can potentially violate $\phi$.
For the case where $p_{thr}$ is not given we consider the current agent subset $\mathcal{M}_i$.
If $\mathcal{M}_i=\mathcal{M}$ we terminate and return $\mu^\star$ as there are no agents left to consider.
Otherwise, we proceed with the verification stage.

\begin{proposition}
\label{prp:syn}
The sequence $\{P^{\mu_i}_{\mathcal{M}_i}(\phi)\}$ is non-increasing.
\end{proposition}
\begin{proof}
As given in Sec.~\ref{sec:sub:init}, $\mathcal{M}_1$ includes all those agents that can satisfy the propositions that lead to satisfaction of $\phi$.
Let $pref(\phi)$ be the set of finite words that satisfy $\phi$ and let MC $\mathbf{M}_j$ of agent $j$ be such that $\mathbf{M}_j \not \in \mathcal{M}_1$.
Consider a finite satisfying word $\sigma$ such that $\sigma = \sigma^0 \sigma^1 \ldots \sigma^l \in pref(\phi)$.
Suppose there exists an index $k \in \{0,\ldots,l\}$ such that for some $q \in \mathcal{Q}_j$ and $\mathcal{L}_j(q) \in \sigma^k$.
Then, $\tilde{\sigma} = \sigma^0 \sigma^1 \ldots \sigma^{k-1} \tilde{\sigma}^k \sigma^{k+1} \ldots \sigma^l$ is also in $pref(\phi)$ where $\tilde{\sigma}^k = \sigma^k \setminus \mathcal{L}_j(q)$.
Now, let $r = q^0 q^1 \ldots q^l$ be a path of the system after including $\mathbf{M}_j$.
Let $\omega = \mathcal{L}(r) = \omega^0 \omega^1 \ldots \omega^l$ be the word generated by $r$.
If $\omega$ satisfies $\phi$, then $\tilde{\omega} = \tilde{\omega}^0 \tilde{\omega}^1 \ldots \tilde{\omega}^l$ also satisfies $\phi$ where $\tilde{\omega}^k = \omega^k \setminus \mathcal{L}_j(q_j^k)$ for each $k\in\{0,\ldots,l\}$ and $q_j^k$ is the state of $\mathbf{M}_j$ in $q^k$.
Thus, we conclude that the set of paths that satisfy $\phi$ cannot increase after we add agent $\mathbf{M}_j \in \mathcal{M}\setminus\mathcal{M}_1$, and the sequence $\{P^{\mu_i}_{\mathcal{M}_i}(\phi)\}$ is non-increasing such that it attains its maximum value $P^{\mu_1}_{\mathcal{M}_1}(\phi)$ at the first iteration and does not increase as more agents from $\mathcal{M}\setminus\mathcal{M}_1$ are considered in the following iterations.
\end{proof}

\begin{corollary}
	If at any iteration $P^{\mu_i}_{\mathcal{M}_i}(\phi) < p_{thr}$, then there does not exist a policy $\mu : P^\mu(\phi) \geq p_{thr}$, where $\mu_i$ is an optimal control policy that we compute at the synthesis stage of the $i^{th}$ iteration considering only the agents in $\mathcal{M}_i$.
\end{corollary}

\subsection{Verification and Selection of $\mathcal{M}_{i+1}^{new}$\label{sec:sub:ver}}
Lines 20 to 30 of Alg.~\ref{alg:ics} correspond to the verification stage of our algorithm.
In the verification stage, we verify the policy $\mu_i$ that we have just synthesized considering the entire system and accordingly update the best policy so far, which we denote by $\mu^\star$.

Note that $\mu_i$ maximizes the probability of satisfying $\phi$ in the presence of agents in $\mathcal{M}_i$ and induces an MC by resolving all non-deterministic choices in $\mathbf{P}_i$.
Thus, we first obtain the induced Markov Chain $\mathbf{M}^{\mu_i}_{\mathcal{M}_i}$ that captures the joint behavior of the plant and the agents in $\mathcal{M}_i$ under policy $\mu_i$.
Then, we proceed by considering the agents that were not considered during synthesis of $\mu_i$, {\it i.e.},\; agents in $\overline{\mathcal{M}_i} = \mathcal{M} \setminus \mathcal{M}_i$.
In order to account for the existence of the agents that we newly consider, we exploit the independence between the systems and construct the MC $\mathbf{M}^{\mu_i}_{\mathcal{M}} = \mathbf{M}^{\mu_i}_{\mathcal{M}_i}\otimes \overline{\mathcal{M}}_i$ in line 22.
In lines 23 and 24 of Alg.~\ref{alg:ics}, we construct the product MC $\mathbf{V}_i=\mathbf{M}^{\mu_i}_{\mathcal{M}}\otimes\mathbf{F}$ and compute the probability $P^{\mu_i}_\mathcal{M}(\phi)$ of satisfying $\phi$ in the presence of all agents in $\mathcal{M}$ by computing the probability of reaching $\mathbf{V}_i$'s final states from its initial state using value iteration.
Finally, in lines 25 and 26 we update $\mu^\star$  so that $\mu^\star = \mu_i$ if $P^{\mu_i}_\mathcal{M}(\phi) > P^{\mu^\star}_\mathcal{M}(\phi)$, {\it i.e.},\; if we have a policy that is better than the best we have found so far.
Notice that, keeping track of the best policy $\mu^\star$ makes Alg.~\ref{alg:ics} an anytime algorithm, {\it i.e.},\; the algorithm can be terminated as soon as some $\mu^\star$ is obtained.

At the end of the verification stage, if $p_{thr}$ is given and $P_\mathcal{M}^{\mu^\star}(\phi) \geq p_{thr}$ we terminate and return $\mu^\star$, as it satisfies the given probability threshold.
Otherwise in line 30 of Alg.~\ref{alg:ics}, we pick an arbitrary $\mathbf{M}_j \in \overline{\mathcal{M}}_i$ to be included in $\mathcal{M}^{i+1}$, which we call the {\em random agent first (RAF)} rule.
Note that, one can also choose to pick the smallest $\mathbf{M}_j$ in terms of state and transition count to minimize the overall computation time, which we call the {\em smallest agent first (SAF)} rule.

\begin{proposition}
\label{prp:ver}
The sequence $\{P_\mathcal{M}^{\mu^\star}(\phi)\}$ is a non-decreasing sequence.
\end{proposition}
\begin{proof}
The result directly follows from the fact that $\mu^\star$ is set to $\mu_i$ if and only if $P^{\mu_i}_\mathcal{M}(\phi) > P^{\mu^\star}_\mathcal{M}(\phi)$.
\end{proof}

\subsection{Minimization\label{sec:sub:min}}
The minimization stage of our approach (line 31 in Alg.~\ref{alg:ics}) aims to reduce the overall resource usage by removing those transitions and states of $\mathbf{A}_i$ that are not needed in the subsequent iterations.
We first set the minimization threshold $p_{min}$ to $p_{thr}$ if given, otherwise we set it to $P^{\mu^\star}_\mathcal{M}(\phi)$.
Next, we iterate over the states of $\mathbf{P}_i$ and check the maximum probability of satisfying the mission under each available action.
Note that, the value iteration that we perform in the synthesis step already provides us with the maximum probability of satisfying $\phi$ from any state in $\mathbf{P}_i$.
Then, we remove an action $a$ from state $q_\mathrm{A}$ in $\mathbf{A}_i$ if for all $q_\mathrm{F} \in Q_\mathrm{F}$, the maximum probability of satisfying the mission by taking action $a$ at $\langle q_\mathrm{A}, q_\mathrm{F}\rangle$ in $\mathbf{P}_i$ is below $p_{min}$.
After removing the transitions corresponding to all such actions, we also prune any orphan states in $\mathbf{A}_i$, {\it i.e.},\; states that are not reachable from the initial state.
Then, we proceed with the synthesis stage of the next iteration.

\begin{proposition}
\label{prp:min}
Minimization phase does not affect the correctness and the completeness of our approach.
\end{proposition}
\begin{proof}
To prove the correctness, we need to show that for an arbitrary policy $\mu$ on the minimized MDP $\mathbf{A}_{min}$, the probability that $\mathbf{A}_{min}$ satisfies $\phi$ under $\mu$ is equal to the probability that $\mathbf{A}$ satisfies $\phi$ under $\mu$ where $\mathbf{A}$ is the original MDP before minimization.
Correctness, in this case, follows directly from the fact that, in each state $q$, we do not modify the transition probabilities associated with an action that is enabled in $q$ after minimization.
Thus, it remains to show that minimization does not affect the completeness of the approach.
We first consider the removal of orphaned states.
Since these states cannot be reached from the initial state, they also will not be a part of any feasible control policy, and their removal does not affect the completeness of the approach.
Finally, we consider the removal of those actions that drive the system to the set of target states with probability smaller than the minimization threshold.
For the case where we use $p_{thr}$, completeness is not affected as we remove only those transitions that we would not take as we are looking for control policies with $P^\mu_\mathcal{M}(\phi) \geq p_{thr}$ and $P^{\mu_i}_{\mathcal{M}_i}$ is a non-increasing sequence (Prop.~\ref{prp:syn}).
For the case where we use $P^{\mu^\star}_\mathcal{M}$, we also remove those transitions that we would not take as $P^{\mu^\star}_\mathcal{M}$ is a non-decreasing sequence (Prop.~\ref{prp:ver}).
Hence, the minimization procedure does not affect the completeness of the overall approach as well.
\end{proof}

We finally show that Alg.~\ref{alg:ics} correctly solves Prob.~\ref{prb:problem}.

\begin{proposition}
Alg.~\ref{alg:ics} solves Prob.~\ref{prb:problem}.
\end{proposition}
\begin{proof}
Alg.~\ref{alg:ics} combines all the steps given in this section and synthesizes a control policy $\mu^\star$ that either ensures $P^{\mu^\star}(\phi) \geq p_{thr}$ if $p_{thr}$ is given, or maximizes $P^{\mu^\star}(\phi)$.
If Alg.~\ref{alg:ics} terminates in line 12, completeness is guaranteed by the fact that $P^{\mu_i}_{\mathcal{M}_i}$ is a non-increasing sequence as given in Prop.~\ref{prp:syn}.
Also, as given in Prop.~\ref{prp:min}, minimization stage does not affect the correctness and completeness of the approach.
Thus, Alg.~\ref{alg:ics} solves Prob.~\ref{prb:problem}.
\end{proof}

\section{Experimental Results\label{sec:impl}}

\begin{figure}
\subfigure{
	\centering
	\includegraphics[width=0.9\linewidth]{comp_time}
}
\subfigure{
	\centering
	\includegraphics[width=0.9\linewidth]{state_cnt}
}
\caption{Comparison of the classical single-pass and proposed incremental algorithms. The top plot shows the running times of the algorithms and the probabilities of satisfying $\phi$ under synthesized policies. The bottom plot compares the state counts of the product MDPs on which the MRP problem was solved in both approaches (black and red lines) and shows the state count of the product MC considered in the verification stage of our incremental algorithm (red dashed line).\label{fig:results}}
\end{figure}

In this section we return to the pedestrian crossing problem given in Example~\ref{exp:simple} and illustrated in Figs.~\ref{fig:drawing}, \ref{fig:simple_models}.
The mission specification $\phi$ for this example is given in Eq.~\eqref{eqn:phi}.
In the following, we compare the performance of our incremental algorithm with the performance of the classical method that attempts to solve this problem in a single pass using value iteration as in \cite{LDA:97}.

In our experiments we used an iMac i5 quad-core desktop computer and considered C++ implementations of both approaches.
During the experiments, our algorithm picked the new agent $\mathcal{M}_i^{new}$ to be considered at the next iteration in the following order: $\mathbf{M}_1,\mathbf{M}_2,\mathbf{M}_3,\mathbf{M}_4,\mathbf{M}_5$, {\it i.e.},\; according to the smallest agent first rule given in Sec.~\ref{sec:sub:ver}.

When no $p_{thr}$ was given, optimal control policies synthesized by both of the algorithms satisfied $\phi$ with a probability of 0.8.
The classical approach solved the control synthesis problem in 6.75 seconds, and the product MDP on which the MRP problem was solved had 1004 states and 26898 transitions.
In comparison, our incremental approach solved the same problem in 4.44 seconds, thanks to the minimization stage of our approach, which reduced the size of the problem at every iteration by pruning unneeded actions and states.
The largest product MDP on which the MRP problem was solved in the synthesis stage of our approach had 266 states and 4474 transitions.
The largest product MC that was considered in the verification stage of our approach had 405 states and 6125 transitions.
The probabilities of satisfying $\phi$ under policy $\mu_i$ obtained at each iteration of our algorithm were $P^{\mu_1}_\mathcal{M}(\phi) = 0.463$, $P^{\mu_2}_\mathcal{M}(\phi) = 0.566$, $P^{\mu_3}_\mathcal{M}(\phi) = 0.627$, $P^{\mu_4}_\mathcal{M}(\phi) = 0.667$, and $P^{\mu_5}_\mathcal{M}(\phi) = 0.8$.
When $p_{thr}$ was given as 0.65, our approach finished in 3.63 seconds and terminated after the fourth iteration returning a sub-optimal control policy with a 0.667 probability of satisfying $\phi$.
In this case, the largest product MDP on which the MRP problem was solved had only 99 states and 680 transitions.
Furthermore, since our algorithm runs in an anytime manner, it could be terminated as soon as a control policy was available, {\it i.e.},\; at the end of the first iteration (1.25 seconds).
Fig.~\ref{fig:results} compares the classical single-pass approach with our incremental algorithm in terms of running time and state counts of the product MDPs and MCs.

It is interesting to note that state count of the product MDP considered in the synthesis stage of our algorithm increases as more agents are considered, whereas state count of the product MC considered in the verification stage of our algorithm decreases as the minimization stage removes unneeded states and transitions after each iteration.
It must also be noted that, $|\mathcal{M}_1|$, {\it i.e.},\; cardinality of the initial agent subset, is an important factor for the performance of our algorithm.
As discussed in this section, for $|\mathcal{M}_1| << |\mathcal{M}|$ our algorithm outperforms the classical method both in terms of running time and memory usage.
However, for $|\mathcal{M}_1|\sim|\mathcal{M}|$ we expect the resource usage of our algorithm to be close to that of the classical approach, as in this case almost all of the agents will be considered in the synthesis stage of the first iteration.
We plan to address this issue in future work. %
Nevertheless, most typical finite horizon \emph{safety} missions, where the plant is expected to reach a goal while avoiding a majority or all of the agents, already satisfy the condition $|\mathcal{M}_1| << |\mathcal{M}|$.

\section{Conclusions \label{sec:conclusions}}
In this paper we presented a highly efficient incremental method for automatically synthesizing optimal control policies for a system comprising a plant and multiple independent agents, where the plant is expected to satisfy a high level mission specification in the presence of the agents.
We considered independent agents modeled as Markov chains and assumed that the plant was modeled as a deterministic transition system.
However, our approach is general enough to accommodate plants modeled as Markov Decision Processes.
For mission specifications, we considered syntactically co-safe Linear Temporal Logic formulas over a set of propositions that are satisfied by the components of the system.
If a probability threshold is given, our method exploits this knowledge to terminate earlier and returns a sub-optimal control policy.
Otherwise, our method synthesizes an optimal control policy that maximizes the probability of satisfying the mission.
Since our method does not need to run to completion, it has practical value in applications where a safe control policy must be synthesized under resource constraints.
For future work, we plan to extend our approach to mission specifications expressed in full LTL as opposed to a subset of it.

\bibliographystyle{IEEEtran}

redpajama_set_name: RedPajamaArXiv


text:
mkdir -p "$PREFIX/bin"
export MACHTYPE=x86_64
export BINDIR=$(pwd)/bin
export L="${LDFLAGS}"
mkdir -p "$BINDIR"
(cd kent/src/lib && make)
(cd kent/src/htslib && make)
(cd kent/src/jkOwnLib && make)
(cd kent/src/hg/lib && make)
(cd kent/src/utils/twoBitDup && make)
cp bin/twoBitDup "$PREFIX/bin"
chmod +x "$PREFIX/bin/twoBitDup"

redpajama_set_name: RedPajamaGithub


text:
'The Chilling Adventures of Sabrina' in Development at The CW
Spencer Barrett @spencerbarrett September 20, 2017 / 4:17 PM
Photo courtesy Archie Comics
Hold on to your brooms – Sabrina the Teenage Witch will soon be flying back to television. The Hollywood Reporter has announced a series based on The Chilling Adventures of Sabrina – a darker comic book take on the Sabrina story – is in the works at The CW.
Developed in partnership with Warner Bros. Television, the potential one-hour series is a far departure from the spunky Sabrina the Teenage Witch which ran on ABC, and later the WB, from 1996-2003.
The CW's project, described tonally as Rosemary's Baby meets The Exorcist, reimagines the classic Archie Comics character Sabrina as a dark coming-of-age story deals with horror, the occult, and witchcraft, and will see Sabrina struggle to reconcile her dual nature of being half-witch and half-mortal while protecting her family and the world from the forces of evil.
The television adaption will be written by Riverdale showrunner Roberto Aguirre-Sacasa, who also writes the comic book series. Lee Toland-Krieger, who directed multiple episodes of Riverdale's freshman run, is set to helm the Sabrina pilot should The CW opt to move forward with production. Joining Aguirre-Sacasa in producing roles will be Riverdale mainstays Greg Berlanti, Sarah Schechter, and Archie Comics CEO Jon Goldwater.
The new project is eyed to debut in The CW's 2018-19 television season as a companion to Riverdale. Casting and additional news on the new series will be revealed in the months to come.
Tagged: Development Pilot News Sabrina the Teenage Witch The Chilling Adventures of Sabrina The CW	Share
Spencer Barrett
Stars are his kind of thing! Spencer Barrett joined the TV Source team as a staff writer in 2013. In 2018, he was promoted to Senior Writer, TV & Pop Culture, shaping our pop culture content. He loves all things horror, Archie Comics and Taylor Swift.
@spencerbarrett
5 Teasers for 'Chilling Adventures of Sabrina: Part 4'
Netflix Reveals Official Trailer for 'Chilling Adventures of Sabrina: Part 4'
Prepare for 'WandaVision' with New Disney+ Original Series 'Marvel Studios: Legends'
'Cobra Kai' Season 3 Original Score Available for Pre-Order
Previous Story Days of our Lives Week in Review: Makes Sense to Me
Next Story General Hospital Spoilers: September 25-29, 2017 Edition
TV News December 24, 2020 December 24, 2020
'Cobra Kai' Season 3 Releasing Early on Netflix
The holidays just got a little more badass. Cobra Kai season 3 will now arrive…
TV News December 9, 2020 December 9, 2020
Choose Your Side in First Trailer for 'Cobra Kai' Season 3
New year, new season, highest stakes ever. Netflix just released the first trailer for the…
POPCultureTV News December 1, 2020 December 1, 2020
Gifts and Merchandise Every 'Cobra Kai' Fan Will Love
There's no denying that Cobra Kai has been a huge success since moving from YouTube…
TV News October 26, 2020 October 26, 2020
Get ready, witches — Netflix has announced that Chilling Adventures of Sabrina: Part 4 will…
TV News October 2, 2020 October 2, 2020
Netflix Reveals 'Cobra Kai' Season 3 Premiere Date, Season 4 Renewal
Return to the dojo in 2021. Cobra Kai will return for its third season on…

redpajama_set_name: RedPajamaCommonCrawl


Please be advised that the Oprah Magazine customer service number does not directly connect you with Oprah Winfrey herself. At least I don't think it does. Maybe you should try it. Wouldn't that be great if you did get her on the phone, and she gave you a car? Seriously, there are many ways to contact customer service reps for O!. Read on to find out how.
Seriously, this is not an easy number to find. To reach the customer service department, call 866-399-6820. This number is not publicized very much, so I don't know what kind of customer service support you can receive here. I think you can join Oprah's Circle of Friends through this number. Members receive a welcome box, two seasonal beauty boxes, a deluxe subscription to O, a gift subscription to O, a weekly newsletter, O insider access, and a birthday card from Oprah herself.
Do you have a specific question or comment regarding your subscription? Fill out the customer service form here: https://w1.buysub.com/pubs/HR/OPR/OPR_keyed_email_external_contact.jsp?lsid=81641433221026832&vid=3&cds_mag_code=OPR&cds_to_id=contact&cslogin=N.
If you are having technical problems with the O! website, email mailto:techsupport@own.oprah.com.
Do you want to hang out for a weekend with Oprah? Contact someone from the Oprah's The Life You Want Weekend department at mailto:contactus@oprahweekend.com.
To share an opinion about something you read in the Oprah Magazine, fill out the following contact information: https://www.oprah.com/plug_sg.html?plug_id=s3/3627627/What-s-your-opinion.
To send a message to the editors of the magazine, email mailto:letters@hearst.com.
The Oprah Magazine does not offer a live chat option.
There are two different sides of the Oprah Magazine contact information. The editorial and creative people are in New York. To receive help regarding content, check out this page: https://www.oprah.com/app/helpfaq.html – anchor_contactus. Find out how to create a profile and access your account settings, share a comment with an editor, live stream videos from Oprah, and obtain information regarding Oprah's Book Club.
To receive information and help regarding the magazine subscription, find the answer to your question on this page: https://w1.buysub.com/pubs/HR/OPR/OPR_FAQ.jsp?null=57435&cds_mag_code=OPR&id=1528918801796&lsid=81641433221026832&vid=3&cds_page_id=57435&cds_to_id=faq – contacts1.
Of course, the queen of media utilizes social media accounts.
Sign up to receive the magazine through Facebook.
Tweet to customer service reps via Twitter.
Find out more about Hearst, the publisher of the Oprah Magazine through LinkedIn.
Check out what Oprah has to say on Google+.
Find out more about the Queen of Media from the Oprah Magazine YouTube Channel.
Get inspired by reading quotes from Oprah on Instagram.
Oprah's first issue of her magazine was published in April of 2000.


Stunning lot with abundant views - more than 180 degrees of long range views will surround your home in the Reynolds Mountain, an exclusive community of luxury custom homes. Watch the sunrise off your front porch and then enjoy watching the sunset as you relax on your deck where long range views seem to go on forever. The sloping lot is situated at the top of the mountain but offers both an easy drive up and a lot that allows for a gentle driveway to the first level and a walkout basement. Reynolds Mountain is located less than 10 minutes from the heart of vibrant downtown Asheville and minutes from the conveniences of Reynolds Village and North Asheville. For those seeking nearby recreation, enjoy the trails around Beaver Lake and the golf courses of The Country Club of Asheville just moments from home. CHECK OUT THE DRONE VIDEO ATTACHED TO THE LISTING! Home plans for this building site have been drafted and are available for your review.


the oceans of the world.
dominant features of the evolving earth.
elements. Some of the material is dissolved and carried to the sea in solution.
and 8 feet high. These dimensions represent a volume of 1,000 cubic feet.
throughout the sea have failed.
copper) than for the manganese.
same method used by the Chinese as early as 1000 b.c.
lies on the seafloor off the coast of San Diego and that economic recovery is quite feasible.


text:
Q: Function pageExist(); always returns false So I'm still improving my template engine, and now I'm at the part that's going to see if the requested page actually exists. Please take a look at the following function:
public function pageExist( $id )
{
    $query = $this->db->connection->prepare( 'SELECT id FROM ' . $this->functions->prefix( 'pages' ) . ' where id = ?' );
    $query->bind_param( 'i', $id );
    $query->execute();
    if ( $query->num_rows > 0 )
    {
        return true;
    }
        else
    {
        return false;
    }
    $query->close();
}

But the proplem is, it always returns false, so is there anything wrong with my prepared statement or anything?
I call a page with ID 1, I don't know if that has anything to do with it, but as it might help, I'll just state it.
Thanks.

A: There can never be a row with id of 0. Database tables must start at 1 if an integer. This will return false as no rows will be found.

A: Before accessing mysqli_stmt::$num_rows, you must call mysqli_stmt::store_result().  See mysqli_stmt::$num_rows on php.net
Excerpt:

Returns the number of rows in the result set. The use of mysqli_stmt_num_rows() depends on whether or not you used mysqli_stmt_store_result() to buffer the entire result set in the statement handle.
If you use mysqli_stmt_store_result(), mysqli_stmt_num_rows() may be called immediately.

Try this:
public function pageExist( $id )
{
    $query = $this->db->connection->prepare( 'SELECT id FROM ' . $this->functions->prefix( 'pages' ) . ' where id = ?' );
    $query->bind_param( 'i', $id );
    $query->execute();
    // Call store_result() before accessing num_rows.
    $query->store_result();
    if ( $query->num_rows > 0 )
    {
        return true;
    }
    else
    {
        return false;
    }
    $query->close();
}

redpajama_set_name: RedPajamaStackExchange


text:
Winthrop Realty Trust Closes Offering of $80.6 Million of Its 9.25% Series D Cumulative Redeemable Preferred Shares
BOSTON, March 23, 2012 (GLOBE NEWSWIRE) -- Winthrop Realty Trust (NYSE:FUR) ("Winthrop") today announced the closing of its previously announced underwritten public offering of 3,220,000 9.25% Series D Cumulative Redeemable Preferred Shares of Beneficial Interest (the 'Series D Preferred Shares")
Winthrop Realty Trust Announces Pricing of $70.1 Million of Its 9.25% Series D Cumulative Redeemable Preferred Shares of Beneficial Interest
BOSTON, March 20, 2012 (GLOBE NEWSWIRE) -- Winthrop Realty Trust (NYSE:FUR) ("Winthrop") today announced that it has sold in an underwritten public offering 2,800,000 shares of its 9.25% Series D Cumulative Redeemable Preferred Shares of Beneficial Interest at a price of $25.0385 per share
Winthrop Realty Trust Announces Offering of Its 9.25% Series D Cumulative Redeemable Preferred Shares of Beneficial Interest
BOSTON, March 19, 2012 (GLOBE NEWSWIRE) -- Winthrop Realty Trust (NYSE:FUR) ("Winthrop") today announced it has commenced an underwritten public offering of its shares of Series D Cumulative Redeemable Preferred Shares of Beneficial Interest. Barclays Capital Inc., Stifel, Nicolaus & Company,
~ FFO Per Share Increased Year Over Year 20.9% to $1.85 ~ ~ Declares First Quarter 2012 Cash Dividend ~ BOSTON, March 1, 2012 (GLOBE NEWSWIRE) -- Winthrop Realty Trust (NYSE:FUR), a leading real estate value investor, announced today financial and operating results for the fourth quarter and full
Mack-Cali and Winthrop Acquire Senior Mezzanine Position on Stamford Portfolio
Mack-Cali and Winthrop Acquire Senior Mezzanine Position on Stamford Portfolio Edison, New Jersey and Boston, Massachusetts-February 21, 2012-Mack-Cali Realty Corporation (NYSE: CLI), along with Winthrop Realty Trust (NYSE:FUR), today announced that they have formed a joint venture that acquired a
Winthrop Realty Trust Acquires $140.3 Million Mortgage Note at a Discount Through Its Joint Venture
Company's Joint Venture Purchases and Restructures Existing Debt on a Mixed Use Property in Chicago, Illinois
BOSTON, Jan. 23, 2012 (GLOBE NEWSWIRE) -- Winthrop Realty Trust ("Winthrop") (NYSE:FUR), a leading opportunistic real estate investor, announced that it will release its fourth quarter and year end 2011 results on the morning of Thursday, March 1, 2012 prior to the market open.
Winthrop Realty Trust Joint Venture Obtains $40 Million in Financing
BOSTON, Jan. 9, 2012 (GLOBE NEWSWIRE) -- Winthrop Realty Trust (NYSE:FUR) announced today that its joint venture, which holds the $117.9 million C note in a $798.0 million first mortgage encumbering a 4.5 million square foot, 31 property portfolio of office properties situated throughout southern
Winthrop Realty Trust Declares Dividend on Its 9.25% Series D Cumulative Redeemable Preferred Shares
BOSTON, Dec. 14, 2011 (GLOBE NEWSWIRE) -- Winthrop Realty Trust (NYSE:FUR) ("Winthrop") today announced that its Board of Trustees has declared a dividend for the fourth quarter of 2011 of $0.211979 per 9.25% Series D Cumulative Redeemable Preferred Share (the "Series D Shares") payable on December
Winthrop Realty Trust Closes Offering of 9.25% Series D Cumulative Redeemable Preferred Shares
BOSTON, Nov. 28, 2011 (GLOBE NEWSWIRE) -- Winthrop Realty Trust (NYSE:FUR) ("Winthrop") today announced the closing of its previously announced underwritten public offering of 1,600,000 9.25% Series D Cumulative Redeemable Preferred Shares of Beneficial Interest (the 'Series D Preferred Shares") at
Winthrop Realty Trust Announces Pricing of 1,600,000 of Its 9.25% Series D Cumulative Redeemable Preferred Shares of Beneficial Interest
BOSTON, Nov. 18, 2011 (GLOBE NEWSWIRE) -- Winthrop Realty Trust (NYSE:FUR) ("Winthrop") announced the pricing of an underwritten public offering of 1,600,000 of its 9.25% Series D Cumulative Redeemable Preferred Shares of beneficial interest at a price of $25.00 per share for total gross proceeds
Declared Fourth Quarter 2011 Dividend
Winthrop Realty Trust Settles Churchill Litigation
Enters Into New Lease With Westinghouse for Space at Churchill Property
BOSTON, Oct. 7, 2011 (GLOBE NEWSWIRE) -- Winthrop Realty Trust ("Winthrop") (NYSE:FUR), a leading opportunistic real estate investor, announced that it will release its third quarter 2011 results on the morning of Thursday, November 3, 2011 prior to the market open.
Winthrop Realty Increases Occupancy to 89% at Its Deer Valley Office and Medical Center Property
Sells Knoxville, Tennessee Property for $2.3 Million
Invested $70.7 Million in the Second Quarter ~ Declared Third Quarter 2011 Dividend
BOSTON, June 23, 2011 (GLOBE NEWSWIRE) -- Winthrop Realty Trust ("Winthrop") (NYSE:FUR), a leading opportunistic real estate investor, announced that it will release its second quarter 2011 results on the morning of Thursday, August 4, 2011 prior to the market open.
$112 Million Capital Deployed and Committed
Company Declares Second Quarter 2011 Cash Dividend

FFO Per Share Increased 19% to $0.44 compared to First Quarter 2010


All about Insider Tales: The Secret of Casanova. Download the trial version for free or purchase a key to unlock the game!
Stroll through the gothic alleyways of Prague, listen to music on the streets of Paris and enjoy the elegant architecture of Venice as you retrace the footsteps of history's greatest lover and uncover the secrets his family buried with him.
i am looking for some help. i am enjoying the game, but i am stuck. she is looking for a key to unlock the bird cage to get the rest of the clippers. i keep hitting the hint buttom and where it shows the hint and some where in that area is the key, but i can not find. can somebody give a clue to where it is?
I have the same problem. I am stuck and cannot find the key.
Insider Tales - The Secret of Casanova This is a nice relaxing un-timed love story adventure game. This game is: Addictive, Good Replay, Original, Involved, Good Value "This was a nice un-timed relaxed Love Story, which took place in Italy. There is one element missing for Casanova's Life, and the gamer must help the characters figure what is missing. There are a series of puzzles, mini-games, riddles, locate objects missing from lists, matching two scenes, and various other brain-teasing activities. You must be a logical thinking person to solve this mystery adventurous story. This game would be recommended for adults, only. Some of the puzzles involve difficult mathematics, and some of the skills necessary to advance through all the levels would probably be too intense for a child to understand. There is NO violence in it, and there is nice soothing music...so, a child probably could play it, but it is more made for an adult player in mind. Also, it is encouraged to lighten your computer monitor's graphics, as it is difficult to locate some of the items in the dark, if the graphics aren't set just correctly; just offering some advice, if you know how to change settings around. Hope this review helps. If it does help you then, please rate this review as helpful. Thanks, and hope you enjoy this game as much as I did. It is also a great replay game."
this game is so cool.try it everyone.


text:
Connor Sephton
Korea's crypto market is among the strongest — and the strangest — in the world
Between strict capital controls and regulations, Korea's cryptocurrency industry is so closed off that Bitcoin commands a steep premium and DeFi is in its infancy.
On a day in which Bitcoin crashed briefly to $30,000 in a rampant bear market, the leading cryptocurrency never got anywhere close to that on Korean exchanges. The so-called "kimchi premium" saw to that, keeping the price of Bitcoin as much as $5,000 above its level on leading U.S. exchanges.
The major reason for this kimchi premium is that Korea's exchanges are fairly isolated by a combination of the country's strict capital control laws preventing funds from leaving the country, and the tax code and anti-money laundering (AML) regulations that make it difficult for foreigners to use Korean exchanges — even giants like Bithumb and Upbit — without local Korean bank accounts.
Nor is that premium the only part of South Korea's crypto industry that sets it apart from the rest of the world. Among other things, the market's isolation combined with the extraordinary stability of the Korean won has kept stablecoin usage low and the embrace of decentralized finance, or DeFi, well behind that of the rest of the world.
Korea's Bitcoin boom
Despite this isolation, Korea's embrace of Bitcoin in particular and cryptocurrency in general is very strong. In April, more than five million unique cryptocurrency users — about 10% of the country's population — reportedly bought or sold digital assets at least once since the beginning of 2021.
On May 19, the day the kimchi premium hit $5,000, just one Korean exchange, Upbit, had a 24-hour transaction volume of more than $31.5 billion, according to CoinMarketCap. Add in the rest of the country's "big four" cryptocurrency exchanges, Bithumb, Korbit and Coinone, and it was $38.1 billion — substantially more than has been traded recently on the leading Korean stock exchange KRX.
One interesting aspect of Korea's cryptocurrency craze is how broadly it is spread across age groups. One February survey showed that almost half of the users of leading Korean exchanges Bithumb and Upbit were in their 40s or 50s — many of them mothers. That said, a broader survey of Korean crypto exchange apps in March showed that young people dominate the ranks of new Korean crypto users, with those in their 20s and 30s accounting for nearly two-thirds of the new monthly app users in the first three months of the year. However, they are investing small amounts, often less than $100.
All that's clearly having an impact. Bithumb Korea recently announced that its Q1 2021 net profit was up 876% compared with the previous year.
Government roadblocks
At the same time, the Korean government and regulators are far from being fans of cryptocurrency. In February, Bank of Korea Governor Lee Joo-yeol told a National Assembly committee hearing that "a crypto asset is an asset that has no intrinsic value." He added that "it is difficult to understand why the price of Bitcoin is so high."
Korea's crypto regulations also make it difficult for foreign competitors. In December 2020, the world's biggest exchange, Binance, shuttered its Binance Korea operation less than a year after it launched, thanks in large part to a law that banned exchanges operating in the country from sharing order books — meaning Binance Korea could no longer lean on Binance's liquidity.
That law came into effect in March 2021, the same month that another leading cryptocurrency exchange — OKEx — announced it was shuttering its Korean operations due to the new AML regulations. It has also been suggested that these rules will make it difficult for smaller Korean exchanges to compete with the big four.
Not a fan of stablecoins?
Despite this booming crypto market, Korea is far behind the rest of the world in adoption of stablecoins, in no small part because the Korean won is stable enough that there isn't as strong a need for stablecoins in the largely walled-off crypto market.
Beyond that, the Korean government frowns on stablecoins, according to Oleg Smagin, head of global marketing at Delio, a leading Korean crypto lending and staking firm. That makes exchanges leery of them, he adds.
In addition, exchange fees are low — largely in the 0.15% to 0.25% range at the big four. While the fees for withdrawals in won are flat and very low — about $1 — the fee for moving cryptocurrencies directly off can be steep. The big four's withdrawal fees range from 0.0005 to 0.0015 BTC to withdraw Bitcoins directly — $20 to $60 for one BTC at $40,000.
Which could help explain why the Korean won is the fourth-most traded national currency for Bitcoin, behind only the Japan yen, the euro, and the dominant U.S. dollar.
The CeFi-DeFi hybrid
One victim of Korea's closed-off crypto market and unfamiliarity with stablecoins is that the booming DeFi industry hasn't had a chance to take hold there, Smagin says.
"2019 became a tipping point for the wide adoption of DeFi globally, but in Korea it was barely recognized, mostly because most of the local retail investors lacked experience using overseas crypto services and the adoption of stablecoins was low," he says.
Delio's solution is a hybrid centralized-decentralized finance model that uses CeFi as a way to build the initial crypto lending ecosystem that will become more and more decentralized over time. In the meantime, the firm realized there is an "enormous niche for a CeFi crypto-to-crypto lending service that can serve the needs of the local traders," Smagin says.
The firm currently has four CeFi lending offerings, as well as a new payment service that lets Delio wallet holders pay with Bitcoin at a network of more than 70 retail firms services by payment app Money Tree. In addition, it's Delio Liquidity arm provides institutional clients with digital asset loans of between $800,000 and $45 million.
Delio offers Bitcoin and Ethereum loans of up to 90% of the borrower's BTC or ETH collateral, and also provides lending services to Bithumb customers, who can use either BTC or ETH, or Korean won, as collateral. Staking and yield farming are also available. Delio recently passed $2 billion in total value utilized.
Delio's DeFi hybrid plans are centered around Ducato, a won-based stablecoin project scheduled to launch in the third quarter of 2021. The KRWD stablecoin — fixed at one won — will be generated by collateralizing cryptocurrency. Ducato is a DeFi protocol with its own token, DUCATO, which is used to pay fees and for governance. But the CeFi Delio platform provides the stablecoin with a user-friendly interface.
Learn more about Delio
Disclaimer. Cointelegraph does not endorse any content or product on this page. While we aim at providing you all important information that we could obtain, readers should do their own research before taking any actions related to the company and carry full responsibility for their decisions, nor this article can be considered as an investment advice.
#Bitcoin Regulation
#AML
#Kimchi Premium
The biggest crypto heists of all time
14 years since the Bitcoin white paper: Why it matters
Korean crypto exchanges could soon face fines for gaps in due diligence measures
South Korea's crypto regulation is now expanding to foreign businesses
Bybit crypto exchange suspends services in South Korea


It is well established that fighting cancer is an overwhelmed mission. Not only for the disease itself but also for all the consequences from the treatments.
During his battle with throat cancer, James underwent radiotherapy. To attend the treatments, James used to take the London Underground, and found it really difficult to find a seat as he was not visibly unwell and could not speak because of his treatment.
Inspired by the Transport for London (TFL)'s Baby On Board badges, James created the Cancer on Board badge to encourage people to make room on public transport for those undergoing treatment. The aim is to help cancer patients' journeys to and from treatment a little more bearable.
James McNaught, from London, UK, was diagnosed with throat cancer in 2014. James had to use the London Underground to get to University College Hospital for the treatments. As he was not visibly unwell and could not speak because of his treatment, James struggled to find a seat. So, he came up with the idea of wearing "Cancer on board" badges when riding the network.


text:
Gabriela Matuszek-Stec (* 31. Dezember 1953 in Jaworzno) ist eine polnische Literaturhistorikerin, Essayistin, Kritikerin und Übersetzerin deutscher Literatur.

Leben
Gabriela Matuszek-Stec ist Professorin für Polonistik an der Jagiellonen-Universität in Krakau und befasst sich mit der Literatur des 19. und 20. Jahrhunderts – vornehmlich mit Stanisław Przybyszewski, dem naturalistischen Drama und moderner Prosa, deutsch-polnischen Literaturverbänden und der literarischen Übersetzung. Von 1983 bis 1987 hielt sie Vorlesungen über polnische Literatur an der Humboldt-Universität Berlin, war dort Gastprofessorin (2004 und 2006), ebenso in Jena, Köln, Leipzig, Wien, Grenoble und Prag.

Sie war Stipendiatin verschiedener wissenschaftlicher und literarischer Stiftungen, u. a. der Deutschen Schillergesellschaft in Marbach am Neckar (1995, 1996), der Literaturakademie in Ranis (2002), des International Writers and Translators Center of Rhodes (2002), des Baltic Centre for Writers and Translators, Gotland (2003). Seit 1992 ist sie Mitglied der Societas Jablonoviana zu Leipzig.

Sie ist Gründerin und Direktorin der ersten "polnischen Literaturinstitutes" (des Studium Literacko-Artystyczne an der Jagiellonen-Universität in Krakau). Von 2005 bis 2008 war sie Vizepräsidentin, danach bis 2014 Präsidentin des Krakauer Niederlassung des Polnischen Schriftstellerverbandes, seit 2014 Mitglied des Verwaltungsrates. Seit 2007 ist Gabriela Matuszek-Stec Redakteurin der Seria Studium Literacko-Artystycznego UJ sowie der Krakauer Bibliothek des Polnischen Schriftstellerverbandes (seit 2009). Gabriela Matuszek war Teilnehmerin des deutsch-polnischen Lyrikfestivals wortlust in Lublin.

Auszeichnungen
 Medaille der Nationalen Wissenschaftskommission (Medal Komisji Edukacji Narodowej), 2002
 Preis des polnischen Wissenschaftsministeriums für ihr Buch Stanisław Przybyszewski – ein moderner Schriftsteller. Essays und Prosa – Versuch einer Monographie, 2009
 Gloria-Artis-Medaille für kulturelle Verdienste, 2015

Schaffen

Bücher
 "Der geniale Pole"? Niemcy o Stanisławie Przybyszewskim (1892–1992). Universitas, Kraków 1993, ISBN 83-7052-114-2; wyd. II rozszerzone, Kraków 1996, ISBN 83-7052-317-X.
 dt. Übersetzung von Dietrich Scholze: "Der geniale Pole"? Stanisław Przybyszewski in Deutschland. Igel Verlag, Paderborn 1996, ISBN 3-89621-014-9.
 Naturalistyczne dramaty/Naturalistische Dramen. Universitas, Kraków 2001 (ISBN 83-7052-640-3), II wyd. Kraków 2008, ISBN 97883-242-0859-3.
 Stanisław Przybyszewski – pisarz nowoczesny. Eseje i proza – próba monografii. Universitas, Kraków 2008, ISBN 978-83-242-0930-9.
 dt. Übersetzung von Dietmar Gass: Krisen und Neurosen – Das Werk Stanisław Przybyszewskis in der literarischen Moderne. Igel Verlag, Hamburg 2013, ISBN 978-3-86815-567-9.
 Maski i demony wczesnego modernizmu, Wydawnictwo Uniwersytetu Jagiellońskiego, Kraków 2014, ISBN 978-83-233-3769-0.

Redaktionelle Arbeiten – eine Auswahl
 Stanisław Przybyszewski: Dzieci szatana, Oficyna Literacka, Kraków 1993 (oprac.), ISBN 83-85158-79-0.
 Über Stanisław Przybyszewski. Rezensionen – Erinnerungen – Porträts – Studien. Rezeptionsdokumente aus 100 Jahren, Igel Verlag, Paderborn 1995 ISBN 3-89621-013-0.
 mit German Ritz: Recepcja literacka i proces literacki. Literarische Rezeption und literarischer Prozess. (O polsko-niemieckich związkach literackich w okresie modernizmu i dwudziestolecia międzywojennego), Kraków 1999, ISBN 83-7052-846-5.
 Lektury polonistyczne. Od realizmu do preekspresjonizmu, Universitas, Kraków 2001, ISBN 83-7052-606-3.
 Stanisław Przybyszewski: Poematy prozą, Wydawnictwo Literackie, Kraków 2003, ISBN 83-08-03548-5.
 Literatura wobec nowej rzeczywistości, Księgarnia Akademicka, Kraków 2005, ISBN 83-7188-815-5.
 Po(st)mosty. Polacy i Niemcy w nowej Europie. Tom ofiarowany pamięci Henryka Bereski, Księgarnia Akademicka, Kraków 2006, ISBN 83-7188-915-1.
 Krynickie Jesienie Literackie. Poezje, eseje, głosy, Kraków 2007, ISBN 978-83-918287-4-8.
 mit Brigitta Helbig-Mischewski (Hrsg.): Fährmann grenzenlos. Deutsche und Polen im heutigen Europa. Zu Gedenken an Henryk Bereska. Georg Olms Verlag,  Zürich, New York 2008, ISBN 978-3-487-13639-4.
 Przybyszewski. Rewizje i filiacje, Księgarnia Akademicka, Kraków 2015, ISBN 978-83-7638-508-2.
 mit Hanna Sieja-Skrzypulec: Twórcze pisanie w teorii i praktyce, Księgarnia Akademicka, Kraków 2015, ISBN 978-83-7638-590-7.

Übersetzungen deutscher Literatur – Auswahl
 Stanisław Przybyszewski: "Synagoga szatana" i inne eseje, Kraków 1995, ISBN 83-7124-070-8.
 mit Marek Śnieciński: Dieter Kalka:, Wszystko to tylko teatr i inne opowiadania, Poznań 1999, ISBN 83-87235-26-1.
 Felix Mitterer: Dzika kobieta. In: Felix Mitterer: Teatr zaangażowany. Antologia współczesnej dramaturgii austriackiej, t. 3, Warszawa 2002, ISBN 83-7188-815-5.

Einzelnachweise

Weblinks
 http://www.sla.polonistyka.uj.edu.pl/gabriela-matuszek
 http://www.pmp.polonistyka.uj.edu.pl/pracownicy/prof.-dr-hab.-gabriela-matuszek
 http://www.sppkrakow.pl/czlonkowie/gabriela-matuszek/
 http://www.krakow.pl/kultura/79521,artykul,gabriela_matuszek.html
 Gabinet Książki i Prasy Polskiej w Niemczech
 http://www.instytutksiazki.pl/zapowiedzi-i-nowosci-wydawnicze,aktualnosci,22687,stanislaw-przybyszewski---pisarz-nowoczesny.html
 nauka-polska.pl

Literaturhistoriker
Träger der Gloria-Artis-Medaille für kulturelle Verdienste
Essay
Übersetzer aus dem Deutschen
Übersetzer ins Polnische
Autor
Pole
Geboren 1953
Frau

redpajama_set_name: RedPajamaWikipedia


Today's Tarot is the Eight of Swords (Jupiter in Gemini). In a classic case of missing the point, this woman remains trapped despite the fact she could easily free herself. Her home/dixiblog/domains/afoolsjourney.com/public_html castle isn't even a long walk away! But she doesn't, for fear of being cut in the process. She doesn't even want to look, because the entire situation depresses her.
Consider her arrival a prod to evaluate areas you feel trapped, restrained and stuck. Question your assumptions. Specifically, whatever has seemed impossible, too painful, too difficult, unlikely to succeed? Yeah, that. Because your assumptions about the escape are a lot darker than the actual escape route. That water in the background hints it's an emotional experience, but this woman is not drowning. She's on solid ground and can walk away with a minimum of struggle. She just has to figure that out. Enter Tarot, to point the way.
The thing I love about this card is the confirmation that the future is in YOUR OWN hands. Her cage only works because she complies with her captors—and where are they now, by the way? The facts (Tarot Swords) may be cold and hard, but they are not sufficient to cage her. That requires complicity. So if you want hope, there you go.
This is a card of power waiting to be reclaimed. If it helps, I can promise you that it's a lot easier to get it than you've been imagining. So why not give it a go?
Can you relate to the Eight of Swords?
Today's Tarot is the perfectly dressed Five of Swords (Venus in Aquarius). You've been battling to get this dress put together, and it hasn't always been smooth sailing. But it's come together and the remaining loose threads are being snipped.
And you know what? It's beautiful. Just exactly as it should be.
Don't kick yourself, for how long it's taken or how hard you had to fight in order to SEE, to get where you are now. It doesn't matter if it took 10 seconds or 10 days or 10 decades. Don't you see? That doesn't mean you've failed anything. The only way to fail is to give up. But you're still here.
You are in the perfect place at the perfect time, doing the perfect thing for the whatever ways you need to learn and grow. Otherwise, you wouldn't be here. Keep snipping threads where you see them, but in the meantime, be grateful you're finding them to snip.
It may have been a lot of work. But the work shows. The more joy you take in it, the more it's turned up. How cool is that?!
Where do you see the Five of Swords?
Whenever I see the nine of swords, I think of those times in my life I've had secrets…things I didn't talk to parents or friends or husbands about. Heaviness I carried around in my chest; the kind that comes to visit when you lie quiet and still and there's no other noise to fill your mind.
Today's Tarot is the reversed Nine of Swords, associated with Mars in Gemini. Think war (Mars) in your head (Gemini)! I often see this card when someone is having trouble sleeping, especially nightmares, or is dealing with guilt and secret burdens. It's a very lonely and sometimes dark place. Think Sword of Damocles. There's a sense of isolation, often seasoned with some shame or fear.
This is, indeed, one of those cards I prefer reversed, since I'd rather see this energy not expressed full force. It's ouchy. Today, I'm seeing it as letting go of the old worries, fears, and more than anything, the sense of being alone!
You CAN share. You can unburden (and allow others the same gift). It is a risk, I know. But if you afford others the respect of granting them the right to feel however they do, knowing you only own yours and being okay with that, you can afford the risk. You may be surprised to find compassion where you thought you'd find condemnation.
Do you see yourself in the reversed nine of Swords?
Dig the Everyday Tarot? Get a Consultation with Dixie.
Today's Tarot is the Page of Swords or Princess of the Rushing Winds, associated with Earth in Air. I sometimes see this young man heralding formal agreements, new ideas, or advising to apply reason to the task at hand. But we've been talking about taking care of ourselves. Representing Earth, the page is concerned with practical details of our daily lives. In Air, we want to use the sword of reason to detach from concerns that don't belong to us. Cut out what doesn't contribute to the bottom line.
In some ways, that IS psychic self-defense. But it's also managing resources. You want to be clear on your mission. Then, you can use that clarity as a Litmus test to help making decisions. He's giving us permission to choose for ourselves what we want, and the tools for living in accordance with that choice.
This isn't about selfishness. Some goals may be about supporting others. But knowing your aims, you can choose only to do those things that actually DO help, not acting unconsciously and possibly contribute to dysfunction.
Does a decision support your core values? Good expenditure of your energy. Otherwise? Not such a good investment. We've only got so much time, energy…life, to spend creating here. There are only so many lives we'll be touching, so many days we'll be getting up to greet the sun, you know? Make the most of what you've got. Anything less is a waste.
The Page of Swords doesn't tote old baggage. He doesn't repeat old news, or care about how things used to be. He's clear on what he wants, and thinks carefully on how best to achieve his aims. It's not that he doesn't support others. He's just discriminating, because he wants to make the most impact through his decisions. Put your energy behind what you can support, what reflects your core values and convictions, and let go (with good intent) what does not fit. Your load will be lighter and you'll create a lot more without the drag.
Do you have clear mission(s)?
Follow Dixie and the Everyday Tarot on Twitter, Facebook, or Google +. Or just schedule a Tarot consultation.
I've always found emotional energy builds up in physical space. The more emotional torque, the denser and more lingering the after-cloud. Fights, sadness, joy, fear, laughter—it all sticks like a scent that gets into the carpet and drapes. The smell remains remains until it's either dissipated or absorbed by people passing through it.
Today's Tarot forecast is the inverted Two of Swords, or Lord of Peace Restored, associated with the Moon in Libra. There is always a certain stability around this card, if tension. The polarity of the Tarot twos have a built-in sense of balance—the conflicting forces serve to stabilize one another.
The Moon in Libra would like feelings (Moon) to be pretty (Libra), but is practical enough to know that's not always the case. Animal nature is part of who we are; the emotional voice hits a full spectrum of pitches.
The reversed Two of Swords suggest we stop stressing about each individual choice point, afraid we won't measure up. Accept the contradicting pulls as part of the human experience. Shift the freed up energy to taking action that you can feel good about—always looking for whatever light you can contribute to the circumstance.
A more Zen approach lessens the burden and lifts your vibration at the same time. It puts you back in the flow, able to receive guidance and inspiration again. And it leaves you feeling a whole lot happier! Don't worry about being perfect or making a mistake. We do the best we can at the time, and look to grow in the process. Just commit to being the happiest, best person you know how to be. Because that's a good place to live.
How do you do with unresolved decisions?
There's the minute, when you really "get" it. A new idea has found it's way into your sphere of awareness, and all of a sudden, everything shifts. Snap, click, bam! It takes a bit for your eyes to adjust to the light that's been flicked on.
Today's Tarot forecast is the Ace of Sword, or Root of the Powers of Air. It's the essence of the Air Element—thought, reason, and logic. The Ace of Swords makes things conscious. Maybe it's a new perspective, a new idea, or a new possibility you haven't been aware of before. This thought form is young, though, and will require energy to grow.
Swords like unadorned directness, so let's oblige.
Look at that fresh inspiration—the one that just hit you? It is every bit as valuable as it seems. Run with it! You can take off, if you follow through.
Have any fresh ideas lately?


text:
Eagles Rookie Cornerback Rasul Douglas Searching for Consistency
By Dave Zangaro | CSNPhilly.com	• Published August 7, 2017 • Updated on August 7, 2017 at 5:46 pm
When asked about rookie third-round cornerback Rasul Douglas on Sunday, the first word defensive coordinator Jim Schwartz thought of won't instill much confidence.
"Inconsistent," Schwartz said.
That's not to say Douglas hasn't had good moments. He has.
But for every good moment, it seems like there's been a bad one. For every time he nails his technique, it slips somewhere else. Every time he looks like he might be a viable option to play a lot this season, he starts to look like a rookie again.
"I'm sure he would tell you the same way," Schwartz said. "He's not only trying to learn all the nuances of the scheme, he's trying to be consistent with technique. Sometimes I think it feels like every time he gets like a finger in the dyke, so to speak, another leak pops somewhere else, and that's what happens with rookies. I think somewhere along the line for Rasul, the game will slow down a little bit."
The game hasn't slowed down for Douglas yet. Schwartz remembered how confident and competitive the West Virginia product was at rookie camp in the spring. The problems came when the defense started getting more complex and the competition became more intense.
Schwartz made sure to point out that Douglas' struggles are not his alone. He said just about every rookie goes through the same thing.
"It's that rookie part about it," second-year cornerback Jalen Mills said. "It's those growing pains. Me just being in his position last year, I remember each and every day I would feel like I made a great play and then the next play I would mess up on something and Coach Schwartz and Coach Corey (Undlin), they were chewing me out. You want to play up to that high level, those high expectations that Coach (Doug) Pederson and the defensive coordinator and your DB coach have."
Mills agreed that even though rookies know every other rookie goes through something similar, it doesn't offer any solace when you're the one going through it. It's tough.
For Douglas, that's just his reality right now. Things aren't coming easily. Schwartz said Douglas "is not there yet."
"I feel like once you get over that hump, it's smooth sailing and it's just football and having fun," Mills said. "But you have to get over the hump."
There are plenty of reasons to think Douglas will eventually find his way. After all, he was a third-round pick for a reason. He did lead the nation last season with eight interceptions. And it's not like he's been a disaster at training camp. He's learned his playbook and he's made some plays.
Now, it's all about making them consistently.
"I just have to be the same player every day," Douglas said. "Just keep working."
Copyright CSNPhily


text:
iReach Archive
Zonar Welcomes Gareth Wade as New Chief Revenue Officer
Global Business Leader to Direct Expanded Growth and Oversee Successful Sales Operations
Gareth's expertise in working with customers as they adopt new technologies as well as his ability to motivate and energize teams makes him the perfect addition to the Zonar family
SEATTLE (PRWEB) January 30, 2019
Zonar, the leader in smart fleet management technology, has enhanced the senior executive team with the addition of Gareth Wade as the new Chief Revenue Officer. Wade is an award-winning business and sales leader with more than 20 years of diverse global experience helping organizations increase revenue and build successful teams and programs. Wade is joining Zonar with a focus on revenue growth through direct sales, channel and reseller programs.
"This is an important time in our industry as both fleets and commercial vehicle OEMs are working to embrace and accelerate the digitization of their vehicles and businesses," said Ian McKerlich, President and CEO at Zonar. "Gareth's expertise in working with customers as they adopt new technologies as well as his ability to motivate and energize teams makes him the perfect addition to the Zonar family."
Wade joins Zonar as a seasoned leader of technology companies and sales teams in the UK, across Europe and North America. Most recently he served as US Director of Business Development & Strategic Alliances for GCI Communication Corp. Previously he was Chief Sales Officer at content26, Director of Channels Sales at Polycom, Inc. and Principal Revenue Growth Consultant at OneAccord Partners.
Before re-locating to the US from Edinburgh in the United Kingdom, Wade served as the founding Sales & Marketing Director of Viju, (formerly CityIS) in the UK and across Europe. Wade moved to Seattle in 2004 and as President and CEO of CityIS, Inc. he established a new subsidiary business. Wade has won many sales recognition awards, including being ranked in the top 25 Deloitte & Touche "Fastest Growing UK Companies" four years consecutively and "Best Director" in national awards sponsored by Scottish Enterprise. Wade serves as volunteer Chairman for British American Business Connections, Pacific Northwest and is a Vice President of the Seattle Saracens Rugby Club.
At Zonar, Wade will be focused on increasing revenue through designing and executing tailored sales and channel solutions, building high-performance teams, forging strategic partner ecosystems and providing executive leadership.
For more information on Zonar, please visit: http://www.zonarsystems.com
Ben Hohmann
@zonarsystems


Airbnb was founded in 2008 in San Francisco with a mission to give people a sense of belonging. Since then, the website and app have taken off and have become a trusted community marketplace for people to list, discover, and book unique accommodations around the world. As the name states, it's a website that allows anyone to become a host to their own B & B, or bed and breakfast. It has become especially popular for college students and young adults due to its low prices and local venues. Hosts and guests alike have fallen in love with Airbnb, giving other travel sites such as Expedia or HostelWorld a run for their money.
Airbnb.com is more than just a reservation site.
When you go to airbnb.com, you are instantly welcomed with a slideshow of warm videos and the phrase "Belong Anywhere." The search bar for a destination keeps a low profile, allowing you to immerse yourself into what airbnb has to offer. You have easy access to videos of hosts, company culture, and featured locations, allowing you to get to know what this company is about and who is representing it.
When you are done checking out their owned content, you can go to your own personal profile and see where you have stayed, where you're going, and where you wish to go in the future. They do a really great job of integrating your information with what the site has to offer, instead of keeping a very dry profile page.
Side note: They even have a video dedicated to intern life at airbnb. I guarantee Expedia does NOT have that.
Airbnb's brand represents more than just a company's trademark.
Although the video above does an incredible job of explaining airbnb's symbol, I will quickly recap. The bélo represents a pinpoint on a map, the letter 'A' for airbnb, a traveler, and a heart. Those four things together, in airbnb's mind, is all you need to travel, and they're right. Airbnb goes a step further to establish their brand with their consumers by asking travelers to create their own symbol at Create Airbnb and take it with them on trips, or if they're hosts, have it in their windows. It's good when a consumer an identify a brand or simple, but it's even better when they can relate to it, and that's nearly impossible to do.
Airbnb's app is almost too user-friendly.
I first discovered airbnb through the app. I got an email from a friend that had used it before and told me to check it out. I did, and instantly fell in love. I spent hours going through cities I want to go to and cities I've already been to. I'm a travel fiend, so stumbling upon this was a gold mine in my eyes. In my opinion, the app is even more user-friendly than the website. It is crisp, clean, and so easy to maneuver.
You can't access the awesome airbnb.com videos, but the reservation process is entirely accessible through your mobile device. Other hotel sites have apps, but nothing this in-depth. Having an app that is so accessible is key to seasoned travelers. If you're a backpacker, you can book the room the day you arrive in the city without having to get access to WiFi or a place with computers. A working app is the key to a working booking site.
People say that owning a Jeep or being a vegetarian is a lifestyle. I would have to say that airbnb is a lifestyle, as well. Airbnb may not be for everyone, but it is for people who take traveling seriously. People who aren't afraid to stay at a stranger's house, people who take chances, people who take the chance to belong anywhere, fulfilling what the company promises will happen when you book through airbnb. Whether you're a host, a guest, a web engineer, or an executive at airbnb, you feel like you're apart of a community. That is why I love Airbnb, and I don't think people say that about other booking companies.
Give Airbnb a try and let me know what you think of it!