diff --git a/prism/benchmark.org b/prism/benchmark.org index 80cc5571c892658d8510972249c93cbd7babe050..64c0e99643866d91a592c4eb775f19c3fa2d660a 100644 --- a/prism/benchmark.org +++ b/prism/benchmark.org @@ -1,4 +1,5 @@ #+TITLE: PRISM Benchmarks +#+LATEX_HEADER: \usepackage[a4paper,margin=1in,landscape]{geometry} * Introduction @@ -1190,7 +1191,7 @@ We consider the scenario where two stations trying to send packets simultaneously. The PRISM model is taken from [KNS02a] using the integer semantics given in [KNS06]. In the model one time unit - corresponds to 50μs and to ensure integer bounds, where neccessary, scaling lower bound constraints down and + corresponds to 50\mu s and to ensure integer bounds, where neccessary, scaling lower bound constraints down and upper bound constraints up to sensure a sound abstraction. For more information on the probabilistic timed automata see: http://www.prismmodelchecker.org/casestudies/wlan.php