Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Fri 18 Jan 2019 14:29 - 14:51 at Sala I - Semantics Chair(s): Noam Zeilberger

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 $\mu$-calculus model-checking, whose solution can exploit as a key tool Jurdziński’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 $\mu$-calculi.

Slides (talk-online.pdf)3.41MiB

Fri 18 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

13:45 - 14:51: SemanticsResearch Papers at Sala I
Chair(s): Noam ZeilbergerUniversity of Birmingham, UK
13:45 - 14:07
Better Late Than Never: A Fully Abstract Semantics for Classical Processes
Research Papers
Wen KokkeUniversity of Edinburgh, Fabrizio MontesiUniversity of Southern Denmark, Marco PeressottiUniversity of Southern Denmark
Link to publication DOI Media Attached
14:07 - 14:29
Diagrammatic Algebra: From Linear to Concurrent Systems
Research Papers
Filippo BonchiUniversity of Pisa, Joshua HollandUniversity of Southampton, Robin PiedeleuUniversity of Oxford, Pawel SobocinskiUniversity of Southampton, Fabio ZanasiUniversity College London
Link to publication DOI Media Attached
14:29 - 14:51
Fixpoint Games on Continuous Lattices
Research Papers
Paolo BaldanUniversity of Padova, Barbara KönigUniversity of Duisburg-Essen, Christina Mika-MichalskiUniversity of Duisburg-Essen, Tommaso PadoanUniversity of Padova
Link to publication DOI Media Attached File Attached