License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2020.25
URN: urn:nbn:de:0030-drops-128373
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12837/
Go to the corresponding LIPIcs Volume Portal

Baldan, Paolo ; König, Barbara ; Padoan, Tommaso

Abstraction, Up-To Techniques and Games for Systems of Fixpoint Equations

pdf-format:
LIPIcs-CONCUR-2020-25.pdf (0.6 MB)

Abstract

Systems of fixpoint equations over complete lattices, consisting of (mixed) least and greatest fixpoint equations, allow one to express many verification tasks such as model-checking of various kinds of specification logics or the check of coinductive behavioural equivalences. In this paper we develop a theory of approximation for systems of fixpoint equations in the style of abstract interpretation: a system over some concrete domain is abstracted to a system in a suitable abstract domain, with conditions ensuring that the abstract solution represents a sound/complete overapproximation of the concrete solution. Interestingly, up-to techniques, a classical approach used in coinductive settings to obtain easier or feasible proofs, can be interpreted as abstractions in a way that they naturally fit into our framework and extend to systems of equations. Additionally, relying on the approximation theory, we can characterise the solution of systems of fixpoint equations over complete lattices in terms of a suitable parity game, generalising some recent work that was restricted to continuous lattices. The game view opens the way for the development of local algorithms for characterising the solution of such equation systems and we explore some special cases.

BibTeX - Entry

@InProceedings{baldan_et_al:LIPIcs:2020:12837,
  author =	{Paolo Baldan and Barbara K{\"o}nig and Tommaso Padoan},
  title =	{{Abstraction, Up-To Techniques and Games for Systems of Fixpoint Equations}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{25:1--25:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Igor Konnov and Laura Kov{\'a}cs},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12837},
  URN =		{urn:nbn:de:0030-drops-128373},
  doi =		{10.4230/LIPIcs.CONCUR.2020.25},
  annote =	{Keywords: fixpoint equation systems, complete lattices, parity games, abstract interpretation, up-to techniques, μ-calculus, bisimilarity}
}

Keywords: fixpoint equation systems, complete lattices, parity games, abstract interpretation, up-to techniques, μ-calculus, bisimilarity
Collection: 31st International Conference on Concurrency Theory (CONCUR 2020)
Issue Date: 2020
Date of publication: 26.08.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI