From c991cdf90349dc0b32a73e6165a3d1f9bd0c7dbe Mon Sep 17 00:00:00 2001 From: sp Date: Fri, 14 Jun 2024 12:02:46 +0200 Subject: [PATCH] added temporal logic chapter --- decidability/0001.tex | 1 + decidability/0002.tex | 1 + decidability/0003.tex | 1 + decidability/0004.tex | 1 + decidability/decidability.tex | 14 ++++ main.tex | 8 +++ temporal_logic/0001.tex | 6 ++ temporal_logic/0001_sol.tex | 6 ++ temporal_logic/0002.tex | 24 +++++++ temporal_logic/0002_sol.tex | 21 ++++++ temporal_logic/0003.tex | 26 ++++++++ temporal_logic/0003_sol.tex | 27 ++++++++ temporal_logic/0004.tex | 27 ++++++++ temporal_logic/0004_sol.tex | 25 ++++++++ temporal_logic/0005.tex | 8 +++ temporal_logic/0005_sol.tex | 11 ++++ temporal_logic/0006.tex | 7 ++ temporal_logic/0006_sol.tex | 12 ++++ temporal_logic/0007.tex | 12 ++++ temporal_logic/0007_sol.tex | 5 ++ temporal_logic/0008.tex | 12 ++++ temporal_logic/0008_sol.tex | 5 ++ temporal_logic/1000.tex | 6 ++ temporal_logic/1001.tex | 6 ++ temporal_logic/1002.tex | 3 + temporal_logic/1003.tex | 15 +++++ temporal_logic/1004.tex | 18 ++++++ temporal_logic/1005.tex | 24 +++++++ temporal_logic/1006.tex | 25 ++++++++ temporal_logic/1007.tex | 2 + temporal_logic/1008.tex | 2 + .../6_1_ltl_example_lect.tex | 24 +++++++ .../6_1_ltl_example_lect_sol.tex | 13 ++++ .../6_2_ltl_example_lect.tex | 27 ++++++++ .../6_2_ltl_example_lect_sol.tex | 16 +++++ .../practical_questions/6_3_weekdays_lect.tex | 6 ++ .../6_4_ltl_example_self.tex | 24 +++++++ .../6_5_ltl_example_self.tex | 25 ++++++++ .../6_6_ltl_example_self.tex | 26 ++++++++ .../6_6_ltl_example_self_sol.tex | 16 +++++ .../6_7_robot_city_self.tex | 31 +++++++++ .../6_8_traffic_light_lect.tex | 18 ++++++ .../practical_questions/9_1_lect.tex | 6 ++ .../practical_questions/9_1_lect_sol.tex | 6 ++ .../practical_questions/9_2_lect.tex | 8 +++ .../practical_questions/9_2_lect_sol.tex | 11 ++++ .../practical_questions/9_3_lect.tex | 7 ++ .../practical_questions/9_3_lect_sol.tex | 12 ++++ .../practical_questions/9_4_lect.tex | 12 ++++ .../practical_questions/9_4_lect_sol.tex | 5 ++ .../practical_questions/9_5_lect.tex | 12 ++++ .../practical_questions/9_5_lect_sol.tex | 5 ++ temporal_logic/temporal_logic.tex | 64 +++++++++++++++++++ temporal_logic/theory_questions/6_1_self.tex | 6 ++ temporal_logic/theory_questions/6_2_self.tex | 15 +++++ .../6_3_eventually_semantics_lect.tex | 2 + temporal_logic/theory_questions/6_3_self.tex | 3 + .../6_4_until_semantics_lect.tex | 2 + temporal_logic/theory_questions/6_5_self.tex | 6 ++ temporal_logic/theory_questions/6_6_self.tex | 2 + temporal_logic/theory_questions/6_7_self.tex | 2 + util/version.tex | 1 + 62 files changed, 774 insertions(+) create mode 100644 decidability/0001.tex create mode 100644 decidability/0002.tex create mode 100644 decidability/0003.tex create mode 100644 decidability/0004.tex create mode 100644 decidability/decidability.tex create mode 100644 temporal_logic/0001.tex create mode 100644 temporal_logic/0001_sol.tex create mode 100644 temporal_logic/0002.tex create mode 100644 temporal_logic/0002_sol.tex create mode 100644 temporal_logic/0003.tex create mode 100644 temporal_logic/0003_sol.tex create mode 100644 temporal_logic/0004.tex create mode 100644 temporal_logic/0004_sol.tex create mode 100644 temporal_logic/0005.tex create mode 100644 temporal_logic/0005_sol.tex create mode 100644 temporal_logic/0006.tex create mode 100644 temporal_logic/0006_sol.tex create mode 100644 temporal_logic/0007.tex create mode 100644 temporal_logic/0007_sol.tex create mode 100644 temporal_logic/0008.tex create mode 100644 temporal_logic/0008_sol.tex create mode 100644 temporal_logic/1000.tex create mode 100644 temporal_logic/1001.tex create mode 100644 temporal_logic/1002.tex create mode 100644 temporal_logic/1003.tex create mode 100644 temporal_logic/1004.tex create mode 100644 temporal_logic/1005.tex create mode 100644 temporal_logic/1006.tex create mode 100644 temporal_logic/1007.tex create mode 100644 temporal_logic/1008.tex create mode 100644 temporal_logic/practical_questions/6_1_ltl_example_lect.tex create mode 100644 temporal_logic/practical_questions/6_1_ltl_example_lect_sol.tex create mode 100644 temporal_logic/practical_questions/6_2_ltl_example_lect.tex create mode 100644 temporal_logic/practical_questions/6_2_ltl_example_lect_sol.tex create mode 100644 temporal_logic/practical_questions/6_3_weekdays_lect.tex create mode 100644 temporal_logic/practical_questions/6_4_ltl_example_self.tex create mode 100644 temporal_logic/practical_questions/6_5_ltl_example_self.tex create mode 100644 temporal_logic/practical_questions/6_6_ltl_example_self.tex create mode 100644 temporal_logic/practical_questions/6_6_ltl_example_self_sol.tex create mode 100644 temporal_logic/practical_questions/6_7_robot_city_self.tex create mode 100644 temporal_logic/practical_questions/6_8_traffic_light_lect.tex create mode 100644 temporal_logic/practical_questions/9_1_lect.tex create mode 100644 temporal_logic/practical_questions/9_1_lect_sol.tex create mode 100644 temporal_logic/practical_questions/9_2_lect.tex create mode 100644 temporal_logic/practical_questions/9_2_lect_sol.tex create mode 100644 temporal_logic/practical_questions/9_3_lect.tex create mode 100644 temporal_logic/practical_questions/9_3_lect_sol.tex create mode 100644 temporal_logic/practical_questions/9_4_lect.tex create mode 100644 temporal_logic/practical_questions/9_4_lect_sol.tex create mode 100644 temporal_logic/practical_questions/9_5_lect.tex create mode 100644 temporal_logic/practical_questions/9_5_lect_sol.tex create mode 100644 temporal_logic/temporal_logic.tex create mode 100644 temporal_logic/theory_questions/6_1_self.tex create mode 100644 temporal_logic/theory_questions/6_2_self.tex create mode 100644 temporal_logic/theory_questions/6_3_eventually_semantics_lect.tex create mode 100644 temporal_logic/theory_questions/6_3_self.tex create mode 100644 temporal_logic/theory_questions/6_4_until_semantics_lect.tex create mode 100644 temporal_logic/theory_questions/6_5_self.tex create mode 100644 temporal_logic/theory_questions/6_6_self.tex create mode 100644 temporal_logic/theory_questions/6_7_self.tex diff --git a/decidability/0001.tex b/decidability/0001.tex new file mode 100644 index 0000000..90061a6 --- /dev/null +++ b/decidability/0001.tex @@ -0,0 +1 @@ +\item TODO diff --git a/decidability/0002.tex b/decidability/0002.tex new file mode 100644 index 0000000..90061a6 --- /dev/null +++ b/decidability/0002.tex @@ -0,0 +1 @@ +\item TODO diff --git a/decidability/0003.tex b/decidability/0003.tex new file mode 100644 index 0000000..90061a6 --- /dev/null +++ b/decidability/0003.tex @@ -0,0 +1 @@ +\item TODO diff --git a/decidability/0004.tex b/decidability/0004.tex new file mode 100644 index 0000000..90061a6 --- /dev/null +++ b/decidability/0004.tex @@ -0,0 +1 @@ +\item TODO diff --git a/decidability/decidability.tex b/decidability/decidability.tex new file mode 100644 index 0000000..34c667d --- /dev/null +++ b/decidability/decidability.tex @@ -0,0 +1,14 @@ +\begin{questionSection}{Decidability} +\question{decidability/0001.tex} + {no_solution} + {3cm} +\question{decidability/0002.tex} + {no_solution} + {3cm} +\question{decidability/0003.tex} + {no_solution} + {3cm} +\question{decidability/0004.tex} + {no_solution} + {3cm} +\end{questionSection} diff --git a/main.tex b/main.tex index bb219ff..be7100a 100644 --- a/main.tex +++ b/main.tex @@ -5,6 +5,7 @@ \input{util/packages} \input{util/math_macros} +\input{util/ltl_macros} \input{util/styling_macros} \input{util/constants} \input{util/chapter} @@ -127,6 +128,13 @@ \pagebreak \fi +\ifchapterdecidability + \setsectionnum{10} + \section{Decidability} + \input{decidability/decidability.tex} + \pagebreak +\fi + \ifchaptertemporal \setsectionnum{10} \section{Temporal Logic} diff --git a/temporal_logic/0001.tex b/temporal_logic/0001.tex new file mode 100644 index 0000000..a2e32c5 --- /dev/null +++ b/temporal_logic/0001.tex @@ -0,0 +1,6 @@ +\item \lect +Translate the following sentences in computation tree logic $CTL^\star$. +\begin{itemize} + \item In every execution the system gives a grant infinitely often. + \item There exists an execution in which the system sends a request finitely often. +\end{itemize} \ No newline at end of file diff --git a/temporal_logic/0001_sol.tex b/temporal_logic/0001_sol.tex new file mode 100644 index 0000000..4ce8a2b --- /dev/null +++ b/temporal_logic/0001_sol.tex @@ -0,0 +1,6 @@ +\begin{itemize} + \item The Boolean variable $g$ represents ``The system gives a grant.''\newline + $\varphi_1 \coloneqq AGF g$ + \item The Boolean variable $r$ represents ``The system sends a request.'' \newline + $\varphi_2 \coloneqq EFG \neg r$ +\end{itemize} diff --git a/temporal_logic/0002.tex b/temporal_logic/0002.tex new file mode 100644 index 0000000..86782e6 --- /dev/null +++ b/temporal_logic/0002.tex @@ -0,0 +1,24 @@ +\item \lect +Given the following execution word $w$ of a Kripke structure. Evaluate the +formula $\varphi$ on $w$. Evaluate each sub-formula for any execution step using the +provided table. +\begin{itemize} + \item $w = \{\}, \{a\}, \{a\}, \{b\}, \{\}, \{a\}, \{a, b\}^\omega$ + \item $\varphi = \nex a \lor a \unt b$ +\end{itemize} + + \begin{ltltabular}{7} + \ltlSteps{6}{1} + \ltlTrace{a}{0|1|1|0|0|1 |1} + \ltlTrace{b}{0|0|0|1|0|0 |1} + \hline + \hline + \ltlFormula{$\nex a$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$a \unt b$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$\nex a \lor a \unt b$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \end{ltltabular} + + \ No newline at end of file diff --git a/temporal_logic/0002_sol.tex b/temporal_logic/0002_sol.tex new file mode 100644 index 0000000..22d4cff --- /dev/null +++ b/temporal_logic/0002_sol.tex @@ -0,0 +1,21 @@ +\item \lect +Given the following execution word $w$ of a Kripke structure. Evaluate the +formula $\varphi$ on $w$. Evaluate each sub-formula for any execution step using the +provided table. +\begin{itemize} + \item $w = \{\}, \{a\}, \{a\}, \{b\}, \{\}, \{a\}, \{a, b\}^\omega$ + \item $\varphi = \nex a \lor a \unt b$ +\end{itemize} +\begin{ltltabular}{7} + \ltlSteps{6}{1} + \ltlTrace{a}{0|1|1|0|0|1 |1} + \ltlTrace{b}{0|0|0|1|0|0 |1} + \hline + \hline + \ltlFormula{$\nex a$} + {1|1|0|0|1 |1 | 1} + \ltlFormula{$a \unt b$} + {0|1|1|1|0 |1 | 1} + \ltlFormula{$\nex a \lor a \unt b$} + {1|1|1|1|1 |1 | 1} + \end{ltltabular} diff --git a/temporal_logic/0003.tex b/temporal_logic/0003.tex new file mode 100644 index 0000000..f618d93 --- /dev/null +++ b/temporal_logic/0003.tex @@ -0,0 +1,26 @@ +\item \lect +Given the following execution word $w$ of a Kripke structure. Evaluate the +formula $\varphi$ on $w$. Evaluate each sub-formula for any execution step using the +provided table. +\begin{itemize} + \item $w = \{\}, \{a\}, \{ \}, \{a,b,c\}, \{a\}, \{a,b\}, ( \{a\} , \{a,c\}, \{a,c\})^\omega$ + \item $\varphi = \glob a \imp (\event b \lor c )$ +\end{itemize} + + \begin{ltltabular}{9} + \ltlSteps{6}{3} + \ltlTrace{a}{0|1|0|1|1|1 |1|1|1} + \ltlTrace{b}{0|0|0|1|0|1 |0|0|0} + \ltlTrace{c}{0|0|0|1|0|0 |0|1|1} + \hline + \hline + \ltlFormula{$\glob a$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$\event b$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$\event b \vee c$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$\glob a \imp (\event b \lor c)$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \end{ltltabular} + \ No newline at end of file diff --git a/temporal_logic/0003_sol.tex b/temporal_logic/0003_sol.tex new file mode 100644 index 0000000..82e8944 --- /dev/null +++ b/temporal_logic/0003_sol.tex @@ -0,0 +1,27 @@ + +\item \lect +Given the following execution word $w$ of a Kripke structure. Evaluate the +formula $\varphi$ on $w$. Evaluate each sub-formula for any execution step using the +provided table. +\begin{itemize} + \item $w = \{\}, \{a\}, \{ \}, \{a,b,c\}, \{a\}, \{a,b\}, ( \{a\} , \{a,c\}, \{a,c\})^\omega$ + \item $\varphi = \glob a \imp (\event b \lor c )$ +\end{itemize} + + +\begin{ltltabular}{9} + \ltlSteps{6}{3} + \ltlTrace{a}{0|1|0|1|1|1 |1|1|1} + \ltlTrace{b}{0|0|0|1|0|1 |0|0|0} + \ltlTrace{c}{0|0|0|1|0|0 |0|1|1} + \hline + \hline + \ltlFormula{$\glob a$} + {0|1|0|1|1|1 |1|1|1} + \ltlFormula{$\event b$} + {0|1|0|1|1|1 |0|0|0} + \ltlFormula{$\event b \vee c$} + {0|1|0|1|1|1 |0|1|1} + \ltlFormula{$\glob a \imp (\event b \lor c)$} + {0|1|0|1|1|1 |0|1|1} + \end{ltltabular} diff --git a/temporal_logic/0004.tex b/temporal_logic/0004.tex new file mode 100644 index 0000000..e602daa --- /dev/null +++ b/temporal_logic/0004.tex @@ -0,0 +1,27 @@ +\item \lect +Given the following execution word $w$ of a Kripke structure. Evaluate the +formula $\varphi$ on $w$. Evaluate each sub-formula for any execution step using the +provided table. + +\begin{itemize} + \item $w = \{\}, \{a\}, \{ \}, \{a,b,c\}, \{a\}, \{a,b\}, ( \{a\} , \{a,c\}, \{a,c\})^\omega$ + \item $\varphi = \glob \event a \imp (\event \glob \neg b \wedge c )$ +\end{itemize} + + \begin{ltltabular}{9} + \ltlSteps{6}{3} + \ltlTrace{a}{0|1|0|1|1|1 |1|1|1} + \ltlTrace{b}{0|0|0|1|0|1 |0|0|0} + \ltlTrace{c}{0|0|0|1|0|0 |0|1|1} + \hline + \hline + \ltlFormula{$\glob \event a$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$\event \glob \neg b$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$\event \glob \neg b \wedge c$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$\glob \event a \imp (\event \glob \neg b \wedge c )$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \end{ltltabular} + \newline \ No newline at end of file diff --git a/temporal_logic/0004_sol.tex b/temporal_logic/0004_sol.tex new file mode 100644 index 0000000..8c681ae --- /dev/null +++ b/temporal_logic/0004_sol.tex @@ -0,0 +1,25 @@ +\item \lect +Given the following execution word $w$ of a Kripke structure. Evaluate the +formula $\varphi$ on $w$. Evaluate each sub-formula for any execution step using the +provided table. + +\begin{itemize} + \item $w = \{\}, \{a\}, \{ \}, \{a,b,c\}, \{a\}, \{a,b\}, ( \{a\} , \{a,c\}, \{a,c\})^\omega$ + \item $\varphi = \glob \event a \imp (\event \glob \neg b \wedge c )$ +\end{itemize} +\begin{ltltabular}{9} + \ltlSteps{6}{3} + \ltlTrace{a}{0|1|0|1|1|1 |1|1|1} + \ltlTrace{b}{0|0|0|1|0|1 |0|0|0} + \ltlTrace{c}{0|0|0|1|0|0 |0|1|1} + \hline + \hline + \ltlFormula{$\glob \event a$} + {1|1|1|1|1|1 |1|1|1} + \ltlFormula{$\event \glob \neg b$} + {1|1|1|1|1|1 |1|1|1} + \ltlFormula{$\event \glob \neg b \wedge c$} + {0|0|0|1|0|0 |0|1|1} + \ltlFormula{$\glob \event a \imp (\event \glob \neg b \wedge c )$} + {0|0|0|1|0|0 |0|1|1} + \end{ltltabular} diff --git a/temporal_logic/0005.tex b/temporal_logic/0005.tex new file mode 100644 index 0000000..808d3ab --- /dev/null +++ b/temporal_logic/0005.tex @@ -0,0 +1,8 @@ +\item \lect +Translate the following sentences in computation tree logic $CTL^\star$. +\begin{itemize} + \item For any execution, it always holds that whenever the robot +visits region A, it visits region C within the next two steps. + \item There exists an execution such that the robot visits +region C within the next two steps after visiting region A. +\end{itemize} \ No newline at end of file diff --git a/temporal_logic/0005_sol.tex b/temporal_logic/0005_sol.tex new file mode 100644 index 0000000..49a74e0 --- /dev/null +++ b/temporal_logic/0005_sol.tex @@ -0,0 +1,11 @@ +We use the following Boolean variables: +\begin{itemize} + \item $a$ represents ``The robot visits region A'' + \item $b$ represents ``The robot visits region B'' + \item $c$ represents ``The robot visits region C'' +\end{itemize} + +\begin{itemize} + \item $\varphi_1 \coloneqq AG (a \rightarrow Xc \vee XXc)$ + \item $\varphi_2 \coloneqq EG (a \rightarrow Xc \vee XXc)$ +\end{itemize} \ No newline at end of file diff --git a/temporal_logic/0006.tex b/temporal_logic/0006.tex new file mode 100644 index 0000000..722c3d3 --- /dev/null +++ b/temporal_logic/0006.tex @@ -0,0 +1,7 @@ +\item \lect +Translate the following sentences in computation tree logic $CTL^\star$. +\begin{itemize} + \item The robot can visit region A infinitely often and region C infinitely often + \item Always, the robot visits region A infinitely often and region C infinitely often. + \item If the robot visits region A infinitely often, it should also visit region C finitely often. +\end{itemize} \ No newline at end of file diff --git a/temporal_logic/0006_sol.tex b/temporal_logic/0006_sol.tex new file mode 100644 index 0000000..7a11c3b --- /dev/null +++ b/temporal_logic/0006_sol.tex @@ -0,0 +1,12 @@ +We use the following Boolean variables: +\begin{itemize} + \item $a$ represents ``The robot visits region A'' + \item $b$ represents ``The robot visits region B'' + \item $c$ represents ``The robot visits region C'' +\end{itemize} + +\begin{itemize} + \item $\varphi_1 \coloneqq E(GF a \wedge GF c)$ + \item $\varphi_2 \coloneqq A (GF a \wedge FG \neg c)$ + \item $\varphi_3 \coloneqq A (GF a \rightarrow GF c)$ +\end{itemize} \ No newline at end of file diff --git a/temporal_logic/0007.tex b/temporal_logic/0007.tex new file mode 100644 index 0000000..b44ac96 --- /dev/null +++ b/temporal_logic/0007.tex @@ -0,0 +1,12 @@ +\item \lect +Given the following Kripke structure $\mathcal{K}$. Does the initial state $s_0$ of $\mathcal{K}$ satisfy the following formulas? +\begin{itemize} + \item $\varphi_1 \coloneqq EXX(a\wedge b)$ + \item $\varphi_2 \coloneqq EXAX (a \wedge b)$ +\end{itemize} +\begin{figure}[h!] + \centering + \includegraphics[width=0.63\textwidth]{figures/computation_tree.png} + \caption{Left: Kripke structure of Example 7, Right: Corresponding computation tree} + \label{fig3} +\end{figure} \ No newline at end of file diff --git a/temporal_logic/0007_sol.tex b/temporal_logic/0007_sol.tex new file mode 100644 index 0000000..ca13f1e --- /dev/null +++ b/temporal_logic/0007_sol.tex @@ -0,0 +1,5 @@ +\begin{itemize} + \item $s_0 \vDash EXX(a\wedge b)$ + \item $s_0 \nvDash EXAX (a \wedge b)$ +\end{itemize} + diff --git a/temporal_logic/0008.tex b/temporal_logic/0008.tex new file mode 100644 index 0000000..94ad4f2 --- /dev/null +++ b/temporal_logic/0008.tex @@ -0,0 +1,12 @@ +\item \lect +Given the following Kripke structure $\mathcal{K}$. Does the initial state $s_0$ of $\mathcal{K}$ satisfy the following formulas? +\begin{itemize} + \item $\varphi_1 \coloneqq EXp$ + \item $\varphi_2 \coloneqq EG\neg p$ +\end{itemize} +\begin{figure}[h!] + \centering + \includegraphics[width=0.23\textwidth]{figures/kripke5.png} + \caption{Kripke structure of Example 8} + \label{fig3} +\end{figure} \ No newline at end of file diff --git a/temporal_logic/0008_sol.tex b/temporal_logic/0008_sol.tex new file mode 100644 index 0000000..a52013e --- /dev/null +++ b/temporal_logic/0008_sol.tex @@ -0,0 +1,5 @@ +\begin{itemize} + \item $s_0 \vDash EXp$ + \item $s_0 \vDash EG\neg p$ +\end{itemize} + diff --git a/temporal_logic/1000.tex b/temporal_logic/1000.tex new file mode 100644 index 0000000..f501516 --- /dev/null +++ b/temporal_logic/1000.tex @@ -0,0 +1,6 @@ +\item \self +Give the definition of a \emph{Kripke structure}. +Explain the components of the tuple a Kripke structure consists of. +Give an example of a Kripke structure in the representation of a graph. + + diff --git a/temporal_logic/1001.tex b/temporal_logic/1001.tex new file mode 100644 index 0000000..8e40765 --- /dev/null +++ b/temporal_logic/1001.tex @@ -0,0 +1,6 @@ +\item \self +Give the definition of +\emph{paths} and \emph{words} of Kripke structures. +Give an example in which you draw a graph representing a Kripke structure, +and give one possible infinite path and corresponding word. + diff --git a/temporal_logic/1002.tex b/temporal_logic/1002.tex new file mode 100644 index 0000000..be938e8 --- /dev/null +++ b/temporal_logic/1002.tex @@ -0,0 +1,3 @@ +\item \self What does a \emph{computation tree} of a Kripke structure represent? +Give an example in which you draw a graph representing a Kripke structure, +and draw the first 3 levels of the computation tree of this Kripke structure. \ No newline at end of file diff --git a/temporal_logic/1003.tex b/temporal_logic/1003.tex new file mode 100644 index 0000000..5fcc65b --- /dev/null +++ b/temporal_logic/1003.tex @@ -0,0 +1,15 @@ +\item \self + +The temporal operators describe properties that hold along a given infinite path $\rho$ +through the computation tree of a Kripke structure. Given two formulas +$\varphi$ and $\psi$ describing state properties. +\begin{itemize} + \item Which are the properties that $\rho$ needs to satisfy such that + $\rho \vDash G\varphi$? + \item Which are the properties that $\rho$ needs to satisfy such that + $\rho \vDash F\varphi$? + \item Which are the properties that $\rho$ needs to satisfy such that + $\rho \vDash X\varphi$? + \item Which are the properties that $\rho$ needs to satisfy such that + $\rho \vDash \varphi U \psi$? +\end{itemize} diff --git a/temporal_logic/1004.tex b/temporal_logic/1004.tex new file mode 100644 index 0000000..6ebc0f1 --- /dev/null +++ b/temporal_logic/1004.tex @@ -0,0 +1,18 @@ +\item \self + Consider an ordinary traffic junction with incoming lanes from the north, south, east and west. We want to formulate relevant constraints that a traffic light system has to fulfill. + + Give a set of propositional variables that model whether the north and south \emph{or} the east and the west get the + \begin{itemize} + \itemsep0em + \item green, + \item yellow or + \item red + \end{itemize} + light, respectively. \\ + + Formulate the following sentences using \emph{$CTL^\star$}: + \begin{enumerate}[label=(\alph*)] + \item The north/south lanes will never get the green light at same time as the east/west lanes. + \item Whenever the north/south lane receive the green light it will stay green until it changes to yellow. + \item When the east/west lane has the red light, it will eventually get the yellow and red light until the light switches to green. + \end{enumerate} diff --git a/temporal_logic/1005.tex b/temporal_logic/1005.tex new file mode 100644 index 0000000..e2d8bb3 --- /dev/null +++ b/temporal_logic/1005.tex @@ -0,0 +1,24 @@ +\item \self Given the following execution word $w$ of a Kripke structure. Evaluate the +formula $\varphi$ on $w$. Evaluate each sub-formula for any execution step using the +provided table. + +\begin{itemize} + \item $w = \{\}, \{a\}, \{\}, \{a,b\}, \{a \}, \{a,b\}, (\{a\}, \{a, b\}, \{a \})^\omega$ + \item $\varphi = \event \glob a \imp \event \glob b$ +\end{itemize} + + + \begin{ltltabular}{9} + \ltlSteps{6}{3} + \ltlTrace{a}{0|1|0|1|1|1 |1|1|1} + \ltlTrace{b}{0|0|0|1|0|1 |0|1|0} + \hline + \hline + \ltlFormula{$\event \glob a$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$\event \glob b$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$\event \glob a \imp \event \glob b$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \end{ltltabular} + \newline \ No newline at end of file diff --git a/temporal_logic/1006.tex b/temporal_logic/1006.tex new file mode 100644 index 0000000..450847c --- /dev/null +++ b/temporal_logic/1006.tex @@ -0,0 +1,25 @@ +\item \self +Given the following execution word $w$ of a Kripke structure. Evaluate the +formula $\varphi$ on $w$. Evaluate each sub-formula for any execution step using the +provided table. + +\begin{itemize} + \item $w = \{a\},\{a\},\{a\},\{b,c\},\{a\},\{a,b\}(\{a\},\{c\})^\omega$ + \item $\varphi = a \unt c \lor \event b $ +\end{itemize} + + \begin{ltltabular}{8} + \ltlSteps{6}{2} + \ltlTrace{a}{1|1|1|0|1|1 |1|0} + \ltlTrace{b}{0|0|0|1|0|1 |0|0} + \ltlTrace{c}{0|0|0|1|0|0 |0|1} + \hline + \hline + \ltlFormula{$a \unt c$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$\event b$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$a \unt c \lor \event b$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \end{ltltabular} + \newline \ No newline at end of file diff --git a/temporal_logic/1007.tex b/temporal_logic/1007.tex new file mode 100644 index 0000000..1dc7e4c --- /dev/null +++ b/temporal_logic/1007.tex @@ -0,0 +1,2 @@ +\item \self Give the definition of the syntax of the computation tree logic $CTL^\star$. +In particular, give the definition of state formulas and path formulas. \ No newline at end of file diff --git a/temporal_logic/1008.tex b/temporal_logic/1008.tex new file mode 100644 index 0000000..a788be1 --- /dev/null +++ b/temporal_logic/1008.tex @@ -0,0 +1,2 @@ +\item \self Give an intuitive explanation of the semantics of computation tree logic $CTL^\star$. +Therefore, explain the semantics of the introduced path quantifiers and temporal operators with respect to the computation tree of a Kripke structure. \ No newline at end of file diff --git a/temporal_logic/practical_questions/6_1_ltl_example_lect.tex b/temporal_logic/practical_questions/6_1_ltl_example_lect.tex new file mode 100644 index 0000000..86782e6 --- /dev/null +++ b/temporal_logic/practical_questions/6_1_ltl_example_lect.tex @@ -0,0 +1,24 @@ +\item \lect +Given the following execution word $w$ of a Kripke structure. Evaluate the +formula $\varphi$ on $w$. Evaluate each sub-formula for any execution step using the +provided table. +\begin{itemize} + \item $w = \{\}, \{a\}, \{a\}, \{b\}, \{\}, \{a\}, \{a, b\}^\omega$ + \item $\varphi = \nex a \lor a \unt b$ +\end{itemize} + + \begin{ltltabular}{7} + \ltlSteps{6}{1} + \ltlTrace{a}{0|1|1|0|0|1 |1} + \ltlTrace{b}{0|0|0|1|0|0 |1} + \hline + \hline + \ltlFormula{$\nex a$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$a \unt b$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$\nex a \lor a \unt b$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \end{ltltabular} + + \ No newline at end of file diff --git a/temporal_logic/practical_questions/6_1_ltl_example_lect_sol.tex b/temporal_logic/practical_questions/6_1_ltl_example_lect_sol.tex new file mode 100644 index 0000000..266d410 --- /dev/null +++ b/temporal_logic/practical_questions/6_1_ltl_example_lect_sol.tex @@ -0,0 +1,13 @@ + \begin{ltltabular}{7} + \ltlSteps{6}{1} + \ltlTrace{a}{0|1|1|0|0|1 |1} + \ltlTrace{b}{0|0|0|1|0|0 |1} + \hline + \hline + \ltlFormula{$\nex a$} + {1|1|0|0|1 |1 | 1} + \ltlFormula{$a \unt b$} + {0|1|1|1|0 |1 | 1} + \ltlFormula{$\nex a \lor a \unt b$} + {1|1|1|1|1 |1 | 1} + \end{ltltabular} diff --git a/temporal_logic/practical_questions/6_2_ltl_example_lect.tex b/temporal_logic/practical_questions/6_2_ltl_example_lect.tex new file mode 100644 index 0000000..e602daa --- /dev/null +++ b/temporal_logic/practical_questions/6_2_ltl_example_lect.tex @@ -0,0 +1,27 @@ +\item \lect +Given the following execution word $w$ of a Kripke structure. Evaluate the +formula $\varphi$ on $w$. Evaluate each sub-formula for any execution step using the +provided table. + +\begin{itemize} + \item $w = \{\}, \{a\}, \{ \}, \{a,b,c\}, \{a\}, \{a,b\}, ( \{a\} , \{a,c\}, \{a,c\})^\omega$ + \item $\varphi = \glob \event a \imp (\event \glob \neg b \wedge c )$ +\end{itemize} + + \begin{ltltabular}{9} + \ltlSteps{6}{3} + \ltlTrace{a}{0|1|0|1|1|1 |1|1|1} + \ltlTrace{b}{0|0|0|1|0|1 |0|0|0} + \ltlTrace{c}{0|0|0|1|0|0 |0|1|1} + \hline + \hline + \ltlFormula{$\glob \event a$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$\event \glob \neg b$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$\event \glob \neg b \wedge c$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$\glob \event a \imp (\event \glob \neg b \wedge c )$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \end{ltltabular} + \newline \ No newline at end of file diff --git a/temporal_logic/practical_questions/6_2_ltl_example_lect_sol.tex b/temporal_logic/practical_questions/6_2_ltl_example_lect_sol.tex new file mode 100644 index 0000000..ac805a6 --- /dev/null +++ b/temporal_logic/practical_questions/6_2_ltl_example_lect_sol.tex @@ -0,0 +1,16 @@ + \begin{ltltabular}{9} + \ltlSteps{6}{3} + \ltlTrace{a}{0|1|0|1|1|1 |1|1|1} + \ltlTrace{b}{0|0|0|1|0|1 |0|0|0} + \ltlTrace{c}{0|0|0|1|0|0 |0|1|1} + \hline + \hline + \ltlFormula{$\glob \event a$} + {1|1|1|1|1|1 |1|1|1} + \ltlFormula{$\event \glob \neg b$} + {1|1|1|1|1|1 |1|1|1} + \ltlFormula{$\event \glob \neg b \wedge c$} + {0|0|0|1|0|0 |0|1|1} + \ltlFormula{$\glob \event a \imp (\event \glob \neg b \wedge c )$} + {0|0|0|1|0|0 |0|1|1} + \end{ltltabular} \ No newline at end of file diff --git a/temporal_logic/practical_questions/6_3_weekdays_lect.tex b/temporal_logic/practical_questions/6_3_weekdays_lect.tex new file mode 100644 index 0000000..b8f5439 --- /dev/null +++ b/temporal_logic/practical_questions/6_3_weekdays_lect.tex @@ -0,0 +1,6 @@ +\item \lect + \begin{itemize} + \item draw weekdays kripke structure + \item There will always eventually be weekend. + \item If it is Tuesday, the next day will be Wednesday. + \end{itemize} diff --git a/temporal_logic/practical_questions/6_4_ltl_example_self.tex b/temporal_logic/practical_questions/6_4_ltl_example_self.tex new file mode 100644 index 0000000..e2d8bb3 --- /dev/null +++ b/temporal_logic/practical_questions/6_4_ltl_example_self.tex @@ -0,0 +1,24 @@ +\item \self Given the following execution word $w$ of a Kripke structure. Evaluate the +formula $\varphi$ on $w$. Evaluate each sub-formula for any execution step using the +provided table. + +\begin{itemize} + \item $w = \{\}, \{a\}, \{\}, \{a,b\}, \{a \}, \{a,b\}, (\{a\}, \{a, b\}, \{a \})^\omega$ + \item $\varphi = \event \glob a \imp \event \glob b$ +\end{itemize} + + + \begin{ltltabular}{9} + \ltlSteps{6}{3} + \ltlTrace{a}{0|1|0|1|1|1 |1|1|1} + \ltlTrace{b}{0|0|0|1|0|1 |0|1|0} + \hline + \hline + \ltlFormula{$\event \glob a$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$\event \glob b$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$\event \glob a \imp \event \glob b$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \end{ltltabular} + \newline \ No newline at end of file diff --git a/temporal_logic/practical_questions/6_5_ltl_example_self.tex b/temporal_logic/practical_questions/6_5_ltl_example_self.tex new file mode 100644 index 0000000..450847c --- /dev/null +++ b/temporal_logic/practical_questions/6_5_ltl_example_self.tex @@ -0,0 +1,25 @@ +\item \self +Given the following execution word $w$ of a Kripke structure. Evaluate the +formula $\varphi$ on $w$. Evaluate each sub-formula for any execution step using the +provided table. + +\begin{itemize} + \item $w = \{a\},\{a\},\{a\},\{b,c\},\{a\},\{a,b\}(\{a\},\{c\})^\omega$ + \item $\varphi = a \unt c \lor \event b $ +\end{itemize} + + \begin{ltltabular}{8} + \ltlSteps{6}{2} + \ltlTrace{a}{1|1|1|0|1|1 |1|0} + \ltlTrace{b}{0|0|0|1|0|1 |0|0} + \ltlTrace{c}{0|0|0|1|0|0 |0|1} + \hline + \hline + \ltlFormula{$a \unt c$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$\event b$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$a \unt c \lor \event b$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \end{ltltabular} + \newline \ No newline at end of file diff --git a/temporal_logic/practical_questions/6_6_ltl_example_self.tex b/temporal_logic/practical_questions/6_6_ltl_example_self.tex new file mode 100644 index 0000000..f618d93 --- /dev/null +++ b/temporal_logic/practical_questions/6_6_ltl_example_self.tex @@ -0,0 +1,26 @@ +\item \lect +Given the following execution word $w$ of a Kripke structure. Evaluate the +formula $\varphi$ on $w$. Evaluate each sub-formula for any execution step using the +provided table. +\begin{itemize} + \item $w = \{\}, \{a\}, \{ \}, \{a,b,c\}, \{a\}, \{a,b\}, ( \{a\} , \{a,c\}, \{a,c\})^\omega$ + \item $\varphi = \glob a \imp (\event b \lor c )$ +\end{itemize} + + \begin{ltltabular}{9} + \ltlSteps{6}{3} + \ltlTrace{a}{0|1|0|1|1|1 |1|1|1} + \ltlTrace{b}{0|0|0|1|0|1 |0|0|0} + \ltlTrace{c}{0|0|0|1|0|0 |0|1|1} + \hline + \hline + \ltlFormula{$\glob a$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$\event b$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$\event b \vee c$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \ltlFormula{$\glob a \imp (\event b \lor c)$} + {\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}|\ws{1cm}} + \end{ltltabular} + \ No newline at end of file diff --git a/temporal_logic/practical_questions/6_6_ltl_example_self_sol.tex b/temporal_logic/practical_questions/6_6_ltl_example_self_sol.tex new file mode 100644 index 0000000..acfe3de --- /dev/null +++ b/temporal_logic/practical_questions/6_6_ltl_example_self_sol.tex @@ -0,0 +1,16 @@ + \begin{ltltabular}{9} + \ltlSteps{6}{3} + \ltlTrace{a}{0|1|0|1|1|1 |1|1|1} + \ltlTrace{b}{0|0|0|1|0|1 |0|0|0} + \ltlTrace{c}{0|0|0|1|0|0 |0|1|1} + \hline + \hline + \ltlFormula{$\glob a$} + {0|1|0|1|1|1 |1|1|1} + \ltlFormula{$\event b$} + {0|1|0|1|1|1 |0|0|0} + \ltlFormula{$\event b \vee c$} + {0|1|0|1|1|1 |0|1|1} + \ltlFormula{$\glob a \imp (\event b \lor c)$} + {0|1|0|1|1|1 |0|1|1} + \end{ltltabular} \ No newline at end of file diff --git a/temporal_logic/practical_questions/6_7_robot_city_self.tex b/temporal_logic/practical_questions/6_7_robot_city_self.tex new file mode 100644 index 0000000..2d03d4c --- /dev/null +++ b/temporal_logic/practical_questions/6_7_robot_city_self.tex @@ -0,0 +1,31 @@ +\item \self + Consider a robot moving in this small transition system. The robot has to fulfill tasks in the state $00$ and $10$. \\ + Let the state labelling be as follows: $(x_1 x_0)$. + + \begin{figure}[h!] + \centering + \begin{conflictgraph} + %\tikzset{every loop/.style={min distance=10mm,in=0,out=60,looseness=10}} + \node[base node] (00) {$00$}; + \node[base node] (01) [right of=00] {$01$}; + \node[base node] (10) [below of=01] {$10$}; + \node[base node] (11) [below of=00] {$11$}; + \path[->] (00) edge [loop above] node {} (); + \path[->] (10) edge [loop right] node {} (); + \path[->] (11) edge [loop below] node {} (); + \path[] + (00) edge [bend left] node {} (01) + (01) edge [bend left] node {} (00) + (01) edge [bend left] node {} (10) + (10) edge [bend left] node {} (01) + (00) edge [] node {} (11) + (10) edge [] node {} (11); + \end{conflictgraph} + \end{figure} + + Formulate the following using \emph{Linear Temporal Logic}: + \begin{enumerate}[(a)] + \item The robot will infinitely often see state $00$ and $10$. + \item The robot will never visit state $11$. + \item After visiting either state $00$ or $10$ the robot will visit state $01$ within the next three time steps. + \end{enumerate} diff --git a/temporal_logic/practical_questions/6_8_traffic_light_lect.tex b/temporal_logic/practical_questions/6_8_traffic_light_lect.tex new file mode 100644 index 0000000..d537e5a --- /dev/null +++ b/temporal_logic/practical_questions/6_8_traffic_light_lect.tex @@ -0,0 +1,18 @@ +\item \self + Consider an ordinary traffic junction with incoming lanes from the north, south, east and west. We want to formulate relevant constraints that a traffic light system has to fulfill. + + Give a set of propositional variables that model whether the north and south \emph{or} the east and the west get the + \begin{itemize} + \itemsep0em + \item green, + \item yellow or + \item red + \end{itemize} + light, respectively. \\ + + Formulate the following sentences using \emph{$CTL^\star$}: + \begin{enumerate}[(a)] + \item The north/south lanes will never get the green light at same time as the east/west lanes. + \item Whenever the north/south lane receive the green light it will stay green until it changes to yellow. + \item When the east/west lane has the red light, it will eventually get the yellow and red light until the light switches to green. + \end{enumerate} \ No newline at end of file diff --git a/temporal_logic/practical_questions/9_1_lect.tex b/temporal_logic/practical_questions/9_1_lect.tex new file mode 100644 index 0000000..a2e32c5 --- /dev/null +++ b/temporal_logic/practical_questions/9_1_lect.tex @@ -0,0 +1,6 @@ +\item \lect +Translate the following sentences in computation tree logic $CTL^\star$. +\begin{itemize} + \item In every execution the system gives a grant infinitely often. + \item There exists an execution in which the system sends a request finitely often. +\end{itemize} \ No newline at end of file diff --git a/temporal_logic/practical_questions/9_1_lect_sol.tex b/temporal_logic/practical_questions/9_1_lect_sol.tex new file mode 100644 index 0000000..1fb5573 --- /dev/null +++ b/temporal_logic/practical_questions/9_1_lect_sol.tex @@ -0,0 +1,6 @@ +\begin{itemize} + \item The Boolean variable $g$ represents ``The system gives a grant.''\newline + $\varphi_1 \coloneqq AGF g$ + \item The Boolean variable $r$ represents ``The system sends a request.'' \newline + $\varphi_2 \coloneqq EGF \neg r$ +\end{itemize} \ No newline at end of file diff --git a/temporal_logic/practical_questions/9_2_lect.tex b/temporal_logic/practical_questions/9_2_lect.tex new file mode 100644 index 0000000..808d3ab --- /dev/null +++ b/temporal_logic/practical_questions/9_2_lect.tex @@ -0,0 +1,8 @@ +\item \lect +Translate the following sentences in computation tree logic $CTL^\star$. +\begin{itemize} + \item For any execution, it always holds that whenever the robot +visits region A, it visits region C within the next two steps. + \item There exists an execution such that the robot visits +region C within the next two steps after visiting region A. +\end{itemize} \ No newline at end of file diff --git a/temporal_logic/practical_questions/9_2_lect_sol.tex b/temporal_logic/practical_questions/9_2_lect_sol.tex new file mode 100644 index 0000000..49a74e0 --- /dev/null +++ b/temporal_logic/practical_questions/9_2_lect_sol.tex @@ -0,0 +1,11 @@ +We use the following Boolean variables: +\begin{itemize} + \item $a$ represents ``The robot visits region A'' + \item $b$ represents ``The robot visits region B'' + \item $c$ represents ``The robot visits region C'' +\end{itemize} + +\begin{itemize} + \item $\varphi_1 \coloneqq AG (a \rightarrow Xc \vee XXc)$ + \item $\varphi_2 \coloneqq EG (a \rightarrow Xc \vee XXc)$ +\end{itemize} \ No newline at end of file diff --git a/temporal_logic/practical_questions/9_3_lect.tex b/temporal_logic/practical_questions/9_3_lect.tex new file mode 100644 index 0000000..722c3d3 --- /dev/null +++ b/temporal_logic/practical_questions/9_3_lect.tex @@ -0,0 +1,7 @@ +\item \lect +Translate the following sentences in computation tree logic $CTL^\star$. +\begin{itemize} + \item The robot can visit region A infinitely often and region C infinitely often + \item Always, the robot visits region A infinitely often and region C infinitely often. + \item If the robot visits region A infinitely often, it should also visit region C finitely often. +\end{itemize} \ No newline at end of file diff --git a/temporal_logic/practical_questions/9_3_lect_sol.tex b/temporal_logic/practical_questions/9_3_lect_sol.tex new file mode 100644 index 0000000..7a11c3b --- /dev/null +++ b/temporal_logic/practical_questions/9_3_lect_sol.tex @@ -0,0 +1,12 @@ +We use the following Boolean variables: +\begin{itemize} + \item $a$ represents ``The robot visits region A'' + \item $b$ represents ``The robot visits region B'' + \item $c$ represents ``The robot visits region C'' +\end{itemize} + +\begin{itemize} + \item $\varphi_1 \coloneqq E(GF a \wedge GF c)$ + \item $\varphi_2 \coloneqq A (GF a \wedge FG \neg c)$ + \item $\varphi_3 \coloneqq A (GF a \rightarrow GF c)$ +\end{itemize} \ No newline at end of file diff --git a/temporal_logic/practical_questions/9_4_lect.tex b/temporal_logic/practical_questions/9_4_lect.tex new file mode 100644 index 0000000..b44ac96 --- /dev/null +++ b/temporal_logic/practical_questions/9_4_lect.tex @@ -0,0 +1,12 @@ +\item \lect +Given the following Kripke structure $\mathcal{K}$. Does the initial state $s_0$ of $\mathcal{K}$ satisfy the following formulas? +\begin{itemize} + \item $\varphi_1 \coloneqq EXX(a\wedge b)$ + \item $\varphi_2 \coloneqq EXAX (a \wedge b)$ +\end{itemize} +\begin{figure}[h!] + \centering + \includegraphics[width=0.63\textwidth]{figures/computation_tree.png} + \caption{Left: Kripke structure of Example 7, Right: Corresponding computation tree} + \label{fig3} +\end{figure} \ No newline at end of file diff --git a/temporal_logic/practical_questions/9_4_lect_sol.tex b/temporal_logic/practical_questions/9_4_lect_sol.tex new file mode 100644 index 0000000..ca13f1e --- /dev/null +++ b/temporal_logic/practical_questions/9_4_lect_sol.tex @@ -0,0 +1,5 @@ +\begin{itemize} + \item $s_0 \vDash EXX(a\wedge b)$ + \item $s_0 \nvDash EXAX (a \wedge b)$ +\end{itemize} + diff --git a/temporal_logic/practical_questions/9_5_lect.tex b/temporal_logic/practical_questions/9_5_lect.tex new file mode 100644 index 0000000..94ad4f2 --- /dev/null +++ b/temporal_logic/practical_questions/9_5_lect.tex @@ -0,0 +1,12 @@ +\item \lect +Given the following Kripke structure $\mathcal{K}$. Does the initial state $s_0$ of $\mathcal{K}$ satisfy the following formulas? +\begin{itemize} + \item $\varphi_1 \coloneqq EXp$ + \item $\varphi_2 \coloneqq EG\neg p$ +\end{itemize} +\begin{figure}[h!] + \centering + \includegraphics[width=0.23\textwidth]{figures/kripke5.png} + \caption{Kripke structure of Example 8} + \label{fig3} +\end{figure} \ No newline at end of file diff --git a/temporal_logic/practical_questions/9_5_lect_sol.tex b/temporal_logic/practical_questions/9_5_lect_sol.tex new file mode 100644 index 0000000..a52013e --- /dev/null +++ b/temporal_logic/practical_questions/9_5_lect_sol.tex @@ -0,0 +1,5 @@ +\begin{itemize} + \item $s_0 \vDash EXp$ + \item $s_0 \vDash EG\neg p$ +\end{itemize} + diff --git a/temporal_logic/temporal_logic.tex b/temporal_logic/temporal_logic.tex new file mode 100644 index 0000000..cf09952 --- /dev/null +++ b/temporal_logic/temporal_logic.tex @@ -0,0 +1,64 @@ +\begin{questionSection}{Temporal Logic} + +\question{temporal_logic/1000.tex} + {no_solution} + {3cm} +\question{temporal_logic/1001.tex} + {no_solution} + {3cm} +\question{temporal_logic/1002.tex} + {no_solution} + {3cm} +\question{temporal_logic/1003.tex} + {no_solution} + {3cm} + +\question{temporal_logic/1007.tex} + {no_solution} + {3cm} + +\question{temporal_logic/1008.tex} + {no_solution} + {3cm} + +\question{temporal_logic/0001.tex} + {temporal_logic/0001_sol.tex} + {3cm} + +\question{temporal_logic/0005.tex} + {temporal_logic/0005_sol.tex} + {3cm} + +\question{temporal_logic/0006.tex} + {temporal_logic/0006_sol.tex} + {3cm} + + +\mcquestion{temporal_logic/0002.tex} + {temporal_logic/0002_sol.tex} + +\mcquestion{temporal_logic/0003.tex} + {temporal_logic/0003_sol.tex} + +\mcquestion{temporal_logic/0004.tex} + {temporal_logic/0004_sol.tex} + +\mcquestion{temporal_logic/1005.tex} + {temporal_logic/1005.tex} + +\mcquestion{temporal_logic/1006.tex} + {temporal_logic/1006.tex} + +\question{temporal_logic/0007.tex} + {temporal_logic/0007_sol.tex} + {3cm} + +\question{temporal_logic/0008.tex} + {temporal_logic/0008_sol.tex} + {3cm} + +\question{temporal_logic/1004.tex} + {no_solution} + {3cm} + +\end{questionSection} diff --git a/temporal_logic/theory_questions/6_1_self.tex b/temporal_logic/theory_questions/6_1_self.tex new file mode 100644 index 0000000..f501516 --- /dev/null +++ b/temporal_logic/theory_questions/6_1_self.tex @@ -0,0 +1,6 @@ +\item \self +Give the definition of a \emph{Kripke structure}. +Explain the components of the tuple a Kripke structure consists of. +Give an example of a Kripke structure in the representation of a graph. + + diff --git a/temporal_logic/theory_questions/6_2_self.tex b/temporal_logic/theory_questions/6_2_self.tex new file mode 100644 index 0000000..5fcc65b --- /dev/null +++ b/temporal_logic/theory_questions/6_2_self.tex @@ -0,0 +1,15 @@ +\item \self + +The temporal operators describe properties that hold along a given infinite path $\rho$ +through the computation tree of a Kripke structure. Given two formulas +$\varphi$ and $\psi$ describing state properties. +\begin{itemize} + \item Which are the properties that $\rho$ needs to satisfy such that + $\rho \vDash G\varphi$? + \item Which are the properties that $\rho$ needs to satisfy such that + $\rho \vDash F\varphi$? + \item Which are the properties that $\rho$ needs to satisfy such that + $\rho \vDash X\varphi$? + \item Which are the properties that $\rho$ needs to satisfy such that + $\rho \vDash \varphi U \psi$? +\end{itemize} diff --git a/temporal_logic/theory_questions/6_3_eventually_semantics_lect.tex b/temporal_logic/theory_questions/6_3_eventually_semantics_lect.tex new file mode 100644 index 0000000..195bbb5 --- /dev/null +++ b/temporal_logic/theory_questions/6_3_eventually_semantics_lect.tex @@ -0,0 +1,2 @@ +\item \lect + Let $\pi$ be a trace over a transition system. Give the definition of the \emph{Eventually} operator from \emph{LTL}, i.e. when does $\pi\models\event\varphi$? diff --git a/temporal_logic/theory_questions/6_3_self.tex b/temporal_logic/theory_questions/6_3_self.tex new file mode 100644 index 0000000..be938e8 --- /dev/null +++ b/temporal_logic/theory_questions/6_3_self.tex @@ -0,0 +1,3 @@ +\item \self What does a \emph{computation tree} of a Kripke structure represent? +Give an example in which you draw a graph representing a Kripke structure, +and draw the first 3 levels of the computation tree of this Kripke structure. \ No newline at end of file diff --git a/temporal_logic/theory_questions/6_4_until_semantics_lect.tex b/temporal_logic/theory_questions/6_4_until_semantics_lect.tex new file mode 100644 index 0000000..931457c --- /dev/null +++ b/temporal_logic/theory_questions/6_4_until_semantics_lect.tex @@ -0,0 +1,2 @@ +\item \lect + Let $\pi$ be a trace over a transition system. Give the definition of the \emph{Until} operator from \emph{LTL}, i.e. when does $\pi\models\varphi_1\unt\varphi_2$? diff --git a/temporal_logic/theory_questions/6_5_self.tex b/temporal_logic/theory_questions/6_5_self.tex new file mode 100644 index 0000000..8e40765 --- /dev/null +++ b/temporal_logic/theory_questions/6_5_self.tex @@ -0,0 +1,6 @@ +\item \self +Give the definition of +\emph{paths} and \emph{words} of Kripke structures. +Give an example in which you draw a graph representing a Kripke structure, +and give one possible infinite path and corresponding word. + diff --git a/temporal_logic/theory_questions/6_6_self.tex b/temporal_logic/theory_questions/6_6_self.tex new file mode 100644 index 0000000..1dc7e4c --- /dev/null +++ b/temporal_logic/theory_questions/6_6_self.tex @@ -0,0 +1,2 @@ +\item \self Give the definition of the syntax of the computation tree logic $CTL^\star$. +In particular, give the definition of state formulas and path formulas. \ No newline at end of file diff --git a/temporal_logic/theory_questions/6_7_self.tex b/temporal_logic/theory_questions/6_7_self.tex new file mode 100644 index 0000000..a788be1 --- /dev/null +++ b/temporal_logic/theory_questions/6_7_self.tex @@ -0,0 +1,2 @@ +\item \self Give an intuitive explanation of the semantics of computation tree logic $CTL^\star$. +Therefore, explain the semantics of the introduced path quantifiers and temporal operators with respect to the computation tree of a Kripke structure. \ No newline at end of file diff --git a/util/version.tex b/util/version.tex index 805bbe5..c6c20e5 100644 --- a/util/version.tex +++ b/util/version.tex @@ -16,6 +16,7 @@ \newif\ifchaptereqchecking \newif\ifchaptersymbenc \newif\ifchaptertemporal +\newif\ifchapterdecidability \newif\ifassignmentsheet