diff options
Diffstat (limited to 'Assignment1/summary.tex')
| -rw-r--r-- | Assignment1/summary.tex | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/Assignment1/summary.tex b/Assignment1/summary.tex index d18e517..31b65f8 100644 --- a/Assignment1/summary.tex +++ b/Assignment1/summary.tex @@ -11,5 +11,18 @@ Because PLTL formulas need to be able to \enquote{look back}, the satisfaction relation $\vDash$ becomes ternary: it is a subset of $\left(2^{AP}\right)^\omega \times \mathbb N \times PLTL$, where the natural number indicates the index at which a trace satisfies a formula. + + \item + For PLTL, there are two different notions of equivalence. + Initial equivalence $\phi \equiv_0 \psi$ means that all paths that satisfy $\phi$ in position 0 must also satisfy $\psi$ in position 0 (and vice versa). + Equivalence $\phi \equiv \psi$ means that for all paths $\pi$ and positions $i$, $\pi \vDash_i \phi$ entails $\pi \vDash_i \psi$ (and vice versa). + + \item + Because past modalities do not increase expressiveness, PLTL formulas can be translated into initially equivalent LTL formulas. + This can be done with syntactic rewrite rules or with a conversion through B\"uchi automata and Muller automata. + + \item + If $vw^\omega$ is a counterexample for a safety property $P$ in a finite transition system $TS$, there exists a $j \le |TS|\cdot2^{|\lnot P|}\cdot|\lnot P|$ for which $vw^j$ is a bad prefix for $P$. + However, in most cases a smaller counterexample (not of the form $vw^k$) can be found by translating $P$ to a finite automaton and running it with $vw^\omega$. \end{itemize} \cbend |