diff options
| author | Camil Staps | 2018-04-17 12:24:02 +0200 |
|---|---|---|
| committer | Camil Staps | 2018-04-17 12:24:02 +0200 |
| commit | 12976280c5eb4dbe178387b88977fa43795186cb (patch) | |
| tree | a0b0e4d8f3c75f466b1e6d2634ba77a3f086deb5 /Assignment1/intro.tex | |
| parent | Semantics over paths and states (diff) | |
Start with minimal bad prefixes
Diffstat (limited to 'Assignment1/intro.tex')
| -rw-r--r-- | Assignment1/intro.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Assignment1/intro.tex b/Assignment1/intro.tex index 6df3700..d07be86 100644 --- a/Assignment1/intro.tex +++ b/Assignment1/intro.tex @@ -21,6 +21,6 @@ In other words, there is a class of PLTL formulae% 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. -They are also included in many model checking tools, such as NuSMV. +They are also included in many model checking tools, such as NuSMV.% + \footnote{\url{http://nusmv.fbk.eu/}} For this reason, it is useful to discuss them here. -\cbend |