ABSTRACT
Temporal logic has proved to be a useful tool for the specification of computer systems interacting with their environment. Meanwhile, a common approach to the analysis of the performance of such systems has been based on stochastic process theory and, in particular, Markov chains. We describe an approach to modelling a temporal logic system in a random environment and how Markov chain techniques can be applied. We also survey some other approaches.
