Ben Strulo, Dov Gabbay, Peter G. Harrison
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 survey some other approaches.
Information from pubs.doc.ic.ac.uk/temporal-stochastic.