diff options
| author | Camil Staps | 2018-07-04 10:08:07 +0200 |
|---|---|---|
| committer | Camil Staps | 2018-07-04 10:08:07 +0200 |
| commit | 42bc693984173f1cd670eb71f96723cc4458111c (patch) | |
| tree | c78697306f39d113434babb367befedba35f933a /Assignment1 | |
| parent | Add docker image with storm+stormpy (diff) | |
| parent | Finish Summary (diff) | |
Merge branch 'master' of gitlab.science.ru.nl:eveen/Model-Checking
Diffstat (limited to 'Assignment1')
| -rw-r--r-- | Assignment1/conversion.tex | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex index fe9b136..be5196f 100644 --- a/Assignment1/conversion.tex +++ b/Assignment1/conversion.tex @@ -446,14 +446,15 @@ This theorem, in combination with the work of \citet{Meyer1969}, allows for the \begin{enumerate} \item Each $B_i$ is a permutation-reset automaton\footnote{\label{note:definition-omitted}Definition omitted for brevity.} \item There is a homomorphism\footnote{See \cref{note:definition-omitted}.} $\phi$ from $C$ to $A$ - \item Any permutation in some $B_i$ is homomorphic to a subgroup of the tranformation semigroup of $A$ + \item Any permutation in some $B_i$ is homomorphic to a subgroup of the transformation semigroup of $A$ \end{enumerate} \end{theorem} The cascade product can then be used to create star-free regular sets. These sets can then be transformed into LTL formulae. +We will not discuss this transformation in detail since it lies beyond the scope of this book. \cbend %Provide the syntactic algorithm to convert PLTL to LTL -%TODO: Provide algorithm via automata to convert PLTL to LTL +%Provide algorithm via automata to convert PLTL to LTL %TODO: In both cases make use of examples from SSH Paper |