API tools faq
paste
Advertisement
Guest User

Untitled

a guest
Jul 5th, 2019
79
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
Latex 21.84 KB | None | 0 0
raw download clone embed print report
  1. \documentclass{article}
  2. \usepackage[utf8]{inputenc}
  3. \usepackage{ReSyst.Macros}
  4. \usepackage{mathtools}
  5. \usepackage{amsmath,amsfonts,amssymb}
  6. \usepackage[arrow, matrix, curve]{xy}
  7. \RequirePackage{etoolbox}
  8. \usepackage{xifthen}
  9. \usepackage{semantic}
  10. \usepackage{tikz}
  11. \usepackage{amssymb}
  12. \usepackage{dsfont}
  13. \usepackage{amsmath}
  14. \usepackage{natbib}
  15. \usepackage{graphicx}
  16.  
  17. \newcommand{\hmlbr}[1]{$\llbracket\ #1\ \rrbracket$}
  18. \newcommand{\daexists}[1]{$\langle \cdot#1\cdot\rangle$}
  19. \newcommand{\aexists}[1]{$\langle#1\rangle$}
  20. \newcommand{\bunch}[1]{\{#1\}}
  21. \newcommand{\dforalla}[1]{[\cdot#1\cdot]}
  22. \newcommand{\foralla}[1]{[#1]}
  23. \newcommand{\ftrue}{\emph{tt}}
  24. \newcommand{\ffalse}{\emph{ff}}
  25. \newcommand{\daexistsm}[1]{\langle \cdot#1\cdot\rangle}
  26. \newcommand{\aexistsm}[1]{\langle#1\rangle}
  27. \newcommand{\Uw}{\MC{U}^w}
  28. \newcommand{\Us}{\MC{U}^s}
  29.  
  30.  
  31. \newcommand{\nil}{\ensuremath{\mathbf{0}}}
  32. \newcommand{\Proc}{\ensuremath{\mathsf{Proc}}}
  33. \newcommand{\Act}{\ensuremath{\mathsf{Act}}}
  34. \newcommand{\Tran}{\ensuremath{\mathsf{Tran}}}
  35. \newcommand{\Lab}{\MC{L}}
  36. \newcommand{\Exp}{\MC{E}}
  37. \newcommand{\Val}{\MC{V}}
  38. \newcommand{\Var}{\MC{X}}
  39. \newcommand{\Traces}[1]{\ensuremath{\ON{Traces}(#1)}}
  40. \newcommand{\Id}{\ON{Id}}
  41. \newcommand{\Der}[1]{\ensuremath{\ON{Der}(#1, \alpha)}}
  42. \newcommand{\A}{\MC{A}}
  43. \newcommand{\Abar}{\ensuremath{\mkern 7mu\overline{\mkern-7mu\A}}}
  44. \newcommand{\Lang}{\MC{L}}
  45. \newcommand{\Const}{\MC{K}}
  46. \newcommand{\bisim}{\ensuremath{\sim}}
  47. \newcommand{\wbisim}{\ensuremath{\approx}}
  48. \newcommand{\nbisim}{\ensuremath{\nsim}}
  49. \newcommand{\nwbisim}{\ensuremath{\napprox}}
  50. \newcommand{\NCCSTrans}[1]{\ensuremath{\centernot{\stackrel{\ifthenelse{\isempty{#1}}{}{\text{#1}}}{\to}}}}
  51. \newcommand{\WCCSTrans}[1]{\ensuremath{\stackrel{\ifthenelse{\isempty{#1}}{}{\text{#1}}}{\Rightarrow}}}
  52. \newcommand{\NWCCSTrans}[1]{\ensuremath{\centernot{\stackrel{\ifthenelse{\isempty{#1}}{}{\text{#1}}}{\Rightarrow}}}}
  53. \newcommand{\truet}{\ensuremath{\textit{t}\!\textit{t}}}
  54. \newcommand{\falsef}{\ensuremath{\textit{f}\!\textit{f}}}
  55. \newcommand\lbr{\llbracket}
  56. \newcommand\rbr{\rrbracket}
  57. \newcommand\denot[1]{\ensuremath{\left \lbr #1 \right \rbr}}
  58. \newcommand{\possDenot}[1]{\ensuremath{\langle \cdot \, \text{#1} \, \cdot \rangle}}
  59. \newcommand{\necessDenot}[1]{\ensuremath{[ \cdot \, \text{#1} \, \cdot ] }}
  60. \newcommand{\HMmax}{\ensuremath{\stackrel{\text{max}}{=}}}
  61. \newcommand{\HMmin}{\ensuremath{\stackrel{\text{min}}{=}}}
  62. \renewcommand{\O}[1]{\MC{O}_{#1}}
  63. \newcommand{\MCMX}{\MC{M}_{\{X\}}}
  64. \newcommand{\FIX}{\operatorname{FIX}}
  65. \newcommand{\fix}{\operatorname{fix}}
  66. \newcommand{\Inv}[1]{\textit{Inv}\,(#1)}
  67. \newcommand{\Safe}[1]{\textit{Safe}(#1)}
  68. \newcommand{\Even}[1]{\textit{Even}(#1)}
  69. \newcommand{\Pos}[1]{\textit{Pos}(#1)}
  70.  
  71. \newcommand{\MC}[1]{\ensuremath{\mathbin{\mathcal{#1}}}}
  72. \newcommand{\N}{\mathbb{N}}
  73. \newcommand{\und}{\;\text{und}\;}
  74. \renewcommand{\mit}{\;\text{mit}\;}
  75. \newcommand{\furalle}{\;\text{für alle}\;}
  76. \newcommand{\sqN}{\ensuremath{\N^{2+}}}
  77. \newcommand{\abs}[1]{\left|#1\right|}
  78. \newcommand{\norm}[1]{\left\|#1\right\|}
  79. \newcommand{\eqdef}{\stackrel{\mathclap{\normalfont\mbox{def}}}{=\joinrel=}}
  80. \newcommand{\repslash}[2]{{\raisebox{1mm}{\text{#1}}}\big/_{\raisebox{-0.5mm}{\text{#2}}}}
  81. \newcommand{\coname}[1]{\overline{\mbox{\text{#1}}\raisebox{3mm}{}}}
  82. \newcommand{\conm}[1]{\overline{\text{#1}}}
  83. \newcommand{\fixpar}{\par \vspace{2mm}}
  84. \newcommand{\pair}[2]{\left(\textbf{#1}, \textbf{#2}\right)}
  85. \newcommand{\lee}{\ensuremath{\le_2}}
  86. \newcommand{\oneton}{\left\{1, \dots, n\right\}}
  87. \newcommand{\oneto}[1]{\left\{1, \dots, #1\right\}}
  88. \newcommand{\Aufgabe}[1]{\section*{Aufgabe #1}}
  89.  
  90. \newcommand{\setsep}{\@ifstar{\setsepStar}{\setsepNoStar}}
  91. \newcommand{\setsepStar}{\ensuremath{\,|\,}}
  92. \newcommand{\setsepNoStar}{\ensuremath{\,\middle|\,}}
  93.  
  94. \newcommand{\paral}{\@ifstar{\paralStar}{\paralNoStar}}
  95. \newcommand{\paralStar}{\ensuremath{\,|\,}}
  96. \newcommand{\paralNoStar}{\ensuremath{\,\middle|\,}}
  97.  
  98. \newcommand{\tautrip}{\@ifstar{\tautripStar}{\tautripNoStar}}
  99. \newcommand{\tautripStar}[2]{\left(#1, \tau, #2\right)}
  100. \newcommand{\tautripNoStar}[2]{\left(\textbf{#1}, \tau, \textbf{#2}\right)}
  101.  
  102. \newcommand{\trantrip}{\@ifstar{\trantripStar}{\trantripNoStar}}
  103. \newcommand{\trantripStar}[3]{\left(#1, \text{#2}, #3\right)}
  104. \newcommand{\trantripNoStar}[3]{\left(\textbf{#1}, \text{#2}, \textbf{#3}\right)}
  105.  
  106. \newcommand{\cotrantrip}{\@ifstar{\cotrantripStar}{\cotrantripNoStar}}
  107. \newcommand{\cotrantripStar}[3]{\left(#1, \conm{#2}, #3\right)}
  108. \newcommand{\cotrantripNoStar}[3]{\left(\textbf{#1}, \conm{#2}, \textbf{#3}\right)}
  109.  
  110. \newcommand{\ShowBisim}[4]{\MakeBiSim{#1}{#2}{#3}{#4}{\CCSTrans}}
  111. \newcommand{\ShowWBisim}[4]{\MakeBiSim{#1}{#2}{#3}{#4}{\WCCSTrans}}
  112.  
  113. \newcommand{\poss}{\@ifstar{\possStar}{\possNoStar}}
  114. \newcommand{\possStar}[1]{\boldsymbol{\langle} \, #1 \, \boldsymbol{\rangle}}
  115. \newcommand{\possNoStar}[1]{\boldsymbol{\langle} \, \text{#1} \, \boldsymbol{\rangle}}
  116.  
  117. \newcommand{\necess}[1]{\boldsymbol{[} \, \text{#1} \, \boldsymbol{]}\,}
  118. \newcommand{\necessS}[1]{\boldsymbol{[} \, #1 \, \boldsymbol{]}\,}
  119.  
  120. \newcommand{\CCSTrans}{\@ifstar{\CCSTransStar}{\CCSTransNoStar}}
  121. \newcommand{\CCSTransStar}[1]{\ensuremath{\stackrel{\ifthenelse{\isempty{#1}}{}{#1}}{\to}}}
  122. \newcommand{\CCSTransNoStar}[1]{\ensuremath{\stackrel{\ifthenelse{\isempty{#1}}{}{\text{#1}}}{\to}}}
  123.  
  124. \title{Abgabe 4}
  125. \author{Osman Gümüs, Nicolas Philippe Kleinholz, Minh Duc Nguyen}
  126.  
  127. \begin{document}
  128.  
  129. \maketitle
  130.  
  131. \section*{Aufgabe 22: Rekursive Eigenschaften - Berechnung}
  132. \subsection*{a)}
  133. \begin{align*}
  134.    &\begin{pmatrix}
  135.        \MC{O}\textsubscript{\aexists{a}\ftrue \wedge (\foralla{b}X \land \aexists{c}Y)}(Proc, Proc)\\
  136.        \MC{O}_{\foralla{b}\ffalse \lor (\foralla{a}X \land \foralla{b}Y)}(Proc, Proc)\\
  137.    \end{pmatrix}\\
  138.    &\stackrel{Def. \MC{O}_F}{=}
  139.    \begin{pmatrix}
  140.        \daexists{a}Proc \cap (\dforalla{b}Proc \cap \daexists{c}Proc)\\
  141.        \dforalla{b}\emptyset \cup (\dforalla{a}Proc \cap \dforalla{b}Proc)\\
  142.    \end{pmatrix}\\
  143.    &\stackrel{Def. \langle \cdot\cdot\rangle, [\cdot \cdot]}{=}
  144.    \begin{pmatrix}
  145.        \bunch{p_1, p_3, p_4, p_5, p_6, p_7, p_9} \cap (Proc \cap \bunch{p_1, p_2, p_3, p_4, p_5, p_6, p_9})\\
  146.        \bunch{p_2} \cup (Proc \cap Proc)\\
  147.    \end{pmatrix}\\
  148.    &\stackrel{Def. \cap, \cup}{=}
  149.    \begin{pmatrix}
  150.        \bunch{p_1, p_3, p_4, p_5, p_6, p_9}\\
  151.        Proc\\
  152.    \end{pmatrix}\\
  153. \end{align*}
  154. \begin{align*}
  155.    &\begin{pmatrix}
  156.        \MC{O}^2\textsubscript{\aexists{a}\ftrue \wedge (\foralla{b}X \land \aexists{c}Y)}(Proc, Proc)\\
  157.        \MC{O}^2_{\foralla{b}\ffalse \lor (\foralla{a}X \land \foralla{b}Y)}(Proc, Proc)\\
  158.    \end{pmatrix}\\
  159.    &=
  160.    \begin{pmatrix}
  161.        \MC{O}\textsubscript{\aexists{a}\ftrue \wedge (\foralla{b}X \land \aexists{c}Y)}(\bunch{p_1, p_3, p_4, p_5, p_6, p_9}, Proc)\\
  162.        \MC{O}_{\foralla{b}\ffalse \lor (\foralla{a}X \land \foralla{b}Y)}(\bunch{p_1, p_3, p_4, p_5, p_6, p_9}, Proc))\\
  163.    \end{pmatrix}\\
  164.    &\stackrel{Def. \MC{O}_F}{=}
  165.    \begin{pmatrix}
  166.        \daexists{a}Proc \cap (\dforalla{b}\bunch{p_1, p_3, p_4, p_5, p_6, p_9} \cap \daexists{c}Proc)\\
  167.        \dforalla{b}\emptyset \cup (\dforalla{a}\bunch{p_1, p_3, p_4, p_5, p_6, p_9} \cap \dforalla{b}Proc)\\
  168.    \end{pmatrix}\\
  169.    &\stackrel{Def. \langle \cdot\cdot\rangle, [\cdot \cdot]}{=}
  170.    \begin{pmatrix}
  171.        \bunch{p_1, p_3, p_4, p_5, p_6, p_7, p_9} \cap (\bunch{p_1, p_2, p_3, p_4, p_6, p_9} \cap \bunch{p_1, p_2, p_3, p_4, p_5, p_6, p_9}\\
  172.        \bunch{p_2} \cup (\bunch{p_2, p_4, p_5, p_6, p_7, p_8, p_9} \cap Proc)\\
  173.    \end{pmatrix}\\
  174.    &\stackrel{Def. \cap, \cup}{=}
  175.    \begin{pmatrix}
  176.        \bunch{p_1, p_3, p_4, p_6, p_9}\\
  177.        \bunch{p_2, p_4, p_5, p_6, p_7, p_8, p_9}\\
  178.    \end{pmatrix}\\
  179. \end{align*}
  180. \begin{align*}
  181.    &\begin{pmatrix}
  182.        \MC{O}^3\textsubscript{\aexists{a}\ftrue \wedge (\foralla{b}X \land \aexists{c}Y)}(Proc, Proc)\\
  183.        \MC{O}^3_{\foralla{b}\ffalse \lor (\foralla{a}X \land \foralla{b}Y)}(Proc, Proc)\\
  184.    \end{pmatrix}\\
  185.    &=
  186.    \begin{pmatrix}
  187.        \MC{O}\textsubscript{\aexists{a}\ftrue \wedge (\foralla{b}X \land \aexists{c}Y)}(\bunch{p_1, p_3, p_4, p_6, p_9}, \bunch{p_2, p_4, p_5, p_6, p_7, p_8, p_9})\\
  188.        \MC{O}_{\foralla{b}\ffalse \lor (\foralla{a}X \land \foralla{b}Y)}(\bunch{p_1, p_3, p_4, p_6, p_9}, \bunch{p_2, p_4, p_5, p_6, p_7, p_8, p_9})\\
  189.    \end{pmatrix}\\
  190.    &\stackrel{Def. \MC{O}_F}{=}
  191.    \begin{pmatrix}
  192.        \daexists{a}Proc \cap (\dforalla{b}\bunch{p_1, p_3, p_4, p_6, p_9} \cap \daexists{c}\bunch{p_2, p_4, p_5, p_6, p_7, p_8, p_9})\\
  193.        \dforalla{b}\emptyset \cup (\dforalla{a}\bunch{p_1, p_3, p_4, p_6, p_9} \cap \dforalla{b}\bunch{p_2, p_4, p_5, p_6, p_7, p_8, p_9})\\
  194.    \end{pmatrix}\\
  195.    &\stackrel{Def. \langle \cdot\cdot\rangle, [\cdot \cdot]}{=}
  196.    \begin{pmatrix}
  197.        \bunch{p_1, p_3, p_4, p_5, p_6, p_7, p_9} \cap (\bunch{p_1, p_2, p_3, p_4, p_6, p_9} \cap \bunch{p_1, p_2, p_3, p_4, p_5}\\
  198.        \bunch{p_2} \cup (\bunch{p_2, p_5, p_6, p_7, p_8} \cap \bunch{p_1, p_2, p_5, p_6, p_7, p_8})\\
  199.    \end{pmatrix}\\
  200.    &\stackrel{Def. \cap, \cup}{=}
  201.    \begin{pmatrix}
  202.        \bunch{p_1, p_3, p_4}\\
  203.        \bunch{p_2, p_5, p_6, p_7, p_8}\\
  204.    \end{pmatrix}\\
  205. \end{align*}
  206. \begin{align*}
  207.    &\begin{pmatrix}
  208.        \MC{O}^4\textsubscript{\aexists{a}\ftrue \wedge (\foralla{b}X \land \aexists{c}Y)}(Proc, Proc)\\
  209.        \MC{O}^4_{\foralla{b}\ffalse \lor (\foralla{a}X \land \foralla{b}Y)}(Proc, Proc)\\
  210.    \end{pmatrix}\\
  211.    &=
  212.    \begin{pmatrix}
  213.        \MC{O}\textsubscript{\aexists{a}\ftrue \wedge (\foralla{b}X \land \aexists{c}Y)}(\bunch{p_1, p_3, p_4}, \bunch{p_2, p_5, p_6, p_7, p_8})\\
  214.        \MC{O}_{\foralla{b}\ffalse \lor (\foralla{a}X \land \foralla{b}Y)}(\bunch{p_1, p_3, p_4}, \bunch{p_2, p_5, p_6, p_7, p_8})\\
  215.    \end{pmatrix}\\
  216.    &\stackrel{Def. \MC{O}_F}{=}
  217.    \begin{pmatrix}
  218.        \daexists{a}Proc \cap (\dforalla{b}\bunch{p_1, p_3, p_4} \cap \daexists{c}\bunch{p_2, p_5, p_6, p_7, p_8})\\
  219.        \dforalla{b}\emptyset \cup (\dforalla{a}\bunch{p_1, p_3, p_4} \cap \dforalla{b}\bunch{p_2, p_5, p_6, p_7, p_8})\\
  220.    \end{pmatrix}\\
  221.    &\stackrel{Def. \langle \cdot\cdot\rangle, [\cdot \cdot]}{=}
  222.    \begin{pmatrix}
  223.        \bunch{p_1, p_3, p_4, p_5, p_6, p_7, p_9} \cap (\bunch{p_1, p_2, p_3, p_4} \cap \bunch{p_1, p_2, p_3, p_4, p_5, p_6, p_9}\\
  224.        \bunch{p_2} \cup (\bunch{p_2, p_7, p_8} \cap \bunch{p_2, p_5, p_6, p_7, p_8})\\
  225.    \end{pmatrix}\\
  226.    &\stackrel{Def. \cap, \cup}{=}
  227.    \begin{pmatrix}
  228.        \bunch{p_1, p_3, p_4}\\
  229.        \bunch{p_2, p_7, p_8}\\
  230.    \end{pmatrix}\\
  231. \end{align*}
  232. \begin{align*}
  233.    &\begin{pmatrix}
  234.        \MC{O}^5\textsubscript{\aexists{a}\ftrue \wedge (\foralla{b}X \land \aexists{c}Y)}(Proc, Proc)\\
  235.        \MC{O}^5_{\foralla{b}\ffalse \lor (\foralla{a}X \land \foralla{b}Y)}(Proc, Proc)\\
  236.    \end{pmatrix}\\
  237.    &=
  238.    \begin{pmatrix}
  239.        \MC{O}\textsubscript{\aexists{a}\ftrue \wedge (\foralla{b}X \land \aexists{c}Y)}(\bunch{p_1, p_3, p_4}, \bunch{p_2, p_7, p_8})\\
  240.        \MC{O}_{\foralla{b}\ffalse \lor (\foralla{a}X \land \foralla{b}Y)}(\bunch{p_1, p_3, p_4}, \bunch{p_2, p_7, p_8})\\
  241.    \end{pmatrix}\\
  242.    &\stackrel{Def. \MC{O}_F}{=}
  243.    \begin{pmatrix}
  244.        \daexists{a}Proc \cap (\dforalla{b}\bunch{p_1, p_3, p_4} \cap \daexists{c}\bunch{p_2, p_7, p_8})\\
  245.        \dforalla{b}\emptyset \cup (\dforalla{a}\bunch{p_1, p_3, p_4} \cap \dforalla{b}\bunch{p_2, p_7, p_8})\\
  246.    \end{pmatrix}\\
  247.    &\stackrel{Def. \langle \cdot\cdot\rangle, [\cdot \cdot]}{=}
  248.    \begin{pmatrix}
  249.        \bunch{p_1, p_3, p_4, p_5, p_6, p_7, p_9} \cap (\bunch{p_1, p_2, p_3, p_4} \cap \bunch{p_1, p_2, p_3, p_4, p_5, p_9})\\
  250.        \bunch{p_2} \cup (\bunch{p_2, p_7, p_8} \cap \bunch{p_2, p_7, p_8})\\
  251.    \end{pmatrix}\\
  252.    &\stackrel{Def. \cap, \cup}{=}
  253.    \begin{pmatrix}
  254.        \bunch{p_1, p_3, p_4}\\
  255.        \bunch{p_2, p_7, p_8}\\
  256.    \end{pmatrix}\\
  257. \end{align*}
  258. Damit ist der größte Fixpunkt erreicht, da\\
  259.    $
  260.    \begin{pmatrix}
  261.        \MC{O}^4\textsubscript{\aexists{a}\ftrue \wedge (\foralla{b}X \land \aexists{c}Y)}(Proc, Proc)\\
  262.        \MC{O}^4_{\foralla{b}\ffalse \lor (\foralla{a}X \land \foralla{b}Y)}(Proc, Proc)\\
  263.    \end{pmatrix}
  264.    =
  265.    \begin{pmatrix}
  266.        \MC{O}^5\textsubscript{\aexists{a}\ftrue \wedge (\foralla{b}X \land \aexists{c}Y)}(Proc, Proc)\\
  267.        \MC{O}^5_{\foralla{b}\ffalse \lor (\foralla{a}X \land \foralla{b}Y)}(Proc, Proc)\\
  268.    \end{pmatrix}
  269.    =
  270.    \begin{pmatrix}
  271.        \bunch{p_1, p_3, p_4}\\
  272.        \bunch{p_2, p_7, p_8}\\
  273.    \end{pmatrix}
  274.    $. Somit ist $\hmlbr{F} = \bunch{p_1, p_3, p_4}$.
  275. \subsubsection*{b)}
  276. $
  277. X \stackrel{min}{=} (\aexists{a}\foralla{a}\ffalse \wedge \foralla{c}Safe(\aexists{a\ftrue})) \vee \aexists{\bunch{b,c}}X
  278. \\= (\aexists{a}\foralla{a}\ffalse \wedge \foralla{c}Y) \vee \aexists{\bunch{b,c}}X
  279. $\\
  280. \text{mit } $Y \stackrel{max}{=} \aexists{a}\ftrue \wedge (\foralla{Act}\ffalse \vee \aexists{Act}X)$\\\\
  281. \text{Berechne Y wie folgt:}\\\\
  282. $
  283.    \MC{O}\textsubscript{\aexists{a}\ftrue \land (\foralla{Act}\ffalse \lor \aexists{Act}Y)}(Proc)\\
  284.    \stackrel{Def. \MC{O}_F}{=} \daexists{a}Proc \cap (\dforalla{Act}\emptyset \cup \daexists{Act}Proc)\\
  285.    \stackrel{Def. \langle \cdot\cdot\rangle, [\cdot \cdot]}{=} \bunch{p_1, p_3, p_4, p_5, p_6, p_7 p_9} \cap (\emptyset \cup Proc)\\
  286.    \stackrel{Def. \cap, \cup}{=} \bunch{p_1, p_3, p_4, p_5, p_6, p_7, p_9}\\
  287. $\\
  288. $
  289.    \MC{O}^2\textsubscript{\aexists{a}\ftrue \land (\foralla{Act}\ffalse \lor \aexists{Act}Y)}(Proc)\\
  290.    = \MC{O}\textsubscript{\aexists{a}\ftrue \land (\foralla{Act}\ffalse \lor \aexists{Act}Y)}(\bunch{p_1, p_3, p_4, p_5, p_6, p_7, p_9})\\
  291.    \stackrel{Def. \MC{O}_F}{=} \daexists{a}Proc \cap (\dforalla{Act}\emptyset \cup \daexists{Act}\bunch{p_1, p_3, p_4, p_5, p_6, p_7, p_9})\\
  292.    \stackrel{Def. \langle \cdot\cdot\rangle, [\cdot \cdot]}{=} \bunch{p_1, p_3, p_4, p_5, p_6, p_7 p_9} \cap (\emptyset \cup \bunch{p_1, p_2, p_3, p_4, p_5, p_6, p_7, p_8, p_9})\\
  293.    \stackrel{Def. \cap, \cup}{=} \bunch{p_1, p_3, p_4, p_5, p_6, p_7, p_9}\\
  294. $\\
  295. Damit ist der größte Fixpunkt von Y erreicht, da\\
  296. $
  297.    \MC{O}\textsubscript{\aexists{a}\ftrue \land (\foralla{Act}\ffalse \lor \aexists{Act}Y)}(Proc) = \MC{O}^2\textsubscript{\aexists{a}\ftrue \land (\foralla{Act}\ffalse \lor \aexists{Act}Y)}(Proc) =
  298.    \bunch{p_1, p_3, p_4, p_5, p_6, p_7, p_9}
  299. $.\\\\
  300. \text{Somit berechnet sich X wie folgt:}\\\\
  301. $
  302.    \MC{O}\textsubscript{(\aexists{a}\foralla{a}\ffalse \wedge \foralla{c}Y) \wedge \aexists{\bunch{b,c}}X}(\emptyset)\\
  303.    \stackrel{Def. \MC{O}_F, \text{Berechnung von Y}}{=} (\daexists{a}\dforalla{a}\emptyset \cap \dforalla{c}\bunch{p_1, p_3, p_4, p_5, p_6, p_7, p_9}) \cup \daexists{\bunch{b,c}}\emptyset\\
  304.    \stackrel{Def. [\cdot \cdot], \langle \cdot\cdot\rangle}{=} (\daexists{a}\bunch{p_2, p_8} \cap \bunch{p_1, p_7, p_8}) \cup \emptyset\\
  305.    \stackrel{Def. \langle \cdot\cdot\rangle}{=} (\bunch{p_1} \cap \bunch{p_1, p_7, p_8}) \cup \emptyset\\
  306.    \stackrel{Def. \cap, \cup}{=} \bunch{p_1}\\
  307. $\\
  308. $
  309.    \MC{O}^2\textsubscript{(\aexists{a}\foralla{a}\ffalse \wedge \foralla{c}Y) \wedge \aexists{\bunch{b,c}}X}(\emptyset)\\
  310.    = \MC{O}\textsubscript{(\aexists{a}\foralla{a}\ffalse \wedge \foralla{c}Y) \wedge \aexists{\bunch{b,c}}X}(\bunch{p_1})\\
  311.    \stackrel{Def. \MC{O}_F, \text{Berechnung von Y}}{=} (\daexists{a}\dforalla{a}\emptyset \cap \dforalla{c}\bunch{p_1, p_3, p_4, p_5, p_6, p_7, p_9}) \cup \daexists{\bunch{b,c}}\bunch{p_1}\\
  312.    \stackrel{\text{bereits berechnet}, Def. \langle \cdot\cdot\rangle}{=} \bunch{p_1} \cup \bunch{p_2, p_3}\\
  313.    \stackrel{Def. \cup}{=} \bunch{p_1, p_2, p_3}\\
  314. $\\
  315. $
  316.    \MC{O}^3\textsubscript{(\aexists{a}\foralla{a}\ffalse \wedge \foralla{c}Y) \wedge \aexists{\bunch{b,c}}X}(\emptyset)\\
  317.    = \MC{O}\textsubscript{(\aexists{a}\foralla{a}\ffalse \wedge \foralla{c}Y) \wedge \aexists{\bunch{b,c}}X}(\bunch{p_1, p_2, p_3})\\
  318.    \stackrel{Def. \MC{O}_F, \text{Berechnung von Y}}{=} (\daexists{a}\dforalla{a}\emptyset \cap \dforalla{c}\bunch{p_1, p_3, p_4, p_5, p_6, p_7, p_9}) \cup \daexists{\bunch{b,c}}\bunch{p_1, p_2, p_3}\\
  319.    \stackrel{\text{bereits berechnet}, Def. \langle \cdot\cdot\rangle}{=} \bunch{p_1} \cup \bunch{p_2, p_3, p_4, p_5, p_6}\\
  320.    \stackrel{Def. \cup}{=} \bunch{p_1, p_2, p_3, p_4, p_5, p_6}\\
  321. $\\
  322. $
  323.    \MC{O}^3\textsubscript{(\aexists{a}\foralla{a}\ffalse \wedge \foralla{c}Y) \wedge \aexists{\bunch{b,c}}X}(\emptyset)\\
  324.    = \MC{O}\textsubscript{(\aexists{a}\foralla{a}\ffalse \wedge \foralla{c}Y) \wedge \aexists{\bunch{b,c}}X}(\bunch{p_1, p_2, p_3, p_4, p_5, p_6})\\
  325.    \stackrel{Def. \MC{O}_F, \text{Berechnung von Y}}{=} (\daexists{a}\dforalla{a}\emptyset \cap \dforalla{c}\bunch{p_1, p_3, p_4, p_5, p_6, p_7, p_9}) \cup \daexists{\bunch{b,c}}\bunch{p_1, p_2, p_3, p_4, p_5, p_6}\\
  326.    \stackrel{\text{bereits berechnet}, Def. \langle \cdot\cdot\rangle}{=} \bunch{p_1} \cup \bunch{p_2, p_3, p_4, p_5, p_6}\\
  327.    \stackrel{Def. \cup}{=} \bunch{p_1, p_2, p_3, p_4, p_5, p_6}\\
  328. $\\
  329. Damit ist der größte Fixpunkt von X erreicht, da\\
  330. $
  331.    \MC{O}^2\textsubscript{(\aexists{a}\foralla{a}\ffalse \wedge \foralla{c}Y) \wedge \aexists{\bunch{b,c}}X}(\emptyset) = \MC{O}^3\textsubscript{(\aexists{a}\foralla{a}\ffalse \wedge \foralla{c}Y) \wedge \aexists{\bunch{b,c}}X}(\emptyset) =
  332.    \bunch{p_1, p_2, p_3, p_4, p_5, p_6}
  333. $.
  334.  
  335. \section*{Aufgabe 23: Rekursive Eigenschaften - Formalisierung}
  336. \subsubsection*{a)}
  337. $F_1 = \foralla{abendessen}\ffalse \text{ } \Uw \text{ } (\aexists{abendessen}\ftrue \wedge \aexists{loben}\ftrue)$
  338. \subsubsection*{b)}
  339. $F_2 = \foralla{bellen}Inv(\foralla{beißen}\ffalse)$
  340. \subsubsection*{c)}
  341. $F_3 = \foralla{regen}Safe(\aexists{scheinen}\ftrue)$
  342.  
  343. \section*{Aufgabe 24: Charakteristische Formeln}
  344. \begin{align*}
  345.    F_0 = X_1 \mit &X_0 \HMmax \poss{a}X_7 \wedge \poss{b}X_1 \wedge \necess{c}\falsef \wedge \necess{a}X_7 \wedge \necess{b}X_1 \\
  346.    F_1 = X_1 \mit &X_1 \HMmax \poss{c}X_2 \wedge \poss{c}X_5 \wedge \necessS{\{a,b\}}\falsef \wedge \necess{c}(X_2 \vee X_5) \\
  347.    F_2 = X_2 \mit &X_2 \HMmax \poss{c}X_1 \wedge \poss{c}X_5 \wedge \necessS{\{a,b\}}\falsef \wedge \necess{c}(X_1 \vee X_5) \\
  348.    F_3 = X_3 \mit &X_3 \HMmax \poss{a}X_7 \wedge \poss{b}X_1 \wedge \necess{c}\falsef \wedge \necess{a}X_7 \wedge \necess{b}X_1 \\
  349.    F_4 = X_4 \mit &X_4 \HMmax \poss{c}X_4 \wedge \poss{c}X_5 \wedge \necessS{\{a,b\}}\falsef \wedge \necess{c}(X_4 \vee X_5) \\
  350.    F_5 = X_5 \mit &X_5 \HMmax \poss{a}X_6 \wedge \poss{b}X_9 \wedge \necess{c}\falsef \wedge \necess{a}X_6 \wedge \necess{b}X_9 \\
  351.    F_6 = X_6 \mit &X_6 \HMmax \necess{\Act}\falsef \\
  352.    F_7 = X_7 \mit &X_7 \HMmax \necess{\Act}\falsef \\
  353.    F_8 = X_8 \mit &X_8 \HMmax \poss{c}X_4 \wedge \poss{c}X_5 \wedge \poss{c}X_8 \wedge \necessS{\{a,b\}}\falsef \wedge \necess{c}(X_4 \vee X_5 \vee X_8) \\
  354.    F_9 = X_9 \mit &X_9 \HMmax \poss{a}X_6 \wedge \poss{a}X_7 \wedge \poss{b}X_8 \wedge \necess{c}\falsef \wedge \necess{a}(X_6 \vee X_7) \wedge \necess{b}X_8
  355. \end{align*}
  356. \subsection*{b)}
  357. Wir definieren $A^{10} \coloneqq (A,A,A,A,A,A,A,A,A,A) \furalle A \subseteq \Proc$.
  358. Zu lösen ist nun das Gleichungssystem \textbf{F}, deklariert als alle Gleichungen in Teilaufgabe a). Es gilt
  359. \begin{align*}
  360. v_1 \coloneqq \O{\textbf{F}}(\Proc^{10}) &= \left(\O{\ensuremath{F_0}}(\Proc^{10}), \dots, \O{\ensuremath{F_9}}(\Proc^{10})\right) \\
  361. &= \begin{bmatrix}
  362.  \possDenot{a}\Proc \cap \possDenot{b}\Proc \cap \necessDenot{c}\emptyset \\
  363.  \possDenot{c}\Proc \cap \possDenot{c}\Proc \cap \necessDenot{a}\emptyset \cap \necessDenot{b}\emptyset \\
  364.  \possDenot{c}\Proc \cap \possDenot{c}\Proc \cap \necessDenot{a}\emptyset \cap \necessDenot{b}\emptyset \\
  365.  \possDenot{a}\Proc \cap \possDenot{b}\Proc \cap \necessDenot{c}\emptyset \\
  366.  \possDenot{c}\Proc \cap \possDenot{c}\Proc \cap \necessDenot{a}\emptyset \cap \necessDenot{b} \emptyset \\
  367.  \possDenot{a}\Proc \cap \possDenot{b}\Proc \cap \necessDenot{c}\emptyset \\
  368.  \necessDenot{\Act}\emptyset \\
  369.  \necessDenot{\Act}\emptyset \\
  370.  \possDenot{c}\Proc \cap \possDenot{c}\Proc \cap \possDenot{c}\Proc \cap \necessDenot{a}\emptyset \cap \necessDenot{b} \emptyset \\
  371.  \possDenot{a}\Proc \cap \possDenot{a}\Proc \cap \possDenot{b}\Proc \cap \necessDenot{c}\emptyset
  372.  \end{bmatrix} = \begin{bmatrix}
  373.  \{0,3,5,9\} \\
  374.  \{1,2,4,8\} \\
  375.  \{1,2,4,8\} \\
  376.  \{0,3,5,9\} \\
  377.  \{1,2,4,8\} \\
  378.  \{0,3,5,9\} \\
  379.  \{6,7\} \\
  380.  \{6,7\} \\
  381.  \{1,2,4,8\} \\
  382.  \{0,3,5,9\}
  383. \end{bmatrix} \\
  384. \end{align*}
  385. \begin{align*}
  386. v_2 &\coloneqq \O{\textbf{F}}(v_1) = \left(\O{\ensuremath{F_0}}(v_1), \dots, \O{\ensuremath{F_9}}(v_1)\right) \\
  387. &= \begin{bmatrix}
  388.  \possDenot{a}\{6,7\} \cap \possDenot{b}\{1,2,4,8\} \cap \necessDenot{c}\emptyset \cap \necessDenot{a}\{6,7\} \cap \necessDenot{b}\{1,2,4,8\} \\
  389.  \possDenot{c}\{1,2,4,8\} \cap \possDenot{c}\{0,3,5,9\} \cap \necessDenot{a}\emptyset \cap \necessDenot{b}\emptyset \cap \necessDenot{c}\{0,1,2,3,4,5,8,9\}\\
  390.  \possDenot{c}\{1,2,4,8\} \cap \possDenot{c}\{0,3,5,9\} \cap \necessDenot{a}\emptyset \cap \necessDenot{b}\emptyset \cap \necessDenot{c}\{0,1,2,3,4,5,8,9\}\\
  391.  \possDenot{a}\{6,7\} \cap \possDenot{b}\{1,2,4,8\} \cap \necessDenot{c}\emptyset \cap \necessDenot{a}\{6,7\} \cap \necessDenot{b}\{1,2,4,8\} \\
  392.  \possDenot{c}\{1,2,4,8\} \cap \possDenot{c}\{0,3,5,9\} \cap \necessDenot{a}\emptyset \cap \necessDenot{b} \emptyset \cap \necessDenot{c}\{0,1,2,3,4,5,8,9\} \\
  393.  \possDenot{a}\{6,7\} \cap \possDenot{b}\{0,3,5,9\} \cap \necessDenot{c}\emptyset \cap \necessDenot{a}\{6,7\} \cap \necessDenot{b}\{0,3,5,9\}\\
  394.  \necessDenot{\Act}\emptyset \\
  395.  \necessDenot{\Act}\emptyset \\
  396.  \possDenot{c}\{1,2,4,8\} \cap \possDenot{c}\{0,3,5,9\} \cap \possDenot{c}\{1,2,4,8\} \cap \necessDenot{a}\emptyset \cap \necessDenot{b} \emptyset \necessDenot{c}\{0,1,2,3,4,5,8,9\} \\
  397.  \possDenot{a}\{6,7\} \cap \possDenot{a}\{6,7\} \cap \possDenot{b}\{1,2,4,8\} \cap \necessDenot{c}\emptyset \cap \necessDenot{a}\{6,7\} \cap \necessDenot{b}\{1,2,4,8\}
  398.  \end{bmatrix}
  399. \end{align*}
  400.  
  401. \section*{Aufgabe 25: min max mix}
  402.  
  403. \end{document}
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!