2martens/uni
1
0
Fork 0
mirror of https://github.com/2martens/uni.git synced 2026-05-06 11:26:25 +02:00
Code Releases Activity
Files
a51681103ae02a139b93428fd6e187ba30db6d25
uni/fgi2/Blatt5/Aufgabenblatt5.tex
Jim Martens c710912074 FGI2: 5.3.4 und 5.3.5.b bearbeitet
2014-11-13 16:13:59 +01:00

292 lines
12 KiB
TeX
Raw Blame History

\documentclass[10pt,a4paper,oneside,ngerman,numbers=noenddot]{scrartcl}
\usepackage[T1]{fontenc}
\usepackage[utf8x]{inputenc}
\usepackage[ngerman]{babel}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{paralist}
\usepackage{gauss}
\usepackage{pgfplots}
\usepackage[locale=DE,exponent-product=\cdot,detect-all]{siunitx}
\usepackage{tikz}
\usetikzlibrary{automata,matrix,fadings,calc,positioning,decorations.pathreplacing,arrows,decorations.markings}
\usepackage{polynom}
\usepackage{multirow}
\usepackage[german]{fancyref}
\polyset{style=C, div=:,vars=x}
\pgfplotsset{compat=1.8}
\pagenumbering{arabic}
% ensures that paragraphs are separated by empty lines
\parskip 12pt plus 1pt minus 1pt
\parindent 0pt
% define how the sections are rendered
\def\thesection{5.\arabic{section})}
\def\thesubsection{\arabic{subsection}.}
\def\thesubsubsection{(\alph{subsubsection})}
% some matrix magic
\makeatletter
\renewcommand*\env@matrix[1][*\c@MaxMatrixCols c]{%
\hskip -\arraycolsep
\let\@ifnextchar\new@ifnextchar
\array{#1}}
\makeatother
\begin{document}
\author{Benjamin Kuffel, Jim Martens\\Gruppe 6}
\title{Hausaufgaben zum 17. November}
\maketitle
\setcounter{section}{2}
\section{} %4.3
\subsection{}
Der Abwicklungsbaum befindet sich auf \fref{fig:531}.
\begin{figure}
\begin{tikzpicture}[node distance=1cm]
\node[state,initial] (s0start) {\(\{b\}\)};
\node (t0start) [above=0.0001 of s0start] {\(s_{0}\)};
\node[state] (s01) [below left=of s0start] {\(\{b\}\)};
\node (t01) [above=0.0001 of s01] {\(s_{0}\)};
\node[state] (s11) [below right=of s0start] {\(\{s\}\)};
\node (t11) [above=0.0001 of s11] {\(s_{1}\)};
\node[state] (s02) [below left=of s01] {\(\{b\}\)};
\node (t02) [above=0.0001 of s02] {\(s_{0}\)};
\node[state] (s12) [below right=of s01] {\(\{s\}\)};
\node (t12) [above=0.0001 of s12] {\(s_{1}\)};
\node[state] (s22) [below right=of s11] {\(\{g\}\)};
\node (t22) [above=0.0001 of s22] {\(s_{2}\)};
\node[state] (s03) [below left=of s02] {\(\{b\}\)};
\node (t03) [above=0.0001 of s03] {\(s_{0}\)};
\node[state] (s13) [below right=of s02] {\(\{s\}\)};
\node (t13) [above=0.0001 of s13] {\(s_{1}\)};
\node[state] (s23) [below right=of s12] {\(\{g\}\)};
\node (t23) [above=0.0001 of s23] {\(s_{2}\)};
\node[state] (s23-1) [below right=of s22] {\(\{g\}\)};
\node (t23-1) [above=0.0001 of s23-1] {\(s_{2}\)};
\node[state] (s04) [below left=of s03] {\(\{b\}\)};
\node (t04) [above=0.0001 of s04] {\(s_{0}\)};
\node[state] (s14) [below right=of s03] {\(\{s\}\)};
\node (t14) [above=0.0001 of s14] {\(s_{1}\)};
\node[state] (s24) [below right=of s13] {\(\{g\}\)};
\node (t24) [above=0.0001 of s24] {\(s_{2}\)};
\node[state] (s24-1) [below right=of s23] {\(\{g\}\)};
\node (t24-1) [above=0.0001 of s24-1] {\(s_{2}\)};
\node[state] (s24-2) [below right=of s23-1] {\(\{g\}\)};
\node (t24-2) [above=0.0001 of s24-2] {\(s_{2}\)};
\path[->] (s0start) edge (s01)
(s0start) edge (s11)
(s01) edge (s02)
(s01) edge (s12)
(s11) edge (s22)
(s02) edge (s03)
(s02) edge (s13)
(s12) edge (s23)
(s22) edge (s23-1)
(s03) edge (s04)
(s03) edge (s14)
(s13) edge (s24)
(s23) edge (s24-1)
(s23-1) edge (s24-2);
\end{tikzpicture}
\caption{Abwicklungsbaum \(Abwicklung_{AKW}\) der Tiefe 4}
\label{fig:531}
\end{figure}
\subsection{}
\subsubsection{}
\[Sat(\alpha _{1}) = \{s_{0},s_{1},s_{2}\}\]
\subsubsection{}
\[Sat(\textbf{AG}\alpha _{1}) = \{s_{0},s_{1},s_{2}\}\]
\subsubsection{}
\[Sat(\textbf{EG}\lnot b) = \{s_{1},s_{2}\} \]
\subsubsection{}
\[Sat(\textbf{AX}\lnot g) = \{s_{0}\} \]
\subsection{}
\(\beta _{1} = \textbf{AGEX}(s \vee g)\) bedeutet, dass für alle Pfade immer gilt, dass es einen Pfad gibt, für den im nächsten Schritt \(s\) oder \(g\) gilt.
\(\beta _{2} = \textbf{EG}\lnot b\) bedeutet, dass es einen Pfad gibt, für den immer \(\lnot b\) gilt.
\subsubsection{}
\(\beta _{1}\) gilt nach 5.3.2.(b) für alle Zustände und somit auch für den Startzustand. Damit gilt \(M_{AKW} \models \textbf{AGEX}(s \vee g)\).
\subsubsection{}
\(\beta _{2}\) gilt nach 5.3.2.(c) nur für \(s_{1}\) und \(s_{2}\) und somit nicht für den Startzustand. Damit gilt \(M_{AKW} \models \textbf{EG}\lnot b\) nicht.
\subsection{}
\subsubsection{}
Es ist zu beweisen, dass für alle Aussagen \(a\) folgendes gilt: \(\textbf{AGAX}a \equiv \textbf{AXAG}a\).
Dazu wird für beide Seiten der Abwicklungsbaum (ohne konkrete Formel ist dies nur abstrakt möglich) konstruiert. Der Baum für die linke Seite ist auf \fref{fig:ABaum1} zu sehen. Der für die rechte Seite auf \fref{fig:ABaum2}.
Wie aus den Bäumen hervorgeht, sind beide Formel äquivalent. Zur Sicherung dieses vordergründigen Ergebnisses, werden nun die Zustände, in denen die Formel gilt, nach dem Verfahren aus Aufgabe 5.4.2. Dazu werden die Formeln zunächst in die Normalform überführt.
Linke Seite:
\[AGAX a = AG\lnot EX(\lnot a) = \lnot EF(EX(\lnot a))\]
Rechte Seite:
\[AXAG a = AX\lnot EF(\lnot a) = \lnot EX(EF(\lnot a))\]
Nach dem Verfahren ergibt sich folgende Tabelle.
\begin{tabular}{c|c|c|c}
Teilformel & Zustand \(s_{0}\) & Zustand \(s_{1}\) & Zustand \(s_{2}\) \\
\hline
\hline
\(a\) & ? & + & + \\
\(\lnot a\) & ? & -- & -- \\
\(\textbf{EX}\lnot a\) & -- & -- & -- \\
\(\textbf{EF}(\textbf{EX}\lnot a) \) & -- & -- & -- \\
\(\lnot \textbf{EF}(\textbf{EX}\lnot a) \) & + & + & + \\
\(\textbf{EF} \lnot a\) & -- & -- & -- \\
\(\textbf{EX}(\textbf{EF} \lnot a) \) & -- & -- & -- \\
\(\lnot \textbf{EX}(\textbf{EF} \lnot a) \) & + & + & + \\
\end{tabular}
Anhand der Tabelle erschließt sich ebenso, dass beide Formeln äquivalent sind und genau dann im Startzustand gelten, wenn die jeweilige andere Formel ebenso gilt.
\begin{figure}
\begin{tikzpicture}[node distance=1cm]
\node[state,initial] (something) {\(true\)};
\node (tsomething) [above=0.0001 of something] {\(s_{0}\)};
\node[state] (al) [below left=1 and 3 of something] {\(\{a\}\)};
\node (tal) [above=0.0001 of al] {\(s_{1}\)};
\node[state] (all) [below left=1 and 1.5 of al] {\(\{a\}\)};
\node (tall) [above=0.0001 of all] {\(s_{3}\)};
\node[state] (alr) [below right=1 and 1.5 of al] {\(\{a\}\)};
\node (talr) [above=0.0001 of alr] {\(s_{4}\)};
\node (allli) [below left=of all] {...};
\node (allri) [below right=of all] {...};
\node (alrli) [below left=of alr] {...};
\node (alrri) [below right=of alr] {...};
\node[state] (ar) [below right=1 and 3 of something] {\(\{a\}\)};
\node (tar) [above=0.0001 of ar] {\(s_{2}\)};
\node[state] (arl) [below left=1 and 1.5 of ar] {\(\{a\}\)};
\node (tarl) [above=0.0001 of arl] {\(s_{5}\)};
\node[state] (arr) [below right=1 and 1.5 of ar] {\(\{a\}\)};
\node (tarr) [above=0.0001 of arr] {\(s_{6}\)};
\node (arlli) [below left=of arl] {...};
\node (arlri) [below right=of arl] {...};
\node (arrli) [below left=of arr] {...};
\node (arrri) [below right=of arr] {...};
\path[->] (something) edge (al)
(something) edge (ar)
(al) edge (all)
(al) edge (alr)
(ar) edge (arl)
(ar) edge (arr)
(all) edge (allli)
(all) edge (allri)
(alr) edge (alrli)
(alr) edge (alrri)
(arr) edge (arrli)
(arr) edge (arrri)
(arl) edge (arlli)
(arl) edge (arlri);
\end{tikzpicture}
\caption{Abwicklungsbaum für \(\textbf{AGAX}a\)}
\label{fig:ABaum1}
\end{figure}
\begin{figure}
\begin{tikzpicture}[node distance=1cm]
\node[state,initial] (something) {\(true\)};
\node (tsomething) [above=0.0001 of something] {\(s_{0}\)};
\node[state] (al) [below left=1 and 3 of something] {\(\{a\}\)};
\node (tal) [above=0.0001 of al] {\(s_{1}\)};
\node[state] (all) [below left=1 and 1.5 of al] {\(\{a\}\)};
\node (tall) [above=0.0001 of all] {\(s_{3}\)};
\node[state] (alr) [below right=1 and 1.5 of al] {\(\{a\}\)};
\node (talr) [above=0.0001 of alr] {\(s_{4}\)};
\node (allli) [below left=of all] {...};
\node (allri) [below right=of all] {...};
\node (alrli) [below left=of alr] {...};
\node (alrri) [below right=of alr] {...};
\node[state] (ar) [below right=1 and 3 of something] {\(\{a\}\)};
\node (tar) [above=0.0001 of ar] {\(s_{2}\)};
\node[state] (arl) [below left=1 and 1.5 of ar] {\(\{a\}\)};
\node (tarl) [above=0.0001 of arl] {\(s_{5}\)};
\node[state] (arr) [below right=1 and 1.5 of ar] {\(\{a\}\)};
\node (tarr) [above=0.0001 of arr] {\(s_{6}\)};
\node (arlli) [below left=of arl] {...};
\node (arlri) [below right=of arl] {...};
\node (arrli) [below left=of arr] {...};
\node (arrri) [below right=of arr] {...};
\path[->] (something) edge (al)
(something) edge (ar)
(al) edge (all)
(al) edge (alr)
(ar) edge (arl)
(ar) edge (arr)
(all) edge (allli)
(all) edge (allri)
(alr) edge (alrli)
(alr) edge (alrri)
(arr) edge (arrli)
(arr) edge (arrri)
(arl) edge (arlli)
(arl) edge (arlri);
\end{tikzpicture}
\caption{Abwicklungsbaum für \(\textbf{AXAG}a\)}
\label{fig:ABaum2}
\end{figure}
\subsubsection{}
Es ist zu beweisen, dass für alle Aussagen \(s\) die folgende Formel nicht gilt: \(\textbf{EXEG}s \equiv \textbf{EGEX}s\). Dies kann in Bezug zu \(M_{AKW}\) anhand der Aussage \(s\) gezeigt werden. Es wird erneut die Tabelle zur Ermittlung der entsprechenden Zustände aufgestellt. In diesem Fall wird ebenso auf das Verfahren aus Aufgabe 5.4.2 zurückgegriffen.
\begin{tabular}{c|c|c|c}
Teilformel & Zustand \(s_{0}\) & Zustand \(s_{1}\) & Zustand \(s_{2}\) \\
\hline
\hline
\(s\) & -- & + & -- \\
\(\textbf{EX} s\) & + & + & -- \\
\(\textbf{EGEX}s\) & + & -- & -- \\
\(\textbf{EG}s\) & -- & -- & -- \\
\(\textbf{EXEG}s\) & -- & -- & --
\end{tabular}
Anhand der Tabelle ist klar ersichtlich, dass \(\textbf{EGEX}s\) im Startzustand und damit im betrachteten Modell gilt, wohingegen \(\textbf{EXEG}s\) nicht im Startzustand gilt. Damit ist die notwenige Biimplikation zur Gültigkeit nicht gegeben, was bedeutet, dass die betrachteten Formeln nicht äquivalent sind.
\subsection{}
\subsubsection{}
\subsubsection{}
Es ist zu beweisen, dass für alle Aussagen \(s\) die folgende Äquivalenz nicht gilt: \(\textbf{EG}\lnot s \equiv G \lnot s\).
Dies kann wieder anhand der bereits mehrfach verwendeten Tabelle und in Bezug auf \(M_{AKW}\) geschehen.
\begin{tabular}{c|c|c|c}
Teilformel & Zustand \(s_{0}\) & Zustand \(s_{1}\) & Zustand \(s_{2}\) \\
\hline
\hline
\(s\) & -- & + & -- \\
\(\lnot s\) & + & -- & + \\
\(\textbf{EG}\lnot s\) & + & -- & + \\
\(\textbf{G}\lnot s\) & -- & -- & +
\end{tabular}
Anhand der Tabelle ist ersichtlich, dass \(\textbf{EG}\lnot s\) im Startzustand und damit dem Modell gilt, wohingegen \(\textbf{G}\lnot s\) nicht im Startzustand gilt. Damit ist die notwendige Biimplikation nicht gegeben und die Formeln sind daher nicht äquivalent.
\section{} %4.4
\subsection{}
Umwandeln von \(\beta _{1}\) in \(\beta '_{1}\):
\[\beta '_{1} = \lnot EF(\lnot EX \lnot s)\]
Umwandeln von \(\beta _{2}\) in \(\beta '_{2}\):
\[\beta '_{2} = EX(\lnot EF s)\]
\subsection{}
\begin{tabular}{c|c|c|c}
Teilformel & Zustand \(s_{0}\) & Zustand \(s_{1}\) & Zustand \(s_{2}\) \\
\hline
\hline
\(s\) & -- & + & -- \\
\(\lnot s\) & + & -- & + \\
\(\textbf{EX}\lnot s\) & + & + & + \\
\(\lnot \textbf{EX}\lnot s\) & -- & -- & -- \\
\(\textbf{EF}(\lnot \textbf{EX}\lnot s) \) & -- & -- & -- \\
\(\lnot \textbf{EF}(\lnot \textbf{EX}\lnot s) \) & + & + & + \\
\(\textbf{EF}s\) & + & + & -- \\
\(\lnot \textbf{EF}s\) & -- & -- & + \\
\(\textbf{EX}(\lnot \textbf{EF}s) \) & -- & + & +
\end{tabular}
\subsection{}
\(M_{AKW} \models \beta _{1}\) gilt, aber \(M_{AKW} \models \beta _{2}\) gilt nicht.
\end{document}
View Git Blame Copy Permalink