Fixpoint Theory -- Upside Down
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...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2023-06-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/8382/pdf |
| _version_ | 1827174306327560192 |
|---|---|
| author | Paolo Baldan Richard Eggert Barbara König Tommaso Padoan |
| author_facet | Paolo Baldan Richard Eggert Barbara König Tommaso Padoan |
| author_sort | Paolo Baldan |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:32:46Z |
| format | Article |
| id | doaj.art-cb4cd745ba314618a150780a57398a3e |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2025-03-21T03:53:27Z |
| publishDate | 2023-06-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-cb4cd745ba314618a150780a57398a3e2024-07-30T09:03:12ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742023-06-01Volume 19, Issue 210.46298/lmcs-19(2:15)20238382Fixpoint Theory -- Upside DownPaolo Baldanhttps://orcid.org/0000-0001-9357-5599Richard Eggerthttps://orcid.org/0000-0002-9901-7392Barbara KönigTommaso Padoanhttps://orcid.org/0000-0001-7814-1485Knaster-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.https://lmcs.episciences.org/8382/pdfcomputer science - logic in computer science |
| spellingShingle | Paolo Baldan Richard Eggert Barbara König Tommaso Padoan Fixpoint Theory -- Upside Down Logical Methods in Computer Science computer science - logic in computer science |
| title | Fixpoint Theory -- Upside Down |
| title_full | Fixpoint Theory -- Upside Down |
| title_fullStr | Fixpoint Theory -- Upside Down |
| title_full_unstemmed | Fixpoint Theory -- Upside Down |
| title_short | Fixpoint Theory -- Upside Down |
| title_sort | fixpoint theory upside down |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/8382/pdf |
| work_keys_str_mv | AT paolobaldan fixpointtheoryupsidedown AT richardeggert fixpointtheoryupsidedown AT barbarakonig fixpointtheoryupsidedown AT tommasopadoan fixpointtheoryupsidedown |