diff options
author | Erin van der Veen | 2018-04-17 17:17:45 +0200 |
---|---|---|
committer | Erin van der Veen | 2018-04-17 17:17:45 +0200 |
commit | 32f44a52799bb1bc385a1ff26704c4ecd936b15f (patch) | |
tree | 895bc3644419b4aaab81c47c3ba2a61a41560b3f /Assignment1/conversion.tex | |
parent | Start with minimal bad prefixes (diff) |
PLTL to Büchi automaton
Diffstat (limited to 'Assignment1/conversion.tex')
-rw-r--r-- | Assignment1/conversion.tex | 56 |
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 |