diff options
Diffstat (limited to 'Assignment1')
| -rw-r--r-- | Assignment1/assignment1.tex | 10 | ||||
| -rw-r--r-- | Assignment1/conversion.tex | 6 | ||||
| -rw-r--r-- | Assignment1/semantics.tex | 40 | ||||
| -rw-r--r-- | Assignment1/syntax.tex | 2 |
4 files changed, 55 insertions, 3 deletions
diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex index e859f41..c1e6a0d 100644 --- a/Assignment1/assignment1.tex +++ b/Assignment1/assignment1.tex @@ -62,6 +62,8 @@ \usepackage{algpseudocode} \usepackage{tikz} \usetikzlibrary{automata,positioning} +\tikzset{>=stealth} +\tikzset{state/.append style={minimum size=15pt}} \usepackage{relsize} \usepackage{parskip} \usepackage{cleveref} @@ -111,14 +113,22 @@ \setcounter{section}{5} \setcounter{subsection}{2} +% The extra newlines are needed for correct changebars + \input{intro} + \input{syntax} + \input{semantics} + \input{equivalence} + \input{conversion} + \input{bad-prefix} \input{summary} + \input{exercises} \both diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex index 5b97530..e474f74 100644 --- a/Assignment1/conversion.tex +++ b/Assignment1/conversion.tex @@ -20,7 +20,11 @@ The syntactic algorithm as proposed by Gabbay has its foundation in the followin For this paragraph we will use Gabbay's definitions.} \begin{enumerate} \item Every PLTL formula can be written using no other temporal operators than $\Sop$ and $\Uop$ operators. - \item Every formula $\phi$ containing only the $\Sop$ and $\Uop$ operators can be written as a boolean combination of $\wfff \cup \wffp \cup \wffn$. + \item Every formula $\phi$ containing only the $\Sop$ and $\Uop$ operators can be written as a boolean combination of $\wfff \cup \wffp \cup \wffn$.% + \footnote{% + This is known as the Separation Theorem. + It was originally proven by \citet{Gabbay1980}. + Folklore has it that when Hans Kamp, a philosopher working on temporal logics, heard of the result, he went out and bought Gabbay a cake (\url{https://cstheory.stackexchange.com/a/29452}, retrieved April 19, 2018).} \item The same formula without past modalities $\psi$, a boolean combination of $\wfff \cup \wffn$, is initially equivalent to $\phi$. \end{enumerate} When these facts are considered in sequence, diff --git a/Assignment1/semantics.tex b/Assignment1/semantics.tex index 055d66b..dcc8e6b 100644 --- a/Assignment1/semantics.tex +++ b/Assignment1/semantics.tex @@ -51,6 +51,23 @@ The information about $A_0$ is not lost, so whether $\bigcirc\phi$ holds for $\s \label{fig:PLTL-semantics} \end{figure} +\begin{example}[Satisfaction of PLTL Formulae by Words] + Let $\pi = aabcdcdcd\dots$ be an infinite path over $AP=\{a,b,c,d\}$, of which on every moment only one atomic proposition holds (i.e., at position 0, $a$ holds, at position 2, $b$ holds, etc.). + We have for instance: + + \begin{itemize} + \item For all $i\in\mathbb N$, $\pi \vDash_i b \rightarrow \Xop^{-1}a$. + If $i \ne 2$, $b$ does not hold and the implication is trivially satisfied. + If $i = 2$, we have $\pi \vDash_{i-1} a$ and the formula is satisfied as well. + \item For all $i\ge 2$, $\pi \vDash_i (d \rightarrow \Xop^{-1} c) \Sop b$. + We need to give $0 \le j \le i$ with $\pi \vDash_j b$ and $\pi \vDash_k d \rightarrow \Xop^{-1} c$ for all $j < k \le i$. + Clearly, we can only give $j=2$. + Then for odd positions $k$, the implication $d \rightarrow \Xop^{-1} c$ holds trivially since $d$ does not hold. + For even positions $k$, it holds as well since $c$ holds at odd positions $n > 2$. + \qedhere + \end{itemize} +\end{example} + \erin Given these definitions, it is possible to derive the formal semantics of the $\Fop^{-1}$ and $\Gop^{-1}$ operators as well: \[ @@ -59,6 +76,7 @@ Given these definitions, it is possible to derive the formal semantics of the $\ \sigma &\vDash_i &\Gop^{-1}\phi &\text{iff} &\forall_{0 \leq j \leq i}[\sigma \vDash_j \phi] \end{matrix*} \] + \camil The first follows from the rule for $\Sop$ and the fact that $\sigma \vDash_i \top$ for all $i\in\mathbb N$. The second follows from: @@ -81,5 +99,25 @@ With this result we can also derive the semantics of the dual modalities $\lozen This is done in \cref{ex:dual-modalities}. The semantics over words extend to transition systems similar to the LTL case in Definition 5.7. -The only difference is that $\vDash$ now is a ternary relation, and we use $\vDash$ as shorthand for $\vDash_0$. +The only difference is that $\vDash$ now is a ternary relation, and we use $\pi\vDash\phi$ as a shorthand for $\pi\vDash_0\phi$. + +\begin{figure}[h] + \centering + \begin{tikzpicture}[initial text={},node distance=3cm,->] + \node[state,label=below:{$\{a,b\}$},initial] (s1) {$s_1$}; + \node[state,label=below:{$\{a,b\}$},right of=s1] (s2) {$s_2$}; + \node[state,label=below:{$\{a\}$},right of=s2,initial right] (s3) {$s_3$}; + \draw (s1) edge[bend left] (s2); + \draw (s2) edge[bend left] (s1); + \draw (s2) -- (s3); + \draw (s3) edge[loop above,looseness=8,in=60,out=120] (s3); + \end{tikzpicture} + \caption{Example for semantics of PLTL.} + \label{fig:pltl:example-ts} +\end{figure} + +\begin{example}[Satisfaction of PLTL Formulae by Transition Systems] + Consider again the transition system from Figure 5.3, reproduced as \cref{fig:pltl:example-ts}. + % TODO +\end{example} \cbend diff --git a/Assignment1/syntax.tex b/Assignment1/syntax.tex index 81a7d7f..5d2830a 100644 --- a/Assignment1/syntax.tex +++ b/Assignment1/syntax.tex @@ -95,7 +95,6 @@ we include an arrow that points to the state for which the formula holds. \begin{figure} \tikzset{intuitive semantics/.style={shorten >=1pt,node distance=16mm,on grid,initial text={},baseline=-0.5ex,->}} - \tikzset{state/.append style={minimum size=15pt}} \tikzset{arbitrary/.style={state,label={[font=\relsize{-2}]arbitrary}}} \centering \[\begin{array}{rcl} @@ -200,6 +199,7 @@ Before turning to the formal semantics in the next subsection, we provide some e \lozenge^{-1} (\phi_3 \land \lozenge^{-1} (\phi_2 \land \lozenge^{-1} \phi_1))\big) + \qedhere \] \end{example} |