Computer Laboratory Home Page Search A-Z Directory Help
University of Cambridge Home Logic and Semantics Seminar
30th May, 2003: Annabelle McIver
Computer Laboratory > Research > TSG > Logic and Semantics Seminar > 30th May, 2003: Annabelle McIver

Speaker: Annabelle McIver, Macquarie University, Sydney
Title: Games, Probability and the Quantitative Mu-calculus
Time: 30th May, 2003, 14:00
Venue: William Gates Building, room FW11
Abstract:

The Mu-calculus is a powerful tool for specifying and verifying transition systems, including those with demonic (universal) and angelic (existential) choice; its quantitative generalisation qMu --- a quantitative real-typed calculus --- extends that to include probabilistic choice by interpreting expressions as real- rather than Boolean-valued functions of the state. qMu can be used to generate proof rules for probabilistic temporal logic, and, more generally, is expressive enough to formalise a wide range of problems from the theory of Markov Decision Processes.

Kozen defined the standard Boolean-typed calculus denotationally for the Mu-calculus; later Stirling gave it an operational interpretation as a turn-based game between two players, and showed that the two interpretations are equivalent.

In this talk I'll show how the same can be done for qMu so that the quantitative real-typed calculus corresponds to a two-player gambling game, thus providing a solid interface linking the logical and operational frameworks.