Up to [Platon] / doc / statnica-teoria-prog

Update

%
% 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=/*,*/