Opensource.Platon.SK CVS: doc/statnica-teoria-prog/03-modely-konkurentnych-systemov.tex - diff

   Up to  [Platon] / doc / statnica-teoria-prog
Diff for doc/statnica-teoria-prog/03-modely-konkurentnych-systemov.tex between version 1.2 and 1.3


version 1.2, 2006/08/17 21:22:49
version 1.3, 2006/08/18 10:25:42



Line 10 




Line 10 




 % 2006-08-17 - created
 % 2006-08-17 - created


 %
 %


 
 


 % $Platon: doc/statnica-teoria-prog/03-modely-konkurentnych-systemov.tex,v 1.1 2006-08-17 08:04:27 nepto Exp $
 % $Platon: doc/statnica-teoria-prog/03-modely-konkurentnych-systemov.tex,v 1.2 2006-08-17 21:22:49 nepto Exp $


 
 


 \chapter{Modely konkurentných systémov}
 \chapter{Modely konkurentných systémov}


 
 


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


 
 


 \begin{defn}
 \begin{defn}


         Množina akcií $Act = A \cup \overline{A} \cup \{\tau\}$, kde:
         Množina akcií $Act = A \cup \overline{A} \cup \{\tau\}$, kde:


         \begin{enumerate}
         \begin{enumerate}




Line 64 




Line 66 




         \end{enumerate}
         \end{enumerate}


 \end{veta}
 \end{veta}


 
 


 
 % */


 
 


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


 
 


 \begin{defn}
 \begin{defn}


         $S$ je {\it silná bisimulácia až na $\sim$}, ak $PSQ$ implikuje $\forall x \in Act$
         $S$ je {\it silná bisimulácia až na $\sim$}, ak $PSQ$ implikuje $\forall x \in Act$


         \begin{enumerate}
         \begin{enumerate}




Line 112 




Line 118 




         $$
         $$


 \end{veta}
 \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}[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}}{\to}Q'$ a $(P',Q') \in S$


 
                 \item Ak $Q\stackrel{x}{\to}Q'$ potom $\exists P': P\stackrel{\stackrel{\land}{x}}{\to}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}


 
 


 
 


 
 % */


 
 


 % 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.2
 


changed lines


 
Added in v.1.3


















Platon Group <platon@platon.org> http://platon.org/
  Up to  [Platon] / doc / statnica-teoria-prog
-version 1.2, 2006/08/17 21:22:49
+version 1.3, 2006/08/18 10:25:42
 Line 10
 Line 10
 Line 10
  % 2006-08-17 - created
  %
- % $Platon: doc/statnica-teoria-prog/03-modely-konkurentnych-systemov.tex,v 1.1 2006-08-17 08:04:27 nepto Exp $
+ % $Platon: doc/statnica-teoria-prog/03-modely-konkurentnych-systemov.tex,v 1.2 2006-08-17 21:22:49 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}
-Line 64
+Line 66
 Line 64
 Line 66
          \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}
-Line 112
+Line 118
 Line 112
 Line 118
          $$
  \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}[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}}{\to}Q'$ a $(P',Q') \in S$
+                 \item Ak $Q\stackrel{x}{\to}Q'$ potom $\exists P': P\stackrel{\stackrel{\land}{x}}{\to}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}
+ % */
  % vim: ts=4 tw=100
  % vim600: fdl=0 fdm=marker fdc=0 fmr=/*,*/
 Legend:


Removed from v.1.2
 


changed lines


 
Added in v.1.3
 Legend:


Removed from v.1.2
 


changed lines


 
Added in v.1.3
-Removed from v.1.2
+Added in v.1.3


Copyright © 2002-2006 Platon Group Site powered by Metafox CMS	Go to Top