tpmlo.bbl
\begin{thebibliography}{10}
\expandafter\ifx\csname url\endcsname\relax
  \def\url#1{\texttt{#1}}\fi
\expandafter\ifx\csname urlprefix\endcsname\relax\def\urlprefix{URL }\fi

\bibitem{alurdill}
R.~Alur, D.~L. Dill, A theory of timed automata, Theoretical Computer Science
  126 (1994) 183--235.

\bibitem{byz}
F.~B. Schneider, Implementing fault-tolerant services using the state machine
  approach: a tutorial, ACM Computing Surveys 22 (1990) 299--319.

\bibitem{KNS03b}
M.~Kwiatkowska, G.~Norman, J.~Sproston, Probabilistic model checking of
  deadline properties in the {IEEE 1394 FireWire} root contention protocol,
  Formal Aspects of Computing 14 (2003) 295--318.

\bibitem{DKN04}
C.~Daws, M.~Kwiatkowska, G.~Norman, Automatic verification of the {IEEE} 1394
  root contention protocol with {KRONOS} and {PRISM}, International Journal on
  Software Tools for Technology Transfer (STTT) 5 (2004) 221--236.

\bibitem{segala}
M.~Kwiatkowska, G.~Norman, R.~Segala, J.~Sproton, Automatic verification of
  real-time systems with discrete probability distribuitions, Theoretical
  Computer Science 282 (2002) 101--150.

\bibitem{daniele}
D.~Beauquier, On probabilistic timed automata, Theoretical Computer Science 292
  (2003) 65--84.

\bibitem{barbuti}
R.~Barbuti, L.~Tesei, Timed automata with urgent transitions, Acta Informatica
  40 (2004) 317--347.

\bibitem{acetourg}
L.~Aceto, P.~Bouyer, A.~B. K.~G. Larsen, The power of reachability testing for
  timed auotomata, Theoretical Computer Science 300 (2003) 411--475.

\bibitem{urgency}
S.~Bornot, J.~Sifakis, S.~Tripakis, Modeling urgency in timed systems, in:
  COMPOS'97: Revised Lectures from the International Symposium on
  Compositionality: The Significant Difference, Springer-Verlag, 1998, pp.
  103--129.

\bibitem{bornot97relating}
{S. Bornot}, {J. Sifakis}, Relating time progress and deadlines in hybrid
  systems, in: {H}ybrid and {R}eal-{T}ime {S}ystems, Springer Verlag, LNCS
  1201, 1997, pp. 286--300.

\bibitem{tutorial04}
G.~Behrmann, A.~David, K.~G. Larsen, A tutorial on {\sc uppaal}, in:
  M.~Bernardo, F.~Corradini (Eds.), Formal Methods for the Design of Real-Time
  Systems: 4th International School on Formal Methods for the Design of
  Computer, Communication, and Software Systems, SFM-RT 2004, no. 3185 in LNCS,
  Springer--Verlag, 2004, pp. 200--236.

\bibitem{daniele2}
D.~Beauquier, A.~Rabinovich, A.~Slissenko, A logic of probability with
  decidable model-checking, in: Proceedings of the International Congress on
  Computer Science Logic, no. 2471 in Lecture Notes in Computer Science,
  Springer, Berlin, 2002, pp. 306--321.

\bibitem{kemeny}
J.~G. Kemeny, J.~L. Snell, Finite Markov Chains, Van Nostrand, 1960.

\bibitem{alurprob}
R.~Alur, C.~Courcoubetis, D.~L. Dill, Verifying automata specifications of
  probabilistic real-time systems, in: Proceedings of the Real-Time: Theory in
  Practice, REX Workshop, Springer-Verlag, 1992, pp. 28--44.

\bibitem{BaierK98}
C.~Baier, M.~Z. Kwiatkowska, On the verification of qualitative properties of
  probabilistic processes under fairness constraints., Inf. Process. Lett. 66
  (1998) 71--79.

\bibitem{buchi}
J.~R. B{\"u}chi, On a decision method in restricted second order arithmetic,
  in: Proceedings of the International Congress on Logic, Method, and
  Philosophy of Science, Stanford Univ. Press, 1962, pp. 1--12.

\bibitem{thomas}
W.~Thomas, Automata on infinite objects, Handbook of Theoretical Computer
  Science Volume B (1990) 133--192.

\bibitem{daniele3}
D.~Beauquier, Markov decision processes and deterministic {B\"uchi} automata,
  Fundamenta Informaticae 50 (2002) 1--13.

\bibitem{vardi}
M.~Vardi, Automatic verification of probabilistic concurrent finite-state
  programs, in: In Proceedings of 26th Annual Symposium on Foundations of
  Computer Science, IEEE Computer Society Press, 1985, pp. 327--338.

\bibitem{francesiCAV2000}
P.~Bouyer, C.~Dufourd, E.~Fleury, A.~Petit, Updatable timed automata,
  Theoretical Computer Science 321 (2004) 291--345.

\bibitem{alurprob2}
R.~Alur, C.~Courcoubetis, D.Dill, Model-checking for probabilistic real-time,
  in: International Colloquium on Automata, Languages, and Programming, no. 510
  in Lecture Notes in Computer Science, Springer, Berlin, 1991, pp. 115--126.

\bibitem{bouyer}
P.~Bouyer, Timed automata may cause some troubles, Tech. Rep. LSV-02-9, CNRS \&
  ENS de Cachan (2002).
\newline\urlprefix\url{www.lsv.ens-cachan.fr/Publis}

\bibitem{ferrante}
K.~Ferrante, C.~Rackoff, A decision procedure for first-order theory of real
  addition with order, SIAM Journal on Computing 4 (1975) 69--76.

\bibitem{aziz}
A.~Aziz, V.~Singhal, F.~Balarin, R.~K. Brayton, A.~L. Sangiovanni-Vincentelli,
  It is usually works: the temporal logics of stochastic systems, in: Computer
  Aided Verification, no. 939 in Lecture Notes in Computer Science, Springer,
  Berlin, 1995, pp. 155--165.

\bibitem{hansson2}
H.~A. Hansson, B.~Jonsson, A logic of reasoning about time and probability,
  Formal Aspects of Computing 6 (1994) 512--535.

\bibitem{lehmann}
D.~Lehmann, S.~Shelah, Reasoning about time and change, Information and Control
  53 (1982) 165--198.

\bibitem{couryanna}
C.~Courcoubetis, M.~Yannakakis, The complexity of probabilistic verification,
  Journal of the {ACM} 42 (1995) 340--367.

\end{thebibliography}
