01:34:11
published on April 22, 2024
Coq/Rocq tutorial: Ssreflect tactics and the MathComp library
By Marie Kerjean
Fixpoint games
Appears in collection : 19th International Conference on Relational and Algebraic Methods in Computer Science / 19ème Conférence internationale de méthodes relationnelles et algébriques en informatique
Solving fixpoint equations is a recurring problem in several domains: the result of a dataflow analysis can be characterized as either a least or greatest fixpoint. It is well-known that bisimilarity - the largest bisimulation - admits a characterization as a greatest fixpoint and furthermore mu-calculus model-checking requires to solve systems of nested fixpoint equations. Often, these fixpoint equations or equation systems are defined over powerset lattices, however in several applications - such as lattice-valued or real-valued mu-calculi - the lattice under consideration is not a powerset. Hence we extend the notion of fixpoint games (or unfolding games, introduced by Venema) to games for equation systems over more general lattices. In particular continuous lattices admit a very elegant characterization of the solution. We will also describe how to define progress measures which describe winning strategies for the existential players and explain how abstractions and up-to functions can be integrated into the framework. (Joint work with Paolo Baldan, Tommaso Padoan, Christina Mika-Michalski) .
