diff options
author | Camil Staps | 2018-04-22 21:06:02 +0200 |
---|---|---|
committer | Camil Staps | 2018-04-22 21:06:02 +0200 |
commit | 66bf033eca9975aed38a456ad383ce005fea62d3 (patch) | |
tree | 98bfda0b90ec673512e6214365dcea5d6cdf5b97 /Assignment1/conversion.tex | |
parent | Add very tiny explenation of cascade product and Krohn-Rhodes Theorem (diff) |
OCD (if this causes conflict, feel free to rollback)
Diffstat (limited to 'Assignment1/conversion.tex')
-rw-r--r-- | Assignment1/conversion.tex | 43 |
1 files changed, 25 insertions, 18 deletions
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex index 6977f4a..1138e11 100644 --- a/Assignment1/conversion.tex +++ b/Assignment1/conversion.tex @@ -171,7 +171,8 @@ After all, these formulas are meaningless for $\vDash_0$, since (using Gabbay's &\equiv \lnot (\top \Uop (\lnot (c \rightarrow \lnot f \Sop s)))\\ &\equiv \lnot (\top \Uop (c \land \lnot (\lnot f \Sop s))). \end{align*} - With Gabbay's $\Uop$ and $\Sop$, this becomes (first rewriting the $\Sop$, then the $\Uop$): + With Gabbay's $\Uop$ and $\Sop$, this becomes (first rewriting the $\Sop$, then the $\Uop$):% + \footnote{We will informally use $\rightarrow$ for rewriting here, reserving $\equiv$ for true equivalence.} \begin{align*} \lnot (\top \Uop (c \land \lnot(\lnot f \Sop s))) &\rightarrow \lnot (\top \Uop (c \land \lnot(s \lor \lnot f \land \lnot f \Sop s)))\\ @@ -382,29 +383,34 @@ 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~\citep{Safra1988}. -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. +Safra's algorithm is an algorithm to determinize B\"uchi automata, based on subset construction. +This means that we consider sets of states in the original automaton, like we did for the determinization of NFAs described in section 4.1. +These sets of states we call \emph{macrostates}. +In this book, we will not describe the underlying theory of Safra's algorithm. +Instead, we will provide a simple description. +A more thorough discussion of the algorithm is given by \citet{Roggenbach2002}. +We will mostly follow this description, with slight modifications. 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$. +Safra's algorithm returns an automaton without acceptance criterion where the states are constructed as trees of $Q$. Once this automaton is returned, -an accepting condition must be chosen. +an acceptance criterion 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 = (Q', \Sigma, q_0', \delta', F')$. -Choose $V := \{1, 2, \dots, 2\cdot|Q|\}$ for denoting nodes in Safra trees. +Choose $V := \{1, 2, \dots, 2\cdot|Q|\}$ for denoting nodes in Safra trees.% + \footnote{Safra trees are defined by \citet{Roggenbach2002}. + In short, they are ordered trees with macrostates as labels.} \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 $q_0'$ is the Safra tree consisting of only the 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: \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$. + %TODO: this mark is not mentioned anywhere else right now. Perhaps explain the intuition first. + \item For every node $v$ with macrostate $M$ such that $M \cap F \neq \emptyset$, create a new node $v' \in (V\setminus N)$, such that $v'$ becomes the youngest son of $v$ and carries the macrostate $M \cap F$. \item Perform subset construction on every $v$. \item Perform horizontal merge on every node $v$. \item Remove all nodes with empty macrostates. @@ -413,30 +419,31 @@ Choose $V := \{1, 2, \dots, 2\cdot|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} -The last step of the algorithm is converting the Muller automaton to an LTL formula based on the decomposition of automata as described by O. Maler and A. Pnueli~\cite{Maler1994}. -The decomposition of finite automata was first described by K. Krohn and J. Rhodes as is known as the Krohn-Rhodes theorem~\cite{Krohn1965}. -This theorem, in combination with the work of A. Meyer~\cite{Meyer1969} allows for the translation of Muller automaton to LTL. +The last step of the algorithm is converting the Muller automaton to an LTL formula based on the decomposition of automata as described by \citet{Maler1994}. +The decomposition of finite automata was first described by \citet{Krohn1965} and is known as the Krohn-Rhodes theorem. +This theorem, in combination with the work of \citet{Meyer1969}, allows for the translation of Muller automaton to LTL. \begin{definition}[Cascade Product~\cite{Maler2010}] Let $A = (Q, \Sigma, \delta)$ be an automaton, and let $B = (Q \times \Sigma, Q', \delta')$ be an automaton such that for all $q \in Q$ and $q' \in Q'$, either $\delta'(q',(q,\sigma))$ is defined for all $\sigma \in \Sigma$ or it is undefined for every $\sigma$. The cascade product $A \circ B$ is the automaton $C = (\Sigma, Q'', \delta'')$ where \[ - Q'' = \{(q, q') \mid \delta'(q',(q,\sigma))\ is\ defined\} + Q'' = \{(q, q') \mid \delta'(q',(q,\sigma)) \ne \bot\} \] and \[ \delta''((q,q'),\sigma) = (\delta(q',\sigma),\delta'(q',(q,\sigma))) + \qedhere \] \end{definition} \begin{theorem}[Krohn-Rhodes Theorem] For every automaton $A$ there exists a cascade $C = B_1 \circ B_2 \circ \dots \circ B_n$ such that: \begin{enumerate} - \item Each $B_i$ is a permutation-reset automaton\footnote{Definition ommited for brevity} - \item There is a homomorphism\footnotemark[10] $\phi$ from $C$ to $A$ + \item Each $B_i$ is a permutation-reset automaton\footnote{\label{note:definition-omitted}Definition omitted for brevity.} + \item There is a homomorphism\footnote{See \cref{note:definition-omitted}.} $\phi$ from $C$ to $A$ \item Any permutation in some $B_i$ is homomorphic to a subgroup of the tranformation semigroup of $A$ \end{enumerate} \end{theorem} |