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.3 and 1.4


version 1.3, 2006/08/18 10:25:42
version 1.4, 2006/08/18 19:32:24



Line 10 




Line 10 




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


 %
 %


 
 


 % $Platon: doc/statnica-teoria-prog/03-modely-konkurentnych-systemov.tex,v 1.2 2006-08-17 21:22:49 nepto Exp $
 % $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}
 \chapter{Modely konkurentných systémov}


 
 




Line 54 




Line 54 




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


 \end{defn}
 \end{defn}


 
 


 \begin{veta}
 \begin{veta} ~


         $\sim$ je ekvivalencia a najväčšia silná bisimulácia.
         \begin{enumerate}


 
                 \item $\sim$ je ekvivalencia


 
                 \item $\sim$ je najväčšia silná bisimulácia


 
         \end{enumerate}


 \end{veta}
 \end{veta}


 
 


 \begin{veta}
 \begin{veta}




Line 182 




Line 185 




 \begin{defn}
 \begin{defn}


         Relácia $R$ je simulácia ak $PRQ$ implikuje
         Relácia $R$ je simulácia ak $PRQ$ implikuje


         $$
         $$


         P\stackrel{x}{\to}P' \exists Q': Q\stackrel{x}{\to}Q' \land P'RQ'
         P\stackrel{x}{\to}P': \exists Q': Q\stackrel{x}{\to}Q' \land P'RQ'


         $$
         $$


 \end{defn}
 \end{defn}


 
 




Line 194 




Line 197 




 
 


 \section{Slabá bisimulácia} % /*
 \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]
 \begin{defn}[Slabá bisimulácia]


         Binárna relácia $S \subseteq \mathcal{P}\times\mathcal{P}$ je {\it slabá bisimulácia}, ak $(P,Q)
         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í:
         \in S$ implikuje, že pre $\forall x \in Act$ platí:


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


                 \item Ak $Q\stackrel{x}{\to}Q'$ potom $\exists P': P\stackrel{\stackrel{\land}{x}}{\to}P'$ a $(P',Q') \in S$
                         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{enumerate}


 \end{defn}
 \end{defn}


 
 




Line 212 




Line 225 




         S$.
         S$.


 \end{defn}
 \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}


 
 


 % */
 % */


 
 









Legend:


Removed from v.1.3
 


changed lines


 
Added in v.1.4


















Platon Group <platon@platon.org> http://platon.org/
  Up to  [Platon] / doc / statnica-teoria-prog
-version 1.3, 2006/08/18 10:25:42
+version 1.4, 2006/08/18 19:32:24
 Line 10
 Line 10
 Line 10
  % 2006-08-17 - created
  %
- % $Platon: doc/statnica-teoria-prog/03-modely-konkurentnych-systemov.tex,v 1.2 2006-08-17 21:22:49 nepto Exp $
+ % $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}
 Line 54
 Line 54
 Line 54
          $\sim = \cup\{S ~|~ S$ je silná bisimulácia$\}$
  \end{defn}
- \begin{veta}
+ \begin{veta} ~
-         $\sim$ je ekvivalencia a najväčšia silná bisimulácia.
+         \begin{enumerate}
+                 \item $\sim$ je ekvivalencia
+                 \item $\sim$ je najväčšia silná bisimulácia
+         \end{enumerate}
  \end{veta}
  \begin{veta}
-Line 182
+Line 185
 Line 182
 Line 185
  \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'
+         P\stackrel{x}{\to}P': \exists Q': Q\stackrel{x}{\to}Q' \land P'RQ'
          $$
  \end{defn}
-Line 194
+Line 197
 Line 194
 Line 197
  \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}}{\to}Q'$ a $(P',Q') \in S$
+                 \item Ak $P\stackrel{x}{\to}P'$ potom $\exists Q':
-                 \item Ak $Q\stackrel{x}{\to}Q'$ potom $\exists P': P\stackrel{\stackrel{\land}{x}}{\to}P'$ a $(P',Q') \in S$
+                         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}
-Line 212
+Line 225
 Line 212
 Line 225
          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}
  % */
 Legend:


Removed from v.1.3
 


changed lines


 
Added in v.1.4
 Legend:


Removed from v.1.3
 


changed lines


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


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