Quantitative temporal logic mechanized in HOL
The paper describes an implementation in the HOL theorem prover of the quantitative Temporal Logic (qTL) of Morgan and McIver [18,14]. qTL is a branching-time temporal logic suitable for reasoning about probabilistic nondeterministic systems. The interaction between probabilities and nondeterminism, which is generally very difficult to reason about, is handled by interpreting the logic over real- rather than boolean-valued functions. In the qTL framework many laws of standard branching-time temporal logic generalize nicely giving access to a number of logical tools for reasoning about quantitative aspects of randomized algorithms. © Springer-Verlag Berlin Heidelberg 2005.