summaryrefslogtreecommitdiff
path: root/Assignment1/exercises.tex
diff options
context:
space:
mode:
authorCamil Staps2018-04-18 21:48:33 +0200
committerCamil Staps2018-04-18 21:48:33 +0200
commit25ffc622afc727baa7c5c2918ee602b98bb291a3 (patch)
treef1bffb5db779cc505c70892b91acdfc3e13f24dc /Assignment1/exercises.tex
parentBars everywhere (diff)
Example: protocol dependencies
Diffstat (limited to 'Assignment1/exercises.tex')
-rw-r--r--Assignment1/exercises.tex1
1 files changed, 1 insertions, 0 deletions
diff --git a/Assignment1/exercises.tex b/Assignment1/exercises.tex
index 647755e..ba056d5 100644
--- a/Assignment1/exercises.tex
+++ b/Assignment1/exercises.tex
@@ -64,6 +64,7 @@
\end{exercise}
\begin{exercise}
+ \label{ex:succinctness}
In this exercise we prove that PLTL formulas can be exponentially more succinct.
The proof followed here is that of \citet{Markey2003} which, in turn, is based on work by \citet{Etessami2002}.
The proof is achieved by giving an example of a formula which can be expressed in $\mathcal O(n)$ in PLTL but requires $\Omega(n)$ in LTL.