summaryrefslogtreecommitdiff
path: root/Assignment1/conversion.tex
diff options
context:
space:
mode:
authorCamil Staps2018-04-18 17:01:52 +0200
committerCamil Staps2018-04-18 17:01:52 +0200
commit6fad72477577dc093ff7302a4b418517dcde290c (patch)
tree1b5fd3b39cd12c9680f3b7768566a1a01dd229f5 /Assignment1/conversion.tex
parentFinish(?) SSH example (diff)
Copy-edited first part of semantic algorithm
Diffstat (limited to 'Assignment1/conversion.tex')
-rw-r--r--Assignment1/conversion.tex29
1 files changed, 15 insertions, 14 deletions
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 72304d2..2a3272d 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -260,7 +260,7 @@ The final step of the algorithm entails removing the parts of the formula that c
\erin
\paragraph{Automata-based Algorithm}
-The Automata-based Algorithm, which we will call the semantic algorithm hence forth, is based on the following translations:
+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
@@ -295,17 +295,17 @@ Particularly, we must extend it with the property in Figure~\ref{fig:log_consist
Furthermore, we need to modify the generation of the B\"uchi automaton.
Let $\phi$ be an PLTL formua over $AP$.
-Let $\mathcal{G}_\phi = (\mathcal{Q}, 2^{AP}, \delta, \mathcal{Q}_0,\mathcal{F})$ where:
+Let $\mathcal{G}_\phi = (Q, 2^{AP}, \delta, Q_0,\mathcal{F})$ where:
\begin{itemize}
- \item $\mathcal{Q}$ is the set of all elementary formulae $B \subseteq closure(\phi)$
- \item $\mathcal{Q}_0 = \{B \in Q \mid \phi \in B\}$
+ \item $Q$ is the set of all elementary sets of formulae $B \subseteq closure(\phi)$
+ \item $Q_0 = \{B \in Q \mid \phi \in B\}$
\item $\mathcal{F} = \{F_{\phi_1 \Uop \phi_2} \mid \phi_1 \Uop \phi_2 \in closure(\phi)\} \cup \{F_{\phi_1 \Sop \phi_2} \mid \phi_1 \Sop \phi_2 \in closure(\phi)\}$ where
\begin{align*}
F_{\phi_1 \Uop \phi_2} &= \{B \in Q \mid \phi_1 \Uop \phi_2 \not\in B \text{ or } \phi_2 \in B\}\\
F_{\phi_1 \Sop \phi_2} &= \{B \in Q \mid \phi_1 \Sop \phi_2 \not\in B \text{ or } \phi_2 \in B\}
\end{align*}
\end{itemize}
-The transition relation $\delta : \mathcal{Q} \times 2^{AP} \rightarrow 2^\mathcal{Q}$ is given by:
+The transition relation $\delta : Q \times 2^{AP} \rightarrow 2^Q$ is given by:
\begin{itemize}
\item If $A \neq B \cap AP$, then $\delta(B,A) = \emptyset$
\item If $A = B \cap AP$, then $\delta(B,A)$ is the set of all elementary sets of formulas $B'$ satisfying
@@ -326,17 +326,18 @@ The transition relation $\delta : \mathcal{Q} \times 2^{AP} \rightarrow 2^\mathc
The next step in the conversion algorithm is converting the B\"uchi Automaton into a deterministic Muller Automaton.
Let us first define the Muller Automaton:
\begin{definition}[Deterministic Muller Automaton]
- A deterministic Muller automaton~\cite{McNaughton1966} is a tuple $A = (\mathcal{Q}, \Sigma, \delta, \mathcal{Q}_0,F)$ where
- \begin{description}
- \item[$\mathcal{Q}$] is a finite set of states
- \item[$\Sigma$] is an alphabet
- \item[$\delta: \mathcal{Q} \times \Sigma \rightarrow \mathcal{Q}$] is a transition function
- \item[$\mathcal{Q}_0 \subseteq \mathcal{Q}$] is a set of initial states
- \item[$\mathcal{F} \subseteq \mathcal{P}(\mathcal{Q})$] is a set of sets of states that define the acceptance condition. $A$ accepts exactly those runs in which the set of infinitely often occurring states in an element of $\mathcal{F}$.
- \end{description}
+ A deterministic Muller automaton~\cite{McNaughton1966} is a tuple $A = (Q, \Sigma, \delta, Q_0,\mathcal F)$ where
+ \begin{itemize}
+ \item $Q$ is a finite set of states
+ \item $\Sigma$ is an alphabet
+ \item $\delta: Q \times \Sigma \rightarrow Q$ is a transition function
+ \item $Q_0 \subseteq Q$ is a set of initial states
+ \item $\mathcal{F} \subseteq \mathcal{P}(Q)$ is a set of sets of states that define the acceptance condition. $A$ accepts exactly those runs in which the set of infinitely often occurring states in an element of $\mathcal{F}$.
+ \qedhere
+ \end{itemize}
\end{definition}
-Converting a NBA to a Muller automaton was shown to be possible by R. McNaughton~\cite{McNaughton1966}
+Converting NBAs to Muller automata was shown to be possible by \citet{McNaughton1966}
and is part of what is known as McNaughton's theorem.
\cbend