diff options
author | Camil Staps | 2018-04-18 17:01:52 +0200 |
---|---|---|
committer | Camil Staps | 2018-04-18 17:01:52 +0200 |
commit | 6fad72477577dc093ff7302a4b418517dcde290c (patch) | |
tree | 1b5fd3b39cd12c9680f3b7768566a1a01dd229f5 /Assignment1/conversion.tex | |
parent | Finish(?) SSH example (diff) |
Copy-edited first part of semantic algorithm
Diffstat (limited to 'Assignment1/conversion.tex')
-rw-r--r-- | Assignment1/conversion.tex | 29 |
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 |