In Silico Modelling and Analysis 
  of Ribosome Kinetics and aa-tRNA Competition
D. Bosnacki, T.E. Pronk and E.P. de Vink

We present a formal analysis of ribosome kinetics using
pro\-babilistic model checking and the tool Prism. We compute
different parameters of the model, like probabilities of translation
errors and average insertion times per codon. The model predicts
strong correlation to the quotient of the concentrations of the
so-called cognate and near-cognate tRNAs, in accord with experimental
findings and other studies.  Using piecewise analysis of the model, we
are able to give an analytical explanation of this observation.