Witnesses for Fixpoint Games on Lattices
This work provides a theoretical framework for certifying properties in formal verification, but it is incremental as it builds on existing lattice-theoretical approaches.
The paper tackles the problem of deriving strategies in fixpoint games on lattices by constructing witnesses that prove relationships between least fixpoints and given bounds, with applications in certifying lower bounds for termination probabilities in Markov chains.
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.