Platon Technologies
not logged in Login Registration
EnglishSlovak
open source software development celebrating 10 years of open source development! Sunday, October 18, 2026
[BACK] [TXT][DIR] Up to [Platon] / doc / statnica-teoria-prog

Diff for doc/statnica-teoria-prog/03-modely-konkurentnych-systemov.tex between version 1.1 and 1.2

version 1.1, 2006/08/17 08:04:27 version 1.2, 2006/08/17 21:22:49
Line 10 
Line 10 
 % 2006-08-17 - created  % 2006-08-17 - created
 %  %
   
 % $Platon: $  % $Platon: doc/statnica-teoria-prog/03-modely-konkurentnych-systemov.tex,v 1.1 2006-08-17 08:04:27 nepto Exp $
   
 \chapter{Modely konkurentných systémov}  \chapter{Modely konkurentných systémov}
   
   \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}
           $\sim$ je ekvivalencia a najväčšia silná bisimulácia.
   \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}
   
   \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}
   
 % vim: ts=4 tw=100  % vim: ts=4 tw=100
 % vim600: fdl=0 fdm=marker fdc=0 fmr=/*,*/  % vim600: fdl=0 fdm=marker fdc=0 fmr=/*,*/
   
Legend:
Removed from v.1.1  
changed lines
  Added in v.1.2
Platon Group <platon@platon.org> http://platon.org/
Copyright © 2002-2006 Platon Group
Site powered by Metafox CMS 		Go to Top