Fixpoint Theory -- Upside Down

DOI10.46298/LMCS-19(2:15)2023OpenAlexW4379800149MaRDI QIDQ6135764FDOQ6135764

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

Publication date 26 August 2023

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2101.08184

zbMATH Keywords

stochastic gamesMV-algebrasbisimilarityfixpointsKnaster-Tarski theoremnon-expansive functions

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

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 $mathbbM$ 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.

Recommendations

• Fixpoint theory -- upside down
• Publication:3479078
• scientific article; zbMATH DE number 1210271
• Publication:4946179
• scientific article; zbMATH DE number 1973375
• Fixed point theory
• scientific article; zbMATH DE number 5530321
• Publication:4206923
• scientific article; zbMATH DE number 7606925
• Fixed points and alternative principles

Cites work

• scientific article; zbMATH DE number 177532 (Why is no real title available?)
• scientific article; zbMATH DE number 1324833 (Why is no real title available?)
• scientific article; zbMATH DE number 549853 (Why is no real title available?)
• scientific article; zbMATH DE number 7559481 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• scientific article; zbMATH DE number 7649917 (Why is no real title available?)
• A generic strategy improvement method for simple stochastic games
• A lattice-theoretical fixpoint theorem and its applications
• Advanced Łukasiewicz calculus and MV-algebras
• Algebraic laws for nondeterminism and concurrency
• Bisimulation, modal logic and model checking games
• Coalgebraic behavioral metrics
• Combinatorial structure and randomized subexponential algorithms for infinite games
• Complete Lattices and Up-To Techniques
• Computational optimal transport. With applications to data sciences
• Computing Game Metrics on Markov Decision Processes
• Gromov-Wasserstein distances and the metric approach to object matching
• Introduction to bisimulation and coinduction
• Making abstract interpretations complete
• On Nonterminating Stochastic Games
• On strategy improvement algorithms for simple stochastic games
• On-the-fly computation of bisimilarity distances
• Optimal Transport
• The complexity of stochastic games
• The quantitative linear-time-branching-time spectrum
• Value iteration for simple stochastic games: stopping criterion and learning algorithm

This page was built for publication: Fixpoint Theory -- Upside Down

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6135764)