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.

Celiku O.

731.pdf    Gửi cho bạn bè

Từ khóa : Algorithms; Boolean algebra; Data handling; Random processes; Boolean valued functions; Branching-time temporal logic; Nondeterminism; Randomized algorithms; Probabilistic logics