From addc2942f57bd176fcf93ca3880cffef1d149688 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Thu, 19 Apr 2018 15:08:45 +0200
Subject: Lalala
---
Assignment1/conversion.tex | 21 ++++++++++-----------
1 file changed, 10 insertions(+), 11 deletions(-)
(limited to 'Assignment1/conversion.tex')
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}
--
cgit v1.2.3