文章基本信息

标题：Abstraction, Up-To Techniques and Games for Systems of Fixpoint Equations
本地全文：下载
作者：Paolo Baldan ; Barbara K{"o}nig ; Tommaso Padoan 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2020
卷号：171
页码：25:1-25:20
DOI：10.4230/LIPIcs.CONCUR.2020.25
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：fixpoint equation systems; complete lattices; parity games; abstract interpretation; up-to techniques; Î¼-calculus; bisimilarity