diff options
| author | Camil Staps | 2018-04-18 19:33:40 +0200 |
|---|---|---|
| committer | Camil Staps | 2018-04-18 19:33:40 +0200 |
| commit | 32f1f4867bad79eb4d5afd179697b92699521698 (patch) | |
| tree | b617e249813c3d0b2d38a47abc8939e88e499d04 /Assignment1/intro.tex | |
| parent | Finish(?) SSH example (diff) | |
Minor enhancements
Diffstat (limited to 'Assignment1/intro.tex')
| -rw-r--r-- | Assignment1/intro.tex | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Assignment1/intro.tex b/Assignment1/intro.tex index d07be86..15294ee 100644 --- a/Assignment1/intro.tex +++ b/Assignment1/intro.tex @@ -17,7 +17,8 @@ Eventually, formal computing scientists stopped using past modalities for reason In 2003, Nicolas Markey showed that while past modalities do not increase expressive power, they can make LTL formulas exponentially more succinct~\cite{Markey2003}. In other words, there is a class of PLTL formulae% - \footnote{In keeping with the style of the rest of the book, we alternate between \enquote{formulas} and \enquote{formulae} and wish the reader best of luck with this.} + \footnote{In keeping with the style of the rest of the book, we alternate between \enquote{formulas} and \enquote{formulae} and wish the reader best of luck with this. + (Like the book, this section may contain typos and inaccuracies. These are however not intentional.)} for which the size of all equivalent LTL formulas is $\Omega\left(2^n\right)$. Markey achieves this proof by providing a formula that is in exactly this class. Besides being smaller, PLTL formulas can also be easier to write and understand, as examples below will demonstrate. |