PLTL to Büchi automaton

1 files changed, 56 insertions, 0 deletions

diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 7befeb2..8468218 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -110,6 +110,62 @@ The Automata-based Algorithm, which we will call the semantic algorithm hence fo
 	\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.
+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.
+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.
+\end{definition}
+Modifying the definition of elementary sets means we must also change Figure 5.20.
+Particularly, we must extend it with the property in Figure~\ref{fig:log_consistent}.
+\begin{figure}
+	\centering
+	\begin{mdframed}
+		\begin{enumerate}
+			\setcounter{enumi}{3}
+		\item B is \emph{locally consistent} with respect to the since operator, i.e., for all $\phi_1 \Sop \phi_2 \in closure(\phi)$:
+			\begin{itemize}
+				\item $\phi_2 \in B \Rightarrow \phi_1 \Sop \phi_2 \in B$
+				\item $\phi_1 \Sop \phi_2 \in B$ and $\phi_2 \not\in B \Rightarrow \phi_1 \in B$
+			\end{itemize}
+		\end{enumerate}
+	\end{mdframed}
+	\caption{Properties of elementary sets of formulae}
+	\label{fig:log_consistent}
+\end{figure}
+
+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:
+\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 $\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:
+\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
+		\begin{enumerate}
+			\item for every $\Xop \psi \in closure(\phi): \Xop\psi \in B \Leftrightarrow \psi \in B'$
+			\item for every $\Xop^{-1} \psi \in closure(\phi): \Xop^{-1}\psi \in B' \Leftrightarrow \psi \in B$
+			\item for every $\phi_1 \Uop \phi_2 \in closure(\phi):$
+				\[
+					\phi_1 \Uop \phi_2 \in B \Leftrightarrow (\phi_2 \in B \vee (\phi_1 \in B \wedge \phi_1 \Uop \phi_2 \in B'))
+				\]
+			\item for every $\phi_1 \Sop \phi_2 \in closure(\phi):$
+				\[
+					\phi_1 \Sop \phi_2 \in B' \Leftrightarrow (\phi_2 \in B' \vee (\phi_1 \in B' \wedge \phi_1 \Sop \phi_2 \in B))
+				\]
+		\end{enumerate}
+\end{itemize}
+
 \cbend
 %Provide the syntactic algorithm to convert PLTL to LTL
 %TODO: Provide algorithm via automata to convert PLTL to LTL