Location via proxy:   [ UP ]  
[Report a bug]   [Manage cookies]                
Document Open Access Logo

Abstraction, Up-To Techniques and Games for Systems of Fixpoint Equations

Authors Paolo Baldan , Barbara König , Tommaso Padoan

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.25.pdf
  • Filesize: 0.61 MB
  • 20 pages

Document Identifiers

Author Details

Paolo Baldan
  • Università Padova, Italy
Barbara König
  • Universität Duisburg-Essen, Germany
Tommaso Padoan
  • Università di Padova, Italy

Funding

Supported by the PRIN Project Analysis of Program Analyses (ASPRA), the University of Padova project ASTA and the DFG projects BEMEGA and SpeQt.

Cite AsGet BibTex

Paolo Baldan, Barbara König, and Tommaso Padoan. Abstraction, Up-To Techniques and Games for Systems of Fixpoint Equations. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 25:1-25:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CONCUR.2020.25

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
  • Software and its engineering → Model checking
Keywords
  • fixpoint equation systems
  • complete lattices
  • parity games
  • abstract interpretation
  • up-to techniques
  • μ-calculus
  • bisimilarity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Samson Abramsky and Achim Jung. Domain theory. In Samson Abramsky, Dov Gabbay, and Thomas Stephen Edward Maibaum, editors, Handbook of Logic in Computer Science, pages 1-168. Oxford University Press, 1994. Google Scholar
  2. Paolo Baldan, Barbara König, Christina Mika-Michalski, and Tommaso Padoan. Fixpoint games in continuous lattices. In Stephanie Weirich, editor, Proc. of POPL'19, volume 3, pages 26:1-26:29. ACM, 2019. Google Scholar
  3. Paolo Baldan, Barbara König, and Tommaso Padoan. Abstraction, up-to techniques and games for systems of fixpoint equations, 2020. URL: http://arxiv.org/abs/2003.08877.
  4. Gourinath Banda and John P. Gallagher. Constraint-based abstract semantics for temporal logic: A direct approach to design and implementation. In Edmund M. Clarke and Andrei Voronkov, editors, LPAR 2010, volume 6355 of Lecture Notes in Computer Science, pages 27-45. Springer, 2010. Google Scholar
  5. Andrea Bianco and Luca de Alfaro. Model checking of probabalistic and nondeterministic systems. In Proc. of FSTTCS '95, volume 1026 of Lecture Notes in Computer Science, pages 499-513. Springer, 1995. Google Scholar
  6. Filippo Bonchi, Pierre Ganty, Roberto Giacobazzi, and Dusko Pavlovic. Sound up-to techniques and complete abstract domains. In Proc. of LICS '18, pages 175-184. ACM, 2018. Google Scholar
  7. Filippo Bonchi, Barbara König, and Daniela Petrişan. Up-to techniques for behavioural metrics via fibrations. In Proc. of CONCUR '18, volume 118 of LIPIcs, pages 17:1-17:17. Schloss Dagstuhl - Leibniz Center for Informatics, 2018. Google Scholar
  8. Filippo Bonchi and Damien Pous. Checking NFA equivalence with bisimulations up to congruence. In Proc. of POPL '13, pages 457-468. ACM, 2013. Google Scholar
  9. Julian Bradfield and Igor Walukiewicz. The mu-calculus and model checking. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 871-919. Springer, 2018. Google Scholar
  10. Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasipolynomial time. In Proc. of STOC '17, pages 252-263. ACM, 2017. Google Scholar
  11. Rance Cleaveland, Marion Klein, and Bernhard Steffen. Faster model checking for the modal mu-calculus. In Proc. of CAV 1992, volume 663 of Lecture Notes in Computer Science, pages 410-422. Springer, 1992. Google Scholar
  12. Patrick Cousot. Partial completeness of abstract fixpoint checking. In Berthe Y. Choueiry and Toby Walsh, editors, Proceedings of the Fourth International Symposium on Abstraction, Reformulations and Approximation, SARA'2000, volume 1864 of Lecture Notes in Computer Science, pages 1-25. Springer, 26-29 July 2000. Google Scholar
  13. Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. of POPL '77, pages 238-252. ACM, 1977. Google Scholar
  14. Patrick Cousot and Radhia Cousot. Systematic design of program analysis frameworks. In Proc. of POPL '79, pages 269-282. ACM, 1979. Google Scholar
  15. Patrick Cousot and Radhia Cousot. Temporal abstract interpretation. In Mark N. Wegman and Thomas W. Reps, editors, Proc. of POPL '00, pages 12-25. ACM, 2000. Google Scholar
  16. Radhia Cousot and Patrick Cousot. Constructive versions of tarski’s fixed point theorems. Pacific Journal of Mathematics, 82(1):43-57, 1979. Google Scholar
  17. Dennis Dams, Rob Gerth, and Orna Grumberg. Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst., 19(2):253-291, 1997. Google Scholar
  18. Roberto Giacobazzi, Francesco Ranzato, and Francesca Scozzari. Making abstract interpretations complete. Journal of the ACM, 47(2):361-416, 2000. Google Scholar
  19. Orna Grumberg, Martin Lange, Martin Leucker, and Sharon Shoham. When not losing is better than winning: Abstraction and refinement for the full mu-calculus. Information and Computation, 205(8):1130-1148, 2007. Google Scholar
  20. Ichiro Hasuo, Shunsuke Shimizu, and Corina Cîrstea. Lattice-theoretic progress measures and coalgebraic model checking. In Proc. of POPL '16, pages 718-732. ACM, 2016. Google Scholar
  21. Daniel Hirschkoff. Automatically proving up to bisimulation. In Proc. of MFCS '98 Workshop on Concurrency, number 18 in Electronic Notes in Theoretical Computer Science, pages 75-89. Elsevier, 1998. Google Scholar
  22. Daniel Hirschkoff. Mise en oeuvre de preuves de bisimulation. PhD thesis, Ecole Nationale des Ponts et Chaussées, 1999. Google Scholar
  23. Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. The power of parameterization in coinductive proof. In Proc. of POPL '13, pages 193-206. ACM, 2013. Google Scholar
  24. Michael Huth and Marta Kwiatkowska. Quantitative analysis and model checking. In Proc. of LICS '97, pages 111-122. IEEE, 1997. Google Scholar
  25. Marcin Jurdziński. Small progress measures for solving parity games. In Proc. of STACS '00, volume 1770 of Lecture Notes in Computer Science, pages 290-301. Springer, 2000. Google Scholar
  26. Marcin Jurdzinski and Ranko Lazic. Succinct progress measures for solving parity games. In Proc. of LICS '17, pages 1-9. ACM/IEEE, 2017. Google Scholar
  27. Dexter Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27(3):333-354, 1983. Google Scholar
  28. Kim Guldstrand Larsen and Bent Thomsen. A modal process logic. In Proc. of LICS '88, pages 203-210. IEEE, 1988. Google Scholar
  29. Karoliina Lehtinen. A modal μ perspective on solving parity games in quasi-polynomial time. In Proc. of LICS '18, pages 639-648. ACM/IEEE, 2018. Google Scholar
  30. Claire Loiseaux, Susanne Graf, Joseph Sifakis, Ahmed Bouajjani, and Saddek Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6:1-35, 1995. Google Scholar
  31. Annabelle McIver and Carroll Morgan. Results on the quantitative μ-calculus qmμ. ACM Trans. Comp. Log., 8(1:3), 2007. Google Scholar
  32. Robin Milner. Communication and Concurrency. Prentice Hall, 1989. Google Scholar
  33. Antoine Miné. Tutorial on static inference of numeric invariants by abstract interpretation. Foundations and Trends in Programming Languages, 4(3-4):120-372, 2017. Google Scholar
  34. Matteo Mio and Alex Simpson. Łukasiewicz μ-calculus. Fundamenta Informaticae, 150(3-4):317-346, 2017. Google Scholar
  35. Damien Pous. Complete lattices and up-to techniques. In Proc. of APLAS '07, pages 351-366. Springer, 2007. LNCS 4807. Google Scholar
  36. Damien Pous. Coinduction all the way up. In Proc. of LICS'16, pages 307-316. ACM, 2016. Google Scholar
  37. Damien Pous and Davide Sangiorgi. Enhancements of the bisimulation proof method. In Davide Sangiorgi and Jan Rutten, editors, Advanced Topics in Bisimulation and Coinduction. Cambridge University Press, 2011. Google Scholar
  38. Davide Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge University Press, 2011. Google Scholar
  39. Davide Sangiorgi and Robin Milner. The problem of "weak bisimulation up to". In W.R. Cleaveland, editor, Proc. of CONCUR'92, pages 32-46. Springer, 1992. Google Scholar
  40. David A. Schmidt. Binary relations for abstraction and refinement. In Workshop on Refinement and Abstraction. Elsevier Electronic, 2000. Google Scholar
  41. Dana Scott. Continuous lattices. In F. W. Lawvere, editor, Toposes, Algebraic Geometry and Logic, Lecture Notes in Mathematics, pages 97-136. Springer, 1972. Google Scholar
  42. Helmut Seidl. Fast and simple nested fixpoints. Information Processing Letters, 59(6):303-308, 1996. Google Scholar
  43. David Sprunger and Lawrence S. Moss. Precongruences and parametrized coinduction for logics for behavioral equivalence. In Proc. of CALCO '17, volume 72 of LIPIcs, pages 23:1-23:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. Google Scholar
  44. Perdita Stevens and Colin Stirling. Practical model-checking using games. In Proc. of TACAS '98, volume 1384 of Lecture Notes in Computer Science, pages 85-101. Springer, 1998. Google Scholar
  45. Colin Stirling. Local model checking games. In Proc. of CONCUR '95, volume 962 of Lecture Notes in Computer Science, pages 1-11. Springer, 1995. Google Scholar
  46. Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285-309, 1955. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact