The mu-calculus is a powerful tool for specifying and verifying transition systems, including those with both demonic (universal) and angelic (existential) choice; its quantitative generalization qM mu extends to include probabilistic choice. We make two major contributions to the theory of such systems. The first is to show that for a finite-state system, the logical interpretation of qM mu, via fixed points in a domain of real-valued functions into [0, 1], is equivalent to an operational interpretation given as a turn-based gambling game between two players. The second contribution is to show that each player in the gambling game has an optimal memoryless strategy - that is, a strategy which is independent of the game`s history, and with which a player can achieve his optimal expected reward however his opponent chooses to play. Moreover, since qM mu is expressive enough to encode stochastic parity games, our result implies the existence of memoryless strategies in that framework, as well. As an additional feature, we include an extensive case study demonstrating the aforementioned duality between games and logic. Among other things, it shows that the use of algorithmic verification techniques is mathematically justified in the practical computation of probabilistic system properties.

We develop a general testing scenario for probabilistic processes, giving rise to two theories: probabilistic may testing and probabilistic must testing. These are applied to a simple probabilistic version of the process calculus CSP. We examine the algebraic theory of probabilistic testing, and show that many of the axioms of standard testing are no longer valid in our probabilistic setting; even for non-probabilistic CSP processes, the distinguishing power of probabilistic tests is much greater than that of standard tests. We develop a method for deriving inequations valid in probabilistic may testing based on a probabilistic extension of the notion of simulation. Using this, we obtain a complete axiomatisation for non-probabilistic processes subject to probabilistic may testing. © 2007 Elsevier B.V. All rights reserved.

We describe pKA, a probabilistic Kleene-style algebra, based on a well known model of probabilistic/demonic computation [3,16,10]. Our technical aim is to express probabilistic versions of Cohen`s separation theorems[1]. Separation theorems simplify reasoning about distributed systems, where with purely algebraic reasoning they can reduce complicated interleaving behaviour to, `separated` behaviours each of which can be analysed on its own. Until now that has not been possible for probabilistic distributed systems. Algebraic reasoning in general is very robust, and easy to check: thus an algebraic approach to probabilistic distributed systems is attractive because in that `doubly hostile` environment (probability and interleaving) the opportunities for subtle error abound. Especially tricky is the interaction of probability and the demonic or `adversarial` scheduling implied by concurrency. Our case study - based on Rabin`s Mutual exclusion with bounded waiting [6] - is one where just such problems have already occurred: the original presentation was later shown to have subtle flaws [15]. It motivates our interest in algebras, where assumptions relating probability and secrecy are clearly exposed and, in some cases, can be given simple characterisations in spite of their intricacy.