--- a/prio/Paper/document/root.tex	Mon Jan 30 06:46:47 2012 +0000
+++ b/prio/Paper/document/root.tex	Mon Jan 30 08:45:56 2012 +0000
@@ -3,8 +3,8 @@
 \usepackage{isabellesym}
 \usepackage{amsmath}
 \usepackage{amssymb}
-\usepackage{tikz}
-\usepackage{pgf}
+%\usepackage{tikz}
+%\usepackage{pgf}
 %\usetikzlibrary{arrows,automata,decorations,fit,calc}
 %\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}
 %\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf
@@ -17,7 +17,7 @@
 \usepackage{stmaryrd}
 \usepackage{url}
 
-\titlerunning{Myhill-Nerode using Regular Expressions}
+\titlerunning{Proving the Priority Inheritance Protocol Correct}
 
 
 \urlstyle{rm}
@@ -45,23 +45,23 @@
 \maketitle
 
 \begin{abstract}
-In realtime systems with support for resource locking and processes
-involving priorities, one faces the problem of priority
+In realtime systems with support for resource locking and for
+processes with priorities, one faces the problem of priority
 inversion. This problem can make the behaviour of processes
 unpredictable and the resulting bugs can be hard to find.  The
 Priority Inheritance Protocol is one solution implemented in many
 systems for solving this problem, but the correctness of this solution
 has never been formally verified in a theorem prover. As already
-pointed out in the literature, the original description of the
-Property Inheritance Protocol presents an informal correctness
-``proof'' for an \emph{incorrect} algorithm. In this paper we fix the
-problem of the original proof by making all notions precise and
-implementing a variant of a solution proposed earlier. Our
-formalisation in Isabelle/HOL uncovered facts not mentioned in the
-literature, but also shows how to efficiently implement this
-protocol. Earlier correct implementations were criticised as too
-inefficient. Our formalisation is based on Paulson's inductive
-approach to verifying protocols.\medskip
+pointed out in the literature, the original informal investigation of
+the Property Inheritance Protocol presents a correctness ``proof'' for
+an \emph{incorrect} algorithm. In this paper we fix the problem of the
+original proof by making all notions precise and implementing a
+variant of a solution proposed earlier. Our formalisation in
+Isabelle/HOL uncovered facts not mentioned in the literature, but also
+shows how to efficiently implement this protocol. Earlier correct
+implementations were criticised as too inefficient. Our formalisation
+is based on Paulson's inductive approach to verifying
+protocols.\medskip
 
 {\bf Keywords:} Priority Inheritance Protocol, formal connectness proof, 
 realtime systems