论文标题
fixpoint方程系统的抽象，最新技术和游戏
Abstraction, Up-to Techniques and Games for Systems of Fixpoint Equations
论文作者
论文摘要
FIXPOINT方程的系统在完整的晶格上，包括（混合）最少和最大的FIXPOINT方程组成，允许一个人表达许多验证任务，例如对各种规范逻辑的模型检查或检查共同感应性行为等效性的检查。 在本文中，我们开发了一种抽象解释方式的fixpoint方程系统的近似理论：某些混凝土域上的系统被抽象成合适的抽象域中的系统，并确保抽象解决方案代表混凝土解决方案的声音/完全过度应用。 有趣的是，最新技术是一种用于获得更容易或可行证据的共同设置中的经典方法，可以将它们自然地符合我们的框架并扩展到方程式系统的方式将其解释为抽象。 此外，依靠近似理论，我们可以根据适当的平价游戏来提供固定点方程系统的解决方案的特征，从而概括了一些最近的工作，这些工作仅限于连续的晶格。 游戏视图为开发即时算法的开发开辟了道理，以表征这种方程式系统的解决方案。
Systems of fixpoint equations over complete lattices, consisting of (mixed) least and greatest fixpoint equations, allow one to express a number of 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 in our framework and extend to systems of equations. Additionally, relying on the approximation theory, we can provide a characterisation of 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 to the development of on-the-fly algorithms for characterising the solution of such equation systems.
