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