Witnesses for Fixpoint Games on Lattices

TL;DR

This paper introduces a lattice-theoretical framework for constructing witnesses in fixpoint games, enabling strategy derivation and bounds verification across various systems including probabilistic models.

Contribution

It develops a novel approach using Galois connections to connect logic and behavior lattices, applicable to primal and dual games, with practical case studies.

Findings

Constructed witnesses for fixpoint games in lattices

Derived strategies from witnesses in primal and dual games

Applied theory to probabilistic systems and Markov chains

Abstract

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.