%
% 04-semantika-programovaich-jazykov.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/04-semantika-programovaich-jazykov.tex,v 1.1 2006-08-17 08:04:27 nepto Exp $
\chapter{Sémantika programovacích jazykov}
\section{Modálne vlastnosti} % /*
\begin{defn}[Hennesy-Milner Logic]
$$
\phi = true ~|~ false ~|~ \phi_1 \land \phi_2 ~|~ \phi_1 \lor \phi_2 ~|~ [k]\phi ~|~ \langle k \rangle
\phi, k \in Act
$$
\end{defn}
\begin{defn} ~
\begin{enumerate}
\item $P \models true$
\item $P \models ff$
\item $P \models \phi \land \psi \iff P \models \phi \land P \models \psi$
\item $P \models \phi \lor \psi \iff P \models \phi \lor P \models \psi$
\item $P \models [k]\phi \iff \forall R \in \{P'~|~P\stackrel{x}{\to}P' \land x \in K\}
~ R \models \phi$
\item $P \models \langle k \rangle\phi \iff \exists R \in \{P'~|~P\stackrel{x}{\to}P' \land
x \in K\} ~ R \models \phi$
\end{enumerate}
\end{defn}
\begin{defn} ~
\begin{enumerate}
\item $-K$ znamená $Act \setminus K$
\item $-a_1 ... a_n$ znamena $Act \setminus \{a_1 ... a_n\}$
\item $-$ znamená $Act \setminus \emptyset = Act$
\end{enumerate}
\end{defn}
\begin{defn} Výraz $\langle k \rangle tt \land [-k]ff \land [-]\phi$ znamená "len akcia $K$ a bude
platiť $\phi$". Označujeme $(K)\phi$.
\end{defn}
\begin{defn} ~
\begin{enumerate}
\item $P \models \lb ~ \rb\phi \iff \forall R \in \{P'~|~P\stackrel{\epsilon}{\to}P'\}
~ R \models \phi$
\item $P \models \lc ~ \rc\phi \iff \exists R \in \{P'~|~P\stackrel{\epsilon}{\to}P'\}
~ R \models \phi$
\end{enumerate}
\end{defn}
\begin{defn} ~
\begin{enumerate}
\item $D_0 = \tau . Nil$, $D_{n+1} = \tau D_n$
\item $D_0^a = a . Nil$, $D_{n+1}^a = \tau D_n^a$
\end{enumerate}
\end{defn}
\begin{defn}
Velkosť formuly, tj. počet výskytov $\land, \lor, [k], \langle k \rangle$ budeme označovať
$|\Psi|$.
\end{defn}
% */
\section{Image finite} % /*
\begin{defn}
Proces $P$ voláme {\it bezprostredne image finite}, ak množina $\{P ~|~ P\stackrel{x}{\to}P'$ je
konečná pre všetky $x$.
\end{defn}
\begin{defn}
Proces $P$ voláme {\it image finite}, ak každý prvok $\{P ~|~ P\stackrel{b}{\to}P', b \in Act^*$ je
bezprostredne image finite.
\end{defn}
\begin{veta}
Ak procesy $P$ a $R$ sú image finite a platí $P \models \psi$ a tiež $R \models \psi$, potom $P
\sim R$.
\end{veta}
% */
\section{Transition closed} % /*
\begin{defn}
Množina $\epsilon$ je {\it transition closed}, ak
$$
E \in \epsilon \land E \stackrel{x}{\to} F \Rightarrow F \in \epsilon
$$
\begin{enumerate}
\item $\mathcal{P}$ je neprázdna transition closed množina
\item $\mathcal{P}(E)$ je najmenšia transition closed množina, ktorá obsahuje $E$
\end{enumerate}
\end{defn}
\begin{defn}[Modálny Mu-kalkulus]
$$
\phi = Z ~|~ \phi_1 \land \phi_2 ~|~ \phi_1 \lor \phi_2 ~|~ [k]\phi ~|~ \langle k \rangle \phi
~|~ \nu Z \phi ~|~ \mu Z \phi
$$
\begin{itemize}
\item[--] $Z$ je propozičná premenná
\item[--] $\nu Z, \mu Z$ sú operátory prevných bodov
\item[--] $\nu Z \phi, \mu Z \phi$ -- $Z$ je viazaná
\item[--] $tt =^{def} \nu Z.Z$
\item[--] $ff =^{def} \mu Z.Z$
\end{itemize}
Nech $P$ je transition closed množina pocesov. $P \models^{?} \phi$ Problém je s def. $P \models
\mu Z \phi$ a $P \models \nu Z \phi$.
\end{defn}
\begin{veta}
Nech $P \models \phi$, potom $\exists P'$, že $P'$ má konečný počet stavov a $P' \models \phi$.
\end{veta}
% */
\section{Verifikácia temporárnych vlastností} % /*
Problém $E \models \phi$
Hry a v nich 2 hráči:
\begin{itemize}
\item[--] Hráč 1 sa snaží ukázať $E \not \models \phi$.
\item[--] Hráč 2 sa snaží ukázať opak.
\end{itemize}
Hra so začiatkom $(E_0, \phi_0)$ je konečná alebo nekonečná postupnosť
$$
(E_0,\phi_0) ... (E_n, \phi_n) ...
$$
Hráč 1 ťahá keď $\phi$ má tvar $\land, [k], \nu Z.\psi$.\\
Hráč 2 ťahá keď $\phi$ má tvar $\lor, \langle k \rangle, \mu Z.\psi$.
% */
% vim: ts=4 tw=100
% vim600: fdl=0 fdm=marker fdc=0 fmr=/*,*/
Platon Group <platon@platon.org> http://platon.org/
|