diff options
| -rw-r--r-- | Assignment1/assignment1.tex | 9 | ||||
| -rw-r--r-- | Assignment1/bibliographic-notes.tex | 5 | ||||
| -rw-r--r-- | Assignment1/conversion.tex | 21 | ||||
| -rw-r--r-- | Assignment1/exercises.tex | 2 | ||||
| -rwxr-xr-x | Assignment1/library.bib | 8 | ||||
| -rw-r--r-- | Assignment1/summary.tex | 13 |
6 files changed, 35 insertions, 23 deletions
diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex index cb1b363..e859f41 100644 --- a/Assignment1/assignment1.tex +++ b/Assignment1/assignment1.tex @@ -99,8 +99,8 @@ \newcommand{\wfff}{\ifmmode\expandafter\text\fi{\wff\textsuperscript{$+$}}} % Pure future wff \newcommand{\wffp}{\ifmmode\expandafter\text\fi{\wff\textsuperscript{$-$}}} % Pure past wff -\title{Model Checking} -\subtitle{Assignment 1} +\title{Past Modalities in LTL} +\subtitle{Model Checking, Assignment 1} \author{Camil Staps \and Erin van der Veen} \begin{document} @@ -116,25 +116,22 @@ \input{semantics} \input{equivalence} \input{conversion} -%TODO: (Section?) Assess if PLTL is actually more succinct using the examples from the SSH Paper \input{bad-prefix} \input{summary} -\input{bibliographic-notes} \input{exercises} \both \printbibliography \section*{Contribution} -%TODO: Like we are some immature group of children, we have to provide proof of contribution Erin has started writing the text. This text was then copy-edited, slightly corrected where needed and expanded by Camil. (The result was then copy-edited, slightly corrected where needed and expanded by Erin. The result was then copy-edited, slightly corrected where needed and expanded by Camil.)$^\omega$ In the above, yellow bars indicate content primarily contributed by Erin, whereas red bars indicate content primarily contributed by Camil. Thin orange bars indicate material that cannot be attributed to either. -Unfortunately, disabilities of the \textsf{changebar} package make it impossible to indicate the fine-grainedness of our redaction process. +Unfortunately, shortcomings of the \textsf{changebar} package make it impossible to indicate the fine-grainedness of our redaction process. \cbend \end{document} diff --git a/Assignment1/bibliographic-notes.tex b/Assignment1/bibliographic-notes.tex deleted file mode 100644 index e5d7f3a..0000000 --- a/Assignment1/bibliographic-notes.tex +++ /dev/null @@ -1,5 +0,0 @@ -\subsection{Bibliographic Notes} -% TODO: points to be added to 5.4 -% A possibly helpful list is at https://cstheory.stackexchange.com/a/29452 -% Also the bibliography file should be worked through. -\emph{NB: these notes are to be added to the current section 5.4.} diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex index 8919366..5b97530 100644 --- a/Assignment1/conversion.tex +++ b/Assignment1/conversion.tex @@ -299,13 +299,13 @@ After all, these formulas are meaningless for $\vDash_0$, since (using Gabbay's The Automata-based Algorithm, which we will call the semantic algorithm henceforth, is based on the following translations: \begin{enumerate} \item PLTL formulas can be converted to B\"uchi automata~\cite{Lichtenstein1985} - \item B\"uchi automata can be converted to deterministic Muller automata + \item B\"uchi automata can be converted to deterministic Muller automata~\citep{Safra1988} \item Muller automata can be converted to LTL formulae~\cites{Maler1990, Maler1994} \end{enumerate} -Converting an LTL formula to a B\"uchi automata is discussed in Section 5.2 of this book. +Converting an LTL formula to a B\"uchi automaton is discussed in Section 5.2 of this book. Much of this algorithm is the same, -we must just modify some figures and definitions in order to be able to apply it on PLTL formulae. +we only need to modify some figures and definitions in order to be able to apply it on PLTL formulae. The first Definition we must change is 5.35: \begin{definition}[Elementary Sets of PLTL Formulas] $B \subseteq closure(\phi)$ is \emph{elementary} if it is consistent with respect to propositional logic, maximal, and locally consistent with respect to the until and since operators. @@ -376,29 +376,28 @@ Let us first define the Muller Automaton: Converting NBAs to Muller automata was shown to be possible by \citet{McNaughton1966} and is part of what is known as McNaughton's theorem. There are multiple ways to convert a NBA to a Muller Automaton. -In this book we will describe Safra's Determinization Algorithm. +In this book we will describe Safra's Determinization Algorithm~\citep{Safra1988}. -%TODO: Safra's algorithm might be used directly? Safra's algorithm is an algorithm based on subset construction that is capable of determinizing non-deterministic B\"uchi automata. In this book, we will not describe the underlying theory of the algorithm. Instead, we will provide you with a simple description. A more thorough look into the algorithm can be found in a book by Markus Roggenbach~\cite{Roggenbach2002}. We will follow mostly the same description as provided by Roggenbach, with slight modifications. -Let $B = (\mathcal{Q}, \Sigma, q_0, \Delta, F)$ be a NBA. -Safra's algorithm returns an automata without accepting condition where the states are constructed as trees of $\mathcal{Q}$. +Let $B = (Q, \Sigma, q_0, \delta, F)$ be a NBA. +Safra's algorithm returns an automata without accepting condition where the states are constructed as trees of $Q$. Once this automaton is returned, an accepting condition must be chosen. Given that we want to construct a Muller Automaton, we create a set of sets of states containing trees. -For the purpose of this book, Safra's algorithm will therefore be considered to return a Muller Automaton $A = (\mathcal{Q}', \Sigma, q_0', \delta, F')$. +For the purpose of this book, Safra's algorithm will therefore be considered to return a Muller Automaton $A = (Q', \Sigma, q_0', \delta', F')$. -Choose $V := \{1, 2, \dots, 2|\mathcal{Q}|\}$ for denoting nodes in Safra trees. +Choose $V := \{1, 2, \dots, 2\cdot|Q|\}$ for denoting nodes in Safra trees. \begin{enumerate} \item $q_0'$ is the Safra tree\footnote{Safra trees are defined in Roggenbachs book.} consisting of node 1 labelled with macrostate $\{q_0\}$. \item For every input $a$ and tree $T$ with set $N$ of nodes, - the value of the transition function $\delta(T,a)$ is computed as follows: + the value of the transition function $\delta'(T,a)$ is computed as follows: \begin{enumerate} \item Remove all marks ``!'' in $T$ \item For every node $v$ with macrostate $M$ such that $M \cap F \neq \emptyset$, create a new node $v' \in (V\\N)$, such that $v'$ becomes the youngest son of $v$ and carries the macrostate $M \cap F$. @@ -410,7 +409,7 @@ Choose $V := \{1, 2, \dots, 2|\mathcal{Q}|\}$ for denoting nodes in Safra trees. \item Prune all unreachable states. \item Create $F'$ such that for every subset $S$ of $Q'$ it holds that for some $v \in V$: \[ - S \in F' \Leftrightarrow (\forall_{\text{Tree } t \in S} v \text{ is in } t) \wedge (\exists_{\text{Tree } t \in S} v \text{ is marked in } t) + S \in F' \Leftrightarrow (\forall_{\text{Tree } t \in S} v \text{ is in } t) \wedge \exists_{\text{Tree } t \in S} (v \text{ is marked in } t) \] \end{enumerate} diff --git a/Assignment1/exercises.tex b/Assignment1/exercises.tex index ba056d5..930119b 100644 --- a/Assignment1/exercises.tex +++ b/Assignment1/exercises.tex @@ -91,7 +91,7 @@ \begin{answer}% \footnote{Note that this is slightly different from the version in \citet[p. 4]{Markey2003}. The limit on the leftmost $\wedge$ has $i\in[1,n]$ rather than $i\in[0,n]$ in the original paper. - We believe this to be an error, because otherwise $a_0$ is a free variable.} %TODO do you agree? + We believe this to be an error, because otherwise $a_0$ is a free variable.} \[\phi_n(\sigma) = \bigwedge_{\substack{a_i\in\{\top,\bot\}\\i\in[0,n]}} \left[ \left(\lozenge(\bigwedge\nolimits_{i=0}^n p_i=a_i)\right) diff --git a/Assignment1/library.bib b/Assignment1/library.bib index 5f9fbcb..2035c70 100755 --- a/Assignment1/library.bib +++ b/Assignment1/library.bib @@ -159,3 +159,11 @@ year = 2003, pages = {74--88} } + +@inproceedings{Safra1988, + author = {Safra, S.}, + title = {On The Complexity of $\omega$-Automata}, + booktitle = {29th Annual Symposium on Foundations of Computer Science}, + pages = {319--327}, + year = 1988 +} diff --git a/Assignment1/summary.tex b/Assignment1/summary.tex index d18e517..31b65f8 100644 --- a/Assignment1/summary.tex +++ b/Assignment1/summary.tex @@ -11,5 +11,18 @@ Because PLTL formulas need to be able to \enquote{look back}, the satisfaction relation $\vDash$ becomes ternary: it is a subset of $\left(2^{AP}\right)^\omega \times \mathbb N \times PLTL$, where the natural number indicates the index at which a trace satisfies a formula. + + \item + For PLTL, there are two different notions of equivalence. + Initial equivalence $\phi \equiv_0 \psi$ means that all paths that satisfy $\phi$ in position 0 must also satisfy $\psi$ in position 0 (and vice versa). + Equivalence $\phi \equiv \psi$ means that for all paths $\pi$ and positions $i$, $\pi \vDash_i \phi$ entails $\pi \vDash_i \psi$ (and vice versa). + + \item + Because past modalities do not increase expressiveness, PLTL formulas can be translated into initially equivalent LTL formulas. + This can be done with syntactic rewrite rules or with a conversion through B\"uchi automata and Muller automata. + + \item + If $vw^\omega$ is a counterexample for a safety property $P$ in a finite transition system $TS$, there exists a $j \le |TS|\cdot2^{|\lnot P|}\cdot|\lnot P|$ for which $vw^j$ is a bad prefix for $P$. + However, in most cases a smaller counterexample (not of the form $vw^k$) can be found by translating $P$ to a finite automaton and running it with $vw^\omega$. \end{itemize} \cbend |