%
% 03-modely-konkurentnych-systemov.tex
%
% Developed by Ondrej Jombik <nepto@platon.sk>
% Copyright (c) 2006 Platon Group, http://platon.sk/
% Licensed under terms of GNU General Public License.
% All rights reserved.
%
% Changelog:
% 2006-08-17 - created
%

% $Platon: doc/statnica-teoria-prog/03-modely-konkurentnych-systemov.tex,v 1.3 2006-08-18 10:25:42 nepto Exp $

\chapter{Modely konkurentných systémov}

\section{Silná bisimulácia} % /*

\begin{defn}
	Množina akcií $Act = A \cup \overline{A} \cup \{\tau\}$, kde:
	\begin{enumerate}
		\item $A$ sú vstupné akcie
		\item $\overline{A}$ sú výstupné akcie
		\item $\tau$ je vnútorná akcia
	\end{enumerate}
\end{defn}

\begin{defn}[Silná bisimulácia]
	Binárna relácia $S \subseteq \mathcal{P}\times\mathcal{P}$ je {\it silná bisimulácia}, ak $(P,Q)
	\in S$ implikuje, že pre $\forall x \in Act$ platí:
	\begin{enumerate}
		\item Ak $P\stackrel{x}{\to}P'$ potom $\exists Q': Q\stackrel{x}{\to}Q'$ a $(P',Q') \in S$
		\item Ak $Q\stackrel{x}{\to}Q'$ potom $\exists P': P\stackrel{x}{\to}P'$ a $(P',Q') \in S$
	\end{enumerate}
\end{defn}

\begin{veta}
	Ak $S_1, S_2$ sú silné bisimulácie, tak potom aj:
	\begin{enumerate}
		\item $I$, tj. $(P,P) \in S$
		\item $S^{-1}_i$, teda $(x,y) \in S' \iff (y,x) \in S$
		\item $S_1 \circ S_2$
		\item $S_1 \cup S_2$
	\end{enumerate}
	sú silné bisimulácie.
\end{veta}

\begin{defn}
	Procesy $P$ a $Q$ sú silne bisimulárne, ak existuje taká silná bisimulácia $S$, že $(P,Q) \in
	S$.
\end{defn}

\begin{defn}
	$\sim = \cup\{S ~|~ S$ je silná bisimulácia$\}$
\end{defn}

\begin{veta} ~
	\begin{enumerate}
		\item $\sim$ je ekvivalencia
		\item $\sim$ je najväčšia silná bisimulácia
	\end{enumerate}
\end{veta}

\begin{veta}
	$P \sim Q \iff \forall x \in Act:$
	\begin{enumerate}
		\item Ak $P\stackrel{x}{\to}P'$ potom $\exists Q': Q\stackrel{x}{\to}Q'$ a $P' \sim Q'$
		\item Ak $Q\stackrel{x}{\to}Q'$ potom $\exists P': P\stackrel{x}{\to}P'$ a $P' \sim Q'$
	\end{enumerate}
\end{veta}

% */

\section{Silná bisimulácia až na $\sim$} % /*

\begin{defn}
	$S$ je {\it silná bisimulácia až na $\sim$}, ak $PSQ$ implikuje $\forall x \in Act$
	\begin{enumerate}
		\item Ak $P\stackrel{x}{\to}P'$ potom $\exists Q': Q\stackrel{x}{\to}Q'$ a $P' \sim S \sim Q'$
		\item Ak $Q\stackrel{x}{\to}Q'$ potom $\exists P': P\stackrel{x}{\to}P'$ a $P' \sim S \sim Q'$
	\end{enumerate}
\end{defn}

\begin{veta}
	Ak $S$ je silná bisimulácia až na $\sim$, tak $\sim S \sim$ je silná bisimulácia.
\end{veta}

\begin{veta}
	Ak $S$ je silná bisimulácia až na $\sim$, tak $S \subseteq \sim$.
\end{veta}

\begin{veta} ~
	\begin{enumerate}
		\item $P+Q \sim Q+P$
		\item $P+(Q+R) \sim (P+Q)+R$
		\item $P+P \sim P$
		\item $P+Nil \sim P$
	\end{enumerate}
\end{veta}

\begin{veta} ~
	\begin{enumerate}
		\item $P|Q \sim Q|P$
		\item $P|(Q|R) \sim (P|Q)|R$
		\item $P|Nil \sim P$
		\item $(P\setminus K)\setminus L \sim P \setminus K \cup L$
		\item $P[f]\setminus L \sim P \setminus f^{-1}(L)[f]$
		\item $P[id] \sim P$
		\item $P[f][f'] \sim P[f\circ f']$
	\end{enumerate}
\end{veta}

\begin{veta}[Expanzný zákon]
	$P \equiv P_1 | P_2 | ... | P_n$

	$$
	P \sim (\sum_{P_i\stackrel{x}{\to} P'_i} x (P_1 | \dots | P'_i | \dots | P_n)) +
	...
	+ (\sum_{P_i\stackrel{a}{\to} P'_i, P_j\stackrel{\overline{a}}{\to}P'_j} \tau (P_1 | \dots | P'_i |
	... | P'_j | \dots | P_n))
	$$
\end{veta}

% */

\section{Rôzne} % /*

\begin{defn}
	Nech $E$ a $F$ sú CCS termy s voľnou premennou $X$. Potom platí:
	$$
	E \sim F \iff \forall P \in \mathcal{P}: E[P/x] \sim F[P/x]
	$$
\end{defn}

\begin{veta}
	Nech $E \sim F$, potom $\mu XE \sim \mu XF$
\end{veta}

\begin{defn}
	Premenná $X$ je slabo strážená v $E$, ak každý výskyt $X$ je vnútri výrazu $y.F$.
\end{defn}

\begin{veta}
	Ak $X$ je slabo strážená v $E$ a $E[P/X] \stackrel{y}{\to} P'$. Potom $P' \equiv E'[P/X]$ a
	zároveň $E[Q/X] \stackrel{y}{\to} E'[Q/X]$.
\end{veta}

\begin{veta}
	$\mu XE \sim E[\mu XE/X]$
\end{veta}

\begin{veta}
	Nech $X$ je slabostrážená v $E$ a $F \sim E[F/X]$. Potom $F \sim \mu XE$.
\end{veta}

\begin{defn}
	Nech $f: P(\mathcal{P}\times\mathcal{P})\to \mathcal{P}\times\mathcal{P}$. Ak $R \subseteq
	P(\mathcal{P}\times\mathcal{P})$ kde $(P,Q) \in f(R) \iff \forall x \in Act$:
	\begin{enumerate}
		\item Ak $P\stackrel{x}{\to}P'$ potom $\exists Q': Q\stackrel{x}{\to}Q'$ a $P'RQ'$
		\item Ak $Q\stackrel{x}{\to}Q'$ potom $\exists P': P\stackrel{x}{\to}P'$ a $P'RQ'$
	\end{enumerate}
\end{defn}

\begin{veta} ~
	\begin{enumerate}
		\item $f$ je monotónna
		\item $S$ je silná bisimulácia $\iff S \subseteq f(S)$
	\end{enumerate}
\end{veta}

\begin{defn}
	$\mathcal{R}$ je pevný bod ak $\mathcal{R} = f(\mathcal{R})$ a pre pevný bod $\mathcal{R} \subseteq
	f(\mathcal{R})$.
\end{defn}

\begin{veta}
	$\sim = f(\sim)$
\end{veta}

% */

\section{Simulácia} % /*

\begin{defn}
	Relácia $R$ je simulácia ak $PRQ$ implikuje
	$$
	P\stackrel{x}{\to}P': \exists Q': Q\stackrel{x}{\to}Q' \land P'RQ'
	$$
\end{defn}

\begin{defn}
	$\prec$ je zjednotenie všetkých simulácií
\end{defn}

% */

\section{Slabá bisimulácia} % /*

\begin{defn} ~
	\begin{enumerate}
		\item $t \in Act$
		\item $\stackrel{\land}{t} \in Act^*$
		\item $Act = A \cup \{\tau\}$
	\end{enumerate}
\end{defn}

\begin{defn}[Slabá bisimulácia]
	Binárna relácia $S \subseteq \mathcal{P}\times\mathcal{P}$ je {\it slabá bisimulácia}, ak $(P,Q)
	\in S$ implikuje, že pre $\forall x \in Act$ platí:
	\begin{enumerate}
		\item Ak $P\stackrel{x}{\to}P'$ potom $\exists Q':
			Q\stackrel{\stackrel{\land}{x}}{\Rightarrow}Q'$ a $(P',Q') \in S$
		\item Ak $Q\stackrel{x}{\to}Q'$ potom $\exists P':
			P\stackrel{\stackrel{\land}{x}}{\Rightarrow}P'$ a $(P',Q') \in S$
	\end{enumerate}
\end{defn}

\begin{defn}
	$\approx = \cup\{S ~|~ S$ je slabá bisimulácia$\}$
\end{defn}

\begin{defn}
	Procesy $P$ a $Q$ sú slabo bisimulárne, ak existuje taká slabá bisimulácia $S$, že $(P,Q) \in
	S$.
\end{defn}

\begin{veta}
	Ak $S_1, S_2$ sú slabé bisimulácie, tak potom aj:
	\begin{enumerate}
		\item $I_d$
		\item $S^{-1}_i$
		\item $S_1 \circ S_2$
		\item $S_1 \cup S_2$
	\end{enumerate}
	sú slabé bisimulácie.
\end{veta}

\begin{veta} ~
	\begin{enumerate}
		\item $\approx$ je ekvivalencia
		\item $\approx$ je najväčšia slabá bisimulácia
	\end{enumerate}
\end{veta}

\begin{veta}
	$P \approx Q \iff \forall x \in Act:$
	\begin{enumerate}
		\item Ak $P\stackrel{x}{\to}P'$ potom $\exists Q':
			Q\stackrel{\stackrel{\land}{x}}{\Rightarrow}Q'$ a $P' \approx Q'$
		\item Ak $Q\stackrel{x}{\to}Q'$ potom $\exists P':
			P\stackrel{\stackrel{\land}{x}}{\Rightarrow}P'$ a $P' \approx Q'$
	\end{enumerate}
\end{veta}

% */

\section{Slabá bisimulácia až na $\approx$} % /*

\begin{defn}
	$S$ je {\it slabá bisimulácia až na $\approx$}, ak $PSQ$ implikuje $\forall x \in Act$
	\begin{enumerate}
		\item Ak $P\stackrel{x}{\to}P'$ potom $\exists Q':
			Q\stackrel{\stackrel{\land}{x}}{\Rightarrow}Q'$ a $P' \sim S \sim Q'$
		\item Ak $Q\stackrel{x}{\to}Q'$ potom $\exists P':
			P\stackrel{\stackrel{\land}{x}}{\Rightarrow}P'$ a $P' \sim S \sim Q'$
	\end{enumerate}
\end{defn}

\begin{veta}
	Ak $S$ je slabá bisimulácia až na $\approx$, tak $\approx S \approx$ je slabá bisimulácia.
\end{veta}

\begin{veta}
	Ak $S$ je slabá bisimulácia až na $\approx$, tak $S \subseteq \approx$.
\end{veta}

\begin{veta}
	$P \approx \tau P$
\end{veta}

\begin{veta} Nech $P \approx Q$, potom
	\begin{enumerate}
		\item $xP \approx Q$
		\item $P|R \approx R|P$
		\item $P+R \approx Q+R$ neplatí
		\item $P[f] \approx Q[f]$
		\item $P\setminus L \approx Q \setminus L$
	\end{enumerate}
\end{veta}

\begin{veta}[Observation kongruent]
	TODO
\end{veta}

\begin{veta} ~
	\begin{enumerate}
		\item $P \sim Q \Rightarrow P = Q$
		\item $P = Q \Rightarrow P \approx Q$
	\end{enumerate}

	Teda: $\sim \le = \le \approx$
\end{veta}

\begin{example} Nájdite:
	\begin{enumerate}
		\item $P = Q$, ale $P \not \sim Q$
		\item $P \approx Q$, ale $P \not = Q$
	\end{enumerate}
\end{example}

% */

% vim: ts=4 tw=100
% vim600: fdl=0 fdm=marker fdc=0 fmr=/*,*/