2026-09-08T02:22:06Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26570 2026-09-05T19:48:10Z ddc:004 open_access

Witnesses for Fixpoint Games on Lattices König, Barbara Messing, Karla fixpoint games lattice theory witnesses bisimilarity Galois connections Hennessy-Milner theorem distinguishing formulas behavioural metrics 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Barbara König and Karla Messing 2026 Is Part Of LIPIcs, Volume 374, 53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2026.182 urn:nbn:de:0030-drops-265709 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2026.182 eng https://creativecommons.org/licenses/by/4.0/legalcode