path: root/Assignment1/conversion.tex

\erin
\subsubsection{PLTL to LTL}
Above, we stated that past modalities do not increase the expressive power of LTL.
In this section we prove this statement by demonstrating two algorithms that can convert a arbitrary PLTL formulas to initially equivalent LTL formulas.
The first algorithm was first presented by \citet{Gabbay1989} in 1989 and is based on syntactic rewriting.
The second algorithm makes use of the translation of PLTL formulas to automata and automata to LTL formulas.
This algorithm is described in more detail below.

\paragraph{Syntactic Algorithm}
The syntactic algorithm as proposed by Gabbay has its foundation in the following three facts:%
	\footnote{%
		Note that Gabbay used a slightly different, \enquote{non-strict} definition for the $\Uop$ and $\Sop$ operators.
		\camil
		We then get $\sigma \vDash_i \phi_1 \Uop \phi_2 \Leftrightarrow \exists_{j > i}[\sigma \vDash_j \phi_2]$ and $\sigma \vDash_k \phi_1$ for all $i < k < j$ (rather than $i \le k < j$), and similarly for $\Sop$.
		Thus, our $\phi \Uop \psi$ is equivalent to Gabbay's $\psi \lor \phi \land \phi \Uop \psi$.
		Gabbay's $\phi \Uop \psi$ is equivalent to our $\Xop (\phi \Uop \psi)$.
		Also for the $\Sop$ operator is not hard to convert PLTL formulas with the semantics of \cref{def:pltl:semantics-words} to Gabbay's variant or vice versa.
		\erin
		For this paragraph we will use Gabbay's definitions.}
\begin{enumerate}
	\item Every PLTL formula can be written using no other temporal operators than $\Sop$ and $\Uop$ operators.
	\item Every formula $\phi$ containing only the $\Sop$ and $\Uop$ operators can be written as a boolean combination of $\wfff \cup \wffp \cup \wffn$.
	\item The same formula without past modalities $\psi$, a boolean combination of $\wfff \cup \wffn$, is initially equivalent to $\phi$.
\end{enumerate}
When these facts are considered in sequence,
they result in an algorithm that, given a PLTL formula, produces an initially equivalent LTL formula.
We will now consider these facts in more detail.

Step 1 of the algorithm was proven by Kamp in is 1968 PhD thesis \citep{Kamp1968}.
It can also be shown by a set of rewrite rules, the approach taken by \citet{Gabbay1989}.
The correctness then follows from the formal semantics of the operators.
We only need to rewrite $\Xop$ and $\Xop^{-1}$.
Gabbay also gives rewrite rules for $\square$, $\lozenge$ and their PLTL counterparts, but since we have defined them as derived operators this is not necessary.
The next and previous operators can be rewritten as:
\[
	\begin{array}{ll}
		\Pop\phi &\rightarrow\enspace \bot \Sop \phi\\
		\Xop\phi &\rightarrow\enspace \bot \Uop \phi
	\end{array}
\]

Step 2 of the algorithm entails rewriting the formula containing only $\Uop$ and $\Sop$ to a form where there is no $\Sop$ in the scope of a $\Uop$, nor vice versa.
Gabbay proves that this can by done in Theorem 2.4 of his paper via a tedious case distinction.
The different cases are listed below.
For the proofs of the equivalences, we refer the reader to the appendix of \citet{Gabbay1989}.
\begin{enumerate}
	\item Suppose $E = q \Sop (a \wedge \alpha \Uop \beta)$, then $E \equiv E_1 \vee E_2 \vee E_3$ where:
		\begin{align*}
			E_1 &= q \Sop a \wedge \alpha \Sop a \wedge \alpha \wedge \alpha \Uop \beta\\
			E_2 &= \beta \wedge (\alpha \wedge q) \Sop a\\
			E_3 &= q \Sop (\beta \wedge q \wedge \alpha \Sop a \wedge q \Sop a)
		\end{align*}
\end{enumerate}

\camil
\begin{remark}[Intuition Behind the Elimination Rules]
	The intuition behind Gabbay's first elimination rule is as follows.
	If $q \Sop (a \land \alpha \Uop \beta)$, we know that at some point $t$, $a$ held, and that after $t$, $q$ held until the present moment.
	For the moment of fulfilment of $\alpha \Uop \beta$ we distinguish three cases:
	\begin{enumerate}
		\item
			$\alpha$ continuously held since $t$, presently holds, and continues to hold until at some point in the future $\beta$ holds.
		\item
			$\alpha$ has held since $t$ and at present $\beta$ holds.
		\item
			$\alpha$ has held since $t$ until some moment in the past at which $\beta$ held.
	\end{enumerate}
	These cases correspond to the elements of the disjunction $E_1$, $E_2$ and $E_3$, respectively.
	Note that case 2 and 3 are only different because of Gabbay's non-strict semantics.

	It is now easy to reconstruct the case where $\Sop$ and $\Uop$ are swapped, i.e. $E = q \Uop (a \land \alpha \Sop \beta)$.
	In this case, $q$ holds from the next moment until some moment $t$ at which $a$ will hold.
	For the moment of fulfilment of $\alpha \Sop \beta$ we distinguish three cases:
	\begin{enumerate}
		\item
			$\beta$ held at some moment in the future. $\alpha$ held continuously after that moment, including the present moment and up to $t$.
		\item
			$\beta$ currently holds and $\alpha$ continuously holds until $t$.
		\item
			At some point in the future (before $t$), $\beta$ will hold, after which $\alpha$ continuously holds until $t$.
	\end{enumerate}
	Thus we get $E \equiv E_1 \lor E_2 \lor E_3$ where:
	\begin{align*}
		E_1 &= q \Uop a \land \alpha \Uop a \land \alpha \land \alpha \Sop \beta\\
		E_2 &= \beta \land (q \land \alpha) \Uop a\\
		E_3 &= q \Uop (\beta \land q \land \alpha \Uop a \land q \Uop a)
	\end{align*}
	The reasoning behind the other elimination rules is similar and will not be discussed in detail.
\end{remark}

\erin
\begin{enumerate}[resume]
	\item Suppose $E = q \Sop (a \wedge \neg (\alpha \Uop \beta))$, then $E \equiv E_1 \vee E_2 \vee E_3$ where:
		\begin{align*}
			E_1 &= (a \wedge \neg \beta \Sop a) \wedge \neg \beta \wedge \neg (\alpha \Uop \beta)\\
			E_2 &= \neg \beta \wedge \neg \alpha \wedge (\neg \beta \wedge q \Sop a)\\
			E_3 &= a\Sop\neg\beta \wedge \neg \alpha \wedge q \wedge (q \wedge \neg\beta \Sop a)
		\end{align*}

	\item Suppose $E = q \Sop (a \wedge \neg (\alpha \Uop \beta))$, then $E \equiv E_1 \vee E_2 \vee E_3$ where:
		\begin{align*}
			E_1 &= (q \wedge \neg \beta \Sop a) \wedge \neg \beta \wedge \neg (\alpha \Uop \beta)\\
			E_2 &= \neg \beta \wedge \neg \alpha \wedge (\neg \beta \wedge q \Sop a)\\
			E_3 &= q \Sop (\neg \beta \wedge \neg \alpha \wedge q \wedge (\neg \beta \wedge q \Sop a))
		\end{align*}

	\item Suppose $E = (q \vee \neg (\alpha \Uop \beta)) \Sop a$, then $E \equiv \neg (\neg a \Sop \neg q \wedge (\alpha \Uop \beta) \wedge \neg a) \wedge \Fop^{-1} a$,
		which can be reduced via rule 1.

	\item Suppose $E = (q \vee \alpha \Uop \beta) \Sop (a \wedge \alpha \Uop \beta)$, then $E \equiv E_1 \vee (E_2 \wedge E_3)$ where:
		\begin{align*}
			E_1 &= (\alpha \Sop a) \wedge (\beta \vee (\alpha \wedge (\alpha \Uop \beta)))\\
			E_2 &= (\beta \vee \alpha \vee \neg(\neg\beta \Sop \neg q) \Sop \beta \wedge (\alpha \Sop a))\\
			E_3 &= (\beta \vee (\alpha \wedge (\alpha \Uop \beta))) \vee \neg (\neg\beta \Sop \neg q)
		\end{align*}
	
	\item Suppose $E = (q \vee \alpha \Uop \beta) \Sop (a \wedge \neg(\alpha \Uop \beta))$, then $E \equiv E_1 \vee E_2 \vee E_3$ where:
		\begin{align*}
			E_1 &= (\neg \beta \wedge q \Sop a) \wedge \neg \beta \wedge \neg \alpha\\
			E_2 &= q \vee (\alpha \Uop \beta) \Sop \neg \beta \wedge \neg \alpha \wedge (q \vee (\alpha \Uop \beta)) \wedge (\neg \beta \wedge q \Sop a)\\
			E_3 &= (q \wedge \neg \beta \Sop a) \wedge \neg \beta \wedge \neg (\alpha \Uop \beta)
		\end{align*}

	\item Suppose $E = (q \vee \neg(\alpha \Uop \beta)) \Sop (a \wedge \alpha \Uop \beta)$, then $E \equiv E_1 \vee E_2$ where:
		\begin{align*}
			E_1 &= (q \vee \neg (\alpha \Uop \beta) \Sop \beta \wedge (q \vee \neg (\alpha \Uop \beta)) \wedge (\alpha \wedge q \Sop a))\\
			E_2 &= (\alpha \wedge q \Sop a) \wedge \alpha \wedge (\alpha \Uop \beta)
		\end{align*}
		$E_1$ can be further reduced using eliminations 8 and 4.
	\item Suppose $E = (q \vee \neg (\alpha \Uop \beta)) \Sop (a \wedge \neg (\alpha \Uop \beta))$, then $E \equiv \neg \Gop^{-1}(E_1 \vee E_2 \vee E_3)$ where:
		\begin{align*}
			E_1 &= \neg a \vee \neg (\alpha \Uop \beta)\\
			E_2 &= \neg a \vee (\alpha \Uop \beta) \Sop \neg q \wedge (\alpha \Uop \beta) \wedge \neg a\\
			E_3 &= \neg a \vee (\alpha \Uop \beta) \Sop \neg q \wedge (\alpha \Uop \beta)
		\end{align*}
		After elimination of $\Gop^{-1}$, this formula can be further eliminated, in particular using elimination 5.
\end{enumerate}

Note that these rules can only be applied when a $\Uop$ is within the scope of a $\Sop$.
In order to move the $\Sop$ out of the scope of the $\Uop$, consider that $\Sop$ and $\Uop$ are symmetrical.
These equivalences also hold when the path is reversed, so similar elimination rules exist for the case that $\Sop$ occurs within the scope of $\Uop$.

The final step of the algorithm entails removing the parts of the formula that contains the $\Sop$-operators.

\camil
\begin{example}[Properties for an Authentication System]
	Consider again the property from \cref{ex:pltl:authentication-system}, repeated here with less verbose names:
	$\square (c \rightarrow \lnot f \Sop s)$.
	This can be rewritten to a form with only $\Uop$ and $\Sop$:
	\begin{align*}
		\square(c \rightarrow \lnot f \Sop s)
		&\equiv \lnot \lozenge \lnot (c \rightarrow \lnot f \Sop s)\\
		&\equiv \lnot (\top \Uop (\lnot (c \rightarrow \lnot f \Sop s)))\\
		&\equiv \lnot (\top \Uop (c \land \lnot (\lnot f \Sop s))).
	\end{align*}
	With Gabbay's $\Uop$ and $\Sop$, this becomes (first rewriting the $\Sop$, then the $\Uop$):
	\begin{align*}
		\lnot (\top \Uop (c \land \lnot(\lnot f \Sop s)))
		&\rightarrow \lnot (\top \Uop (c \land \lnot(s \lor \lnot f \land \lnot f \Sop s)))\\
		&\equiv \lnot (\top \Uop (c \land \lnot s \land f \land \lnot (\lnot f \Sop s))) \\
		&\rightarrow \lnot ((c \land \lnot s \land f \land \lnot (\lnot f \Sop s)) \lor (\top \Uop (c \land \lnot s \land f \land \lnot (\lnot f \Sop s))))\\
		&\equiv \lnot (c \land \lnot s \land f \land \lnot (\lnot f \Sop s)) \land \lnot(\top \Uop (c \land \lnot s \land f \land \lnot (\lnot f \Sop s)))\\
		&\equiv (\lnot c \lor s \lor \lnot f \Sop s) \land \lnot(\top \Uop (c \land \lnot s \land f \land \lnot (\lnot f \Sop s))).
	\end{align*}
	% TODO: step 2 and 3 on the right part (S nested in U)
\end{example}

\erin
\paragraph{Automata-based Algorithm}
The Automata-based Algorithm, which we will call the semantic algorithm hence forth, 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
	\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}

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}
\end{definition}

Converting a NBA to a Muller automaton was shown to be possible by R. McNaughton~\cite{McNaughton1966}
and is part of what is known as McNaughton's theorem.

\cbend
%Provide the syntactic algorithm to convert PLTL to LTL
%TODO: Provide algorithm via automata to convert PLTL to LTL
%TODO: In both cases make use of examples from SSH Paper