Fixpoint Games on Continuous Lattices
Fixpoint Games on Continuous Lattices
复制标题
DOI：
10.1145/3290339
复制
发表时间：
2019-01-01
影响因子：
1.8
通讯作者：
Padoan, Tommaso
中科院分区：
文献类型：
--
作者：
Baldan, Paolo;Koenig, Barbara;Padoan, Tommaso
许多分析和验证任务，如静态程序分析和时间逻辑的模型检查，可以简化为在合适的格上求解方程组。受最近关于格理论进展措施的工作的启发，我们发展了一种解决格上单调方程组的博弈论方法，其中每个方程要么取最小解，要么取最大解。定义了一个简单的奇偶对策，称为不动点对策，它提供了连续格上方程组解的正确和完整的特征，连续格是语义中广泛使用的一类相当一般的格。对于幂集格，不动点对策与p-微积分模型检验的经典奇偶对策密切相关，其解可以作为关键工具利用Jurdzinski的小进步测度。我们展示了如何将进度度量的概念自然地推广到连续格上的固定点博弈，并证明了小进度度量的存在。我们的结果导致了作为（最少）不动点的进度度量的建设性表述。我们通过引入选择的概念来完善这一特征，选择允许人们约束奇偶博弈中的玩法，从而实现博弈的有效（可能是有效的）解决方案，从而解决相关的验证问题。我们还提出了一种逻辑，用于指定存在玩家的移动，该逻辑可用于系统地推导简化方程，以有效地计算进度度量。讨论了在格形p-微积分模型检验中的潜在应用。
Many analysis and verifications tasks, such as static program analyses and model-checking for temporal logics, reduce to the solution of systems of equations over suitable lattices. Inspired by recent work on lattice-theoretic progress measures, we develop a game-theoretical approach to the solution of systems of monotone equations over lattices, where for each single equation either the least or greatest solution is taken. A simple parity game, referred to as fixpoint game, is defined that provides a correct and complete characterisation of the solution of systems of equations over continuous lattices, a quite general class of lattices widely used in semantics. For powerset lattices the fixpoint game is intimately connected with classical parity games for p-calculus model-checking, whose solution can exploit as a key tool Jurdzinski's small progress measures. We show how the notion of progress measure can be naturally generalised to fixpoint games over continuous lattices and we prove the existence of small progress measures. Our results lead to a constructive formulation of progress measures as (least) fixpoints. We refine this characterisation by introducing the notion of selection that allows one to constrain the plays in the parity game, enabling an effective (and possibly efficient) solution of the game, and thus of the associated verification problem. We also propose a logic for specifying the moves of the existential player that can be used to systematically derive simplified equations for efficiently computing progress measures. We discuss potential applications to the model-checking of latticed p-calculi.