research-article

Open access

Fixpoint games on continuous lattices

Authors:

Barbara König,

Christina Mika-Michalski,

Tommaso PadoanAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 3, Issue POPL

Article No.: 26, Pages 1 - 29

https://doi.org/10.1145/3290339

Published: 02 January 2019 Publication History

Abstract

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 µ-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 µ-calculi.

Supplementary Material

WEBM File (a26-baldan.webm)

Download
92.31 MB

References

[1]

Samson Abramsky and Achim Jung. 1994. Domain Theory. In Handbook of Logic in Computer Science, Samson Abramsky, Dov Gabbay, and Thomas Stephen Edward Maibaum (Eds.). Oxford University Press, 1–168.

Digital Library

[2]

Shaull Almagor, Udi Boker, and Orna Kupferman. 2014. Discounting in LTL. In Proc. of TACAS ’14 (Lecture Notes in Computer Science), Vol. 8413. Springer, 424–439.

[3]

Paolo Baldan, Barbara König, Christina Mika-Michalski, and Tommaso Padoan. 2018. Fixpoint Games on Continuous Lattices. https://arxiv.org/abs/1810.11404 arXiv:1810.11404.

[4]

Harsh Beohar, Barbara König, Sebastian Küpper, and Alexandra Silva. 2017. Conditional Transition Systems with Upgrades. In Proc. of TASE ’17. IEEE Xplore, 1–8.

[5]

Filippo Bonchi, Pierre Ganty, Roberto Giacobazzi, and Dusko Pavlovic. 2018. Sound up-to techniques and Complete abstract domains. In Proc. of LICS ’18. ACM, 175–184.

Digital Library

[6]

Julian Bradfield and Igor Walukiewicz. 2018. The mu-Calculus and Model Checking. In Handbook of Model Checking, Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (Eds.). Springer, 871–919.

[7]

Anca Browne, Edmund M. Clarke, Somesh Jha, David E. Long, and Wilfredo R. Marrero. 1997. An improved algorithm for the evaluation of fixpoint expressions. Theoretical Computer Science 178, 1–2 (1997), 237–255.

Digital Library

[8]

Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. 2017. Deciding parity games in quasipolynomial time. In Proc. of STOC ’17. ACM, 252–263.

Digital Library

[9]

Rance Cleaveland. 1990. Tableau-based model checking in the propositional mu-calculus. Acta Informatica 27, 8 (1990), 725–747.

Digital Library

[10]

Rance Cleaveland, Marion Klein, and Bernhard Steffen. 1992. Faster model checking for the modal Mu-Calculus. In Proc. of CAV 1992 (Lecture Notes in Computer Science), Vol. 663. Springer, 410–422.

Digital Library

[11]

Maxime Cordy, Andreas Classen, Gilles Perrouin, Pierre-Yves Schobbens, Patrick Heymans, and Axel Legay. 2012. Simulationbased abstractions for software product-line model checking. In Proc. of ICSE ’12. IEEE, 672–682.

Digital Library

[12]

Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proc. of POPL ’77 (Los Angeles, California). ACM, 238–252.

Digital Library

[13]

Radhia Cousot and Patrick Cousot. 1979. Constructive versions of Tarski’s fixed point theorems. Pacific J. Math. 82, 1 (1979), 43–57.

[14]

Brian A. Davey and Hilary A. Priestley. 2002. Introduction to lattices and order. Cambridge University Press.

[15]

Giorgio Delzanno and Jean-François Raskin. 2000. Symbolic Representation of Upward-Closed Sets. In Proc. of TACAS ’00 (Lecture Notes in Computer Science), Susanne Graf and Michael I. Schwartzbach (Eds.), Vol. 1785. Springer, 426–440.

Digital Library

[16]

Pantelis E. Eleftheriou, Costas D. Koutras, and Christos Nomikos. 2012. Notions of bisimulation for Heyting-valued modal languages. Journal of Logic and Computation 22 (2012), 213–235.

Digital Library

[17]

E. Allen Emerson. 1985. Automata, tableaux, and temporal logics. In Proceedings of Logics of Programs 1985 (Lecture Notes in Computer Science), R. Parikh (Ed.), Vol. 193. Springer, 79–88.

Digital Library

[18]

E. Allen Emerson and Charanjit S. Jutla. 1991. Tree automata, Mu-Calculus and determinacy. In Proc. of SFCS ’91. IEEE, 368–377.

Digital Library

[19]

Melvin Fitting. 1991. Many-valued modal logics. Fundamenta Informaticae 15 (1991), 235–254.

[20]

Gaëlle Fontaine. 2008. Continuous Fragment of the µ-Calculus. In Proc. of CSL ’08 (Lecture Notes in Computer Science), Vol. 5213. Springer, 139–153.

Digital Library

[21]

Thomas Martin Gawlitza and Helmut Seidl. 2011. Solving systems of rational equations through strategy iteration. ACM Trans. Program. Lang. Syst. 33, 3 (2011), 11:1–11:48.

Digital Library

[22]

Gerhard Gierz, Karl H. Hofmann, Klaus Keimel, Jimmie D. Lawson, Michael W. Mislove, and Dana S. Scott. 2003. Continuous Lattices and Domains. Cambridge University Press.

[23]

Orna Grumberg, Martin Lange, Martin Leucker, and Sharon Shoham. 2005. Don’t Know in the µ-Calculus. In Proc. of VMCAI ’05 (Lecture Notes in Computer Science), Radhia Cousot (Ed.), Vol. 3385. Springer, 233–249.

[24]

Helle Hvid Hansen, Clemens Kupke, Johannes Marti, and Yde Venema. 2017. Parity Games and Automata for Game Logic. In Proc. of DALI ’17 (Lecture Notes in Computer Science), Vol. 10669. Springer, 115–132.

[25]

Ichiro Hasuo, Shunsuke Shimizu, and Corina Cîrstea. 2016. Lattice-theoretic progress measures and coalgebraic model checking. In Proc. of POPL ’16. ACM, 718–732.

Digital Library

[26]

Daniel Hirschkoff. 1998. Automatically Proving Up To Bisimulation. In Proc. of MFCS ’98 Workshop on Concurrency (Electronic Notes in Theoretical Computer Science). Elsevier, 75–89.

[27]

Michael Huth and Marta Kwiatkowska. 1997. Quantitative analysis and model checking. In Proc. of LICS ’97. IEEE, 111–122.

Digital Library

[28]

Marcin Jurdziński. 2000. Small Progress Measures for Solving Parity Games. In Proc. of STACS ’00 (Lecture Notes in Computer Science), Vol. 1770. Springer, 290–301.

Digital Library

[29]

Dexter Kozen. 1983. Results on the Propositional µ-Calculus. Theoretical Computer Science 27, 3 (1983), 333–354.

[30]

Orna Kupfermann and Yoad Lustig. 2007. Latticed Simulation Relations and Games. In Proc. of ATVA ’07 (Lecture Notes in Computer Science), Vol. 4672. Springer, 316–330.

Digital Library

[31]

Angelika Mader. 1997. Verification of Modal Properties Using Boolean Equation Systems. Ph.D. Dissertation. TU München.

[32]

Annabelle McIver and Carroll Morgan. 2007. Results on the quantitative µ-calculus qMµ. ACM Trans. Comp. Log. 8, 1:3 (2007), 43.

Digital Library

[33]

Matteo Mio. 2012. On the Equivalence of Game and Denotational Semantics for the Probabilistic µ-Calculus. Logical Methods in Computer Science 8, 2:07 (2012), 1–21.

[34]

Matteo Mio and Alex Simpson. 2015. Łukasiewicz µ-calculus. https://arxiv.org/abs/1510.00797 arXiv:1510.00797.

[35]

Matteo Mio and Alex Simpson. 2017. Łukasiewicz µ-calculus. Fundamenta Informaticae 150, 3-4 (2017), 317–346.

[36]

Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. 1999. Principles of Program Analysis. Springer.

Digital Library

[37]

Katja Poltermann. 2017. A Modal Logic for Conditional Transition Systems. Bachelor’s thesis. Universität Duisburg-Essen.

[38]

Damien Pous and Davide Sangiorgi. 2011. Enhancements of the bisimulation proof method. In Advanced Topics in Bisimulation and Coinduction, Davide Sangiorgi and Jan Rutten (Eds.). Cambridge University Press.

[39]

Davide Sangiorgi. 2011. Introduction to Bisimulation and Coinduction. Cambridge University Press.

[40]

Klaus Schneider. 2004. Verification of Reactive Systems: Formal Methods and Algorithms. Springer.

Digital Library

[41]

Dana Scott. 1972. Continuous lattices. In Toposes, Algebraic Geometry and Logic (Lecture Notes in Mathematics), F. W. Lawvere (Ed.). Springer, 97–136.

[42]

Helmut Seidl. 1996. Fast and simple nested fixpoints. Inform. Process. Lett. 59, 6 (1996), 303–308.

Digital Library

[43]

Perdita Stevens and Colin Stirling. 1998. Practical Model-Checking Using Games. In Proc. of TACAS ’98 (Lecture Notes in Computer Science), Vol. 1384. Springer, 85–101.

Digital Library

[44]

Colin Stirling. 1995. Local Model Checking Games. In Proc. of CONCUR ’95 (Lecture Notes in Computer Science), Vol. 962. Springer, 1–11.

Digital Library

[45]

Colin Stirling and David Walker. 1991. Local Model Checking in the Modal mu-Calculus. Theoretical Computer Science 89, 1 (1991), 161–177.

Digital Library

[46]

Alfred Tarski. 1955. A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5 (1955), 285–309.

[47]

Franck van Breugel and James Worrell. 2005. A behavioural pseudometric for probabilistic transition systems. Theoretical Computer Science 331 (2005), 115–142.

Digital Library

[48]

Yde Venema. 2008. Lectures on the modal µ-calculus. Lecture notes, Institute for Logic, Language and Computation, University of Amsterdam.

[49]

Wieslaw Zielonka. 1998. Infinite Games on Finitely Coloured Graphs with Applications to Automata on Infinite Trees. Theoretical Computer Science 200, 1-2 (1998), 135–183.

Digital Library

Cited By

Baldan PKönig BPadoan T(2024)Systems of Fixpoint Equations: Abstraction, Games, Up-To Techniques and Local AlgorithmsInformation and Computation10.1016/j.ic.2024.105233(105233)Online publication date: Oct-2024
https://doi.org/10.1016/j.ic.2024.105233
Hausmann DLehaut MPiterman N(2024)Symbolic Solution of Emerson-Lei Games for Reactive SynthesisFoundations of Software Science and Computation Structures10.1007/978-3-031-57228-9_4(55-78)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57228-9_4
Hausmann DPiterman NSağlam ISchmuck A(2024)Fair -Regular GamesFoundations of Software Science and Computation Structures10.1007/978-3-031-57228-9_2(13-33)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57228-9_2
Show More Cited By

Index Terms

Fixpoint games on continuous lattices
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
      1. Semantics
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Automated static analysis
        Model checking
2. Theory of computation
  1. Logic

Recommendations

Continuous lattices in formal concept analysis
Abstract
We introduce the notions of augmented formal contexts and generalized approximable concepts and show that all the generalized approximable concepts of an augmented formal context generates a continuous lattice under inclusion order, on the ...
On Subset Families That Form a Continuous Lattice

It is well known that continuous lattices and algebraic lattices can be respectively represented by the family of all fixed points of the projection operator and the closure operator preserving sups of directed sets on the power set of a set X. Similar ...
Integrally Closed Residuated Lattices
Abstract
A residuated lattice is said to be integrally closed if it satisfies the quasiequations $x y \leq x \Rightarrow y \leq e$ and $y x \leq x \Rightarrow y \leq e$ , or equivalently, the equations $x \ x \approx e$ and $x / x \approx e$ . Every integral, cancellative, or divisible residuated lattice is integrally closed,...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 3, Issue POPL

January 2019

2275 pages

EISSN:2475-1421

DOI:10.1145/3302515

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 02 January 2019

Published in PACMPL Volume 3, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
898
Total Downloads

Downloads (Last 12 months)135
Downloads (Last 6 weeks)16

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Baldan PKönig BPadoan T(2024)Systems of Fixpoint Equations: Abstraction, Games, Up-To Techniques and Local AlgorithmsInformation and Computation10.1016/j.ic.2024.105233(105233)Online publication date: Oct-2024
https://doi.org/10.1016/j.ic.2024.105233
Hausmann DLehaut MPiterman N(2024)Symbolic Solution of Emerson-Lei Games for Reactive SynthesisFoundations of Software Science and Computation Structures10.1007/978-3-031-57228-9_4(55-78)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57228-9_4
Hausmann DPiterman NSağlam ISchmuck A(2024)Fair -Regular GamesFoundations of Software Science and Computation Structures10.1007/978-3-031-57228-9_2(13-33)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57228-9_2
Komorida YKatsumata SHu NKlin BHumeau SEberhart CHasuo I(2022)Codensity Games for BisimilarityNew Generation Computing10.1007/s00354-022-00186-y40:2(403-465)Online publication date: 3-Aug-2022
https://dl.acm.org/doi/10.1007/s00354-022-00186-y
Jurdziński MMorvan RThejaswini K(2022)Universal Algorithms for Parity Games and Nested FixpointsPrinciples of Systems Design10.1007/978-3-031-22337-2_12(252-271)Online publication date: 29-Dec-2022
https://doi.org/10.1007/978-3-031-22337-2_12
Hausmann DSchröder L(2021)Quasipolynomial Computation of Nested FixpointsTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-72016-2_3(38-56)Online publication date: 20-Mar-2021
https://doi.org/10.1007/978-3-030-72016-2_3
Enevoldsen SJensen MLarsen KMariegaard ASrba J(2021)Verification of Multiplayer Stochastic Games via Abstract Dependency GraphsLogic-Based Program Synthesis and Transformation10.1007/978-3-030-68446-4_13(249-268)Online publication date: 13-Feb-2021
https://doi.org/10.1007/978-3-030-68446-4_13
Ivanov DSchupp SGnesi SPlat NDay NRossi M(2019)Static analysis for worst-case battery utilizationProceedings of the 7th International Workshop on Formal Methods in Software Engineering10.1109/FormaliSE.2019.00009(1-10)Online publication date: 27-May-2019
https://dl.acm.org/doi/10.1109/FormaliSE.2019.00009

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents