Platon Technologies
not logged in Login Registration
EnglishSlovak
open source software development celebrating 10 years of open source development! Friday, March 29, 2024

File: [Platon] / doc / statnica-teoria-prog / 04-semantika-programovaich-jazykov.tex (download)

Revision 1.2, Fri Aug 18 23:29:56 2006 UTC (17 years, 7 months ago) by nepto


Changes since 1.1: +133 -1 lines

Another chapter

%
% 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/
Copyright © 2002-2006 Platon Group
Site powered by Metafox CMS
Go to Top