Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Fixpoint Theory -- Upside Down

Paolo Baldan, Richard Eggert, Barbara König, Tommaso Padoan

TL;DR

The paper develops a finitary, approximation-based framework for certifying both greatest and least fixpoints of monotone, non-expansive endomaps on lattices of the form $\mathbb{M}^Y$, with $Y$ finite and $\mathbb{M}$ an MV-chain. By constructing and composing $a$- and $\# $-type approximations (via adjoints $\alpha_{a,\delta}, \gamma_{a,\delta}$) on the finite cube $\mathbf{2}^Y$, it provides sound and complete proof rules that move from a fixpoint candidate to the true fixpoint using finite-space reasoning. The approach unifies and extends witnesses for termination probabilities, behavioural metrics and bisimilarity, and yields original algorithmic techniques for simple stochastic games, including strategy-iteration variants backed by linear programs. The results offer a modular, scalable toolkit for reasoning about complex probabilistic and metric systems in a lattice-theoretic setting, with potential extensions to infinite domains and richer algebraic structures.

Abstract

Knaster-Tarski's theorem, characterising the greatest fixpoint of a monotone function over a complete lattice as the largest post-fixpoint, naturally leads to the so-called coinduction proof principle for showing that some element is below the greatest fixpoint (e.g., for providing bisimilarity witnesses). The dual principle, used for showing that an element is above the least fixpoint, is related to inductive invariants. In this paper we provide proof rules which are similar in spirit but for showing that an element is above the greatest fixpoint or, dually, below the least fixpoint. The theory is developed for non-expansive monotone functions on suitable lattices of the form $\mathbb{M}^Y$, where $Y$ is a finite set and $\mathbb{M}$ an MV-algebra, and it is based on the construction of (finitary) approximations of the original functions. We show that our theory applies to a wide range of examples, including termination probabilities, metric transition systems, behavioural distances for probabilistic automata and bisimilarity. Moreover it allows us to determine original algorithms for solving simple stochastic games.

Fixpoint Theory -- Upside Down

TL;DR

The paper develops a finitary, approximation-based framework for certifying both greatest and least fixpoints of monotone, non-expansive endomaps on lattices of the form , with finite and an MV-chain. By constructing and composing - and -type approximations (via adjoints ) on the finite cube , it provides sound and complete proof rules that move from a fixpoint candidate to the true fixpoint using finite-space reasoning. The approach unifies and extends witnesses for termination probabilities, behavioural metrics and bisimilarity, and yields original algorithmic techniques for simple stochastic games, including strategy-iteration variants backed by linear programs. The results offer a modular, scalable toolkit for reasoning about complex probabilistic and metric systems in a lattice-theoretic setting, with potential extensions to infinite domains and richer algebraic structures.

Abstract

Knaster-Tarski's theorem, characterising the greatest fixpoint of a monotone function over a complete lattice as the largest post-fixpoint, naturally leads to the so-called coinduction proof principle for showing that some element is below the greatest fixpoint (e.g., for providing bisimilarity witnesses). The dual principle, used for showing that an element is above the least fixpoint, is related to inductive invariants. In this paper we provide proof rules which are similar in spirit but for showing that an element is above the greatest fixpoint or, dually, below the least fixpoint. The theory is developed for non-expansive monotone functions on suitable lattices of the form , where is a finite set and an MV-algebra, and it is based on the construction of (finitary) approximations of the original functions. We show that our theory applies to a wide range of examples, including termination probabilities, metric transition systems, behavioural distances for probabilistic automata and bisimilarity. Moreover it allows us to determine original algorithms for solving simple stochastic games.

Paper Structure

This paper contains 21 sections, 17 theorems, 92 equations, 3 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Lattices and MV-algebras
  3. Non-expansive functions and their approximations
  4. Non-expansive functions on MV-algebras.
  5. Approximating the propagation of increases.
  6. Proof rules
  7. Proof rules for fixpoints
  8. Proof rules for pre-fixpoints
  9. The dual view for least fixpoints
  10. (De)Composing functions and approximations
  11. Applications
  12. Termination probability
  13. Behavioural metrics for probabilistic automata and metric transition systems
  14. Comparison with bblmtv:prob-bisim-distance-automata
  15. Branching Distances for Metric Transition Systems
  16. ...and 6 more sections

Key Result

lemma 1

Let $\mathbb{M}$ is an MV-chain and let $Y, Z$ be finite sets. Every non-expansive function $f: \mathbb{M}^Y\to \mathbb{M}^Z$ is monotone.

Figures (3)

  • Figure 1: Function $\mathcal{T}$ (left) and a Markov chain with two fixpoints of $\mathcal{T}$ (right)
  • Figure 2: Visual representation of $\alpha_{a,\delta}$ and $\gamma_{a,\delta}$
  • Figure 3: Strategy iteration from above and below

Theorems & Definitions (79)

  • Definition 2.1: MV-algebra
  • Definition 2.2: natural order
  • Example 2.3
  • proof
  • Definition 3.1: norm
  • proof
  • Definition 3.2: non-expansiveness
  • lemma 1: non-expansiveness implies monotonicity
  • proof
  • lemma 2: characterisation of non-expansiveness
  • ...and 69 more