We construct witnesses that can be used to derive strategies in fixpoint games and provide proof that the least fixpoint of a function is either above or not below some given bound. We rely on a lattice-theoretical approach, including a Galois connection that connects a lattice representing the "logic universe", where the witness lives, with another lattice representing the "behaviour universe", over which the function is defined. In fact we consider two types of games -- primal and dual games -- and in both cases show how to derive winning strategies in the game from witnesses and construct witnesses from strategies. The two games differ wrt. their rules and the choice of basis of the lattice. The theory can be instantiated to well-known examples: in particular we compare with the construction of distinguishing formulas in standard bisimilarity and behavioural metrics for probabilistic systems. As a new case study we consider witnesses for certifying lower bounds for the termination probability for Markov chains.

翻译：暂无翻译