diff -r 12e9aa68d5db -r 4190df6f4488 prio/Paper/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/prio/Paper/document/root.tex	Tue Jan 24 00:20:09 2012 +0000
@@ -0,0 +1,74 @@
+\documentclass[runningheads]{llncs}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\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
+%\usetikzlibrary{matrix}
+\usepackage{pdfsetup}
+\usepackage{ot1patch}
+\usepackage{times}
+%%\usepackage{proof}
+%%\usepackage{mathabx}
+\usepackage{stmaryrd}
+\usepackage{url}
+
+\titlerunning{Myhill-Nerode using Regular Expressions}
+
+
+\urlstyle{rm}
+\isabellestyle{it}
+\renewcommand{\isastyleminor}{\it}%
+\renewcommand{\isastyle}{\normalsize\it}%
+
+
+\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
+\renewcommand{\isasymequiv}{$\dn$}
+\renewcommand{\isasymemptyset}{$\varnothing$}
+\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
+
+\newcommand{\isasymcalL}{\ensuremath{\cal{L}}}
+\newcommand{\isasymbigplus}{\ensuremath{\bigplus}}
+
+\newcommand{\bigplus}{\mbox{\Large\bf$+$}}
+\begin{document}
+
+\title{A Formalisation of Priority Inheritance Protocol \\ 
+       for Correct and Efficient Implementation}
+\author{Xingyuan Zhang\inst{1} \and Christian Urban\inst{2} \and Chunhan Wu\inst{1}}
+\institute{PLA University of Science and Technology, China \and 
+           King's College, University of London, U.K.}
+\maketitle
+
+%\mbox{}\\[-10mm]
+\begin{abstract}
+Despite the wide use of Priority Inheritance Protocol in real time operating
+system, it's correctness has never been formally proved and mechanically checked. 
+All existing verification are based on model checking technology. Full automatic
+verification gives little help to understand why the protocol is correct. 
+And results such obtained only apply to models of limited size. 
+This paper presents a formal verification based on theorem proving. 
+Machine checked formal proof does help to get deeper understanding. We found 
+the fact which is not mentioned in the literature, that the choice of next 
+thread to take over when an critical resource is release does not affect the correctness
+of the protocol. The paper also shows how formal proof can help to construct 
+correct and efficient implementation. 
+\end{abstract}
+
+
+\input{session}
+
+%%\mbox{}\\[-10mm]
+\bibliographystyle{plain}
+\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End: