Fixpoint Theory -- Upside Down

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

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

Publication date: 26 August 2023

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

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.

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The complexity of stochastic games
• Computational Optimal Transport: With Applications to Data Science
• Optimal Transport
• A lattice-theoretical fixpoint theorem and its applications
• Algebraic laws for nondeterminism and concurrency
• Advanced Łukasiewicz calculus and MV-algebras
• Introduction to Bisimulation and Coinduction
• On Nonterminating Stochastic Games
• Gromov-Wasserstein distances and the metric approach to object matching
• Making abstract interpretations complete
• Bisimulation, modal logic and model checking games
• Combinatorial structure and randomized subexponential algorithms for infinite games
• Complete Lattices and Up-To Techniques
• On strategy improvement algorithms for simple stochastic games
• The quantitative linear-time-branching-time spectrum
• Computing Game Metrics on Markov Decision Processes
• Value iteration for simple stochastic games: stopping criterion and learning algorithm

Recommendations

• Fixed Point Theory 👍 👎
• Fixed points and alternative principles 👍 👎
• Fixpoint theory -- upside down 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎

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)