diff options
Diffstat (limited to 'Assignment1')
| -rw-r--r-- | Assignment1/conversion.tex | 11 | ||||
| -rwxr-xr-x | Assignment1/library.bib | 17 |
2 files changed, 26 insertions, 2 deletions
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex index 3a08292..7befeb2 100644 --- a/Assignment1/conversion.tex +++ b/Assignment1/conversion.tex @@ -3,7 +3,7 @@ In Subsection~\ref{sec:intro} we stated that past modalities do not increase the expressive power of LTL. In this section we proof this statement by demonstrating two algorithms that can convert any arbitrary PLTL formula to a LTL formula. The first algorithm that we will demonstrate was first presented by Gabbay in 1989~\cite{Gabbay1989} and is based on syntactic rewriting. -The second algorithm makes use of the translation of LTL formulas to automata. +The second algorithm makes use of the translation of PLTL formulas to automata and automata to LTL formulas. We will explain more about this algorithm once we get to it. \erin @@ -101,9 +101,16 @@ I.e. we can also apply these eliminations when a $\Sop$ is within the scope of a The final step of the algorithm entails removing the part of the formula that contains the $\Sop$-operators. +\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} \cbend -%TODO: Provide the syntactic algorithm to convert PLTL to LTL +%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 diff --git a/Assignment1/library.bib b/Assignment1/library.bib index 4eabf0a..fdd6dfd 100755 --- a/Assignment1/library.bib +++ b/Assignment1/library.bib @@ -1,3 +1,20 @@ +@InProceedings{Maler1990, + title={Tight bounds on the complexity of cascaded decomposition of automata}, + author={Maler, Oded and Pnueli, Amir}, + booktitle={Foundations of Computer Science, 1990. Proceedings., 31st Annual Symposium on}, + pages={672--682}, + year={1990}, + organization={IEEE} +} + +@InProceedings{Maler1994, + title={On the Cascaded Decomposition of Automata, its Complexity and its Application to Logic}, + author={Maler, Oded and Pnueli, Amir}, + booktitle={ACTS Mobile Communication}, + year={1994}, + organization={Citeseer} +} + @Article{Markey2003, author = {Markey, Nicolas}, title = {Temporal logic with past is exponentially more succinct}, |