summaryrefslogtreecommitdiff
path: root/Assignment1/conversion.tex
diff options
context:
space:
mode:
authorErin van der Veen2018-04-17 17:17:45 +0200
committerErin van der Veen2018-04-17 17:17:45 +0200
commit32f44a52799bb1bc385a1ff26704c4ecd936b15f (patch)
tree895bc3644419b4aaab81c47c3ba2a61a41560b3f /Assignment1/conversion.tex
parentStart with minimal bad prefixes (diff)
PLTL to Büchi automaton
Diffstat (limited to 'Assignment1/conversion.tex')
-rw-r--r--Assignment1/conversion.tex56
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