Memoryless strategies for stochastic games via domain theory

In Formal Methods we use mathematical structures to model real systems we want to build, or to reason about; in this paper we are concerned principally with game-based models. In an earlier work [Morgan, C. and A. McIver, Cost analysis of games using program logic, in: Proc. of the 8th Asia-Pacific Software Engineering Conference (APSEC 2001), 2001, abstract only: full text available at [13, key MDP01].] we presented an approach to stochastic minimising games based on our logic for probabilistic programs [Morgan, C., A. McIver and K. Seidel, Probabilistic predicate transformers, ACM Transactions on Programming Languages and Systems 18 (1996) 325-53, doi.acm.org/10.1145/229542.229547, McIver, A. and C. Morgan, Abstraction, Refinement and Proof for Probabilistic Systems, Technical Monographs in Computer Science, Springer Verlag, New York, 2004]. The contribution here is to extend our logical approach to maximising games. That maximising and minimising are not (simply) duals is due to the use of least fixed-points in both cases, as is normal for iterating programs. (For duality, we would have to use greatest fixed-points in the maximising case.) The significance of that extension is that it makes a further link between the program-logical approach and the more general methods for finding control strategies that "solve" games of this kind, in the sense of giving the player a "recipe" which, if followed, will deliver the theoretically optimal result.