{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T07:10:38Z","timestamp":1760080238102,"version":"3.41.0"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["KO 2185\/7-2"],"award-info":[{"award-number":["KO 2185\/7-2"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100011703","name":"Universit\u00e0 degli Studi di Padova","doi-asserted-by":"publisher","award":["ASTA"],"award-info":[{"award-number":["ASTA"]}],"id":[{"id":"10.13039\/501100011703","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats: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 \u00b5-calculus model-checking, whose solution can exploit as a key tool Jurdzi\u0144ski\u2019s 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 \u00b5-calculi.<\/jats:p>","DOI":"10.1145\/3290339","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Fixpoint games on continuous lattices"],"prefix":"10.1145","volume":"3","author":[{"given":"Paolo","family":"Baldan","sequence":"first","affiliation":[{"name":"University of Padua, Italy"}]},{"given":"Barbara","family":"K\u00f6nig","sequence":"additional","affiliation":[{"name":"University of Duisburg-Essen, Germany"}]},{"given":"Christina","family":"Mika-Michalski","sequence":"additional","affiliation":[{"name":"University of Duisburg-Essen, Germany"}]},{"given":"Tommaso","family":"Padoan","sequence":"additional","affiliation":[{"name":"University of Padua, Italy"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"volume-title":"Handbook of Logic in Computer Science","author":"Abramsky Samson","key":"e_1_2_2_1_1"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_37"},{"key":"e_1_2_2_3_1","unstructured":"Paolo Baldan Barbara K\u00f6nig Christina Mika-Michalski and Tommaso Padoan. 2018. Fixpoint Games on Continuous Lattices. https:\/\/arxiv.org\/abs\/1810.11404 arXiv:1810.11404.  Paolo Baldan Barbara K\u00f6nig Christina Mika-Michalski and Tommaso Padoan. 2018. Fixpoint Games on Continuous Lattices. https:\/\/arxiv.org\/abs\/1810.11404 arXiv:1810.11404."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2017.8285624"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209169"},{"volume-title":"Handbook of Model Checking, Edmund M","author":"Bradfield Julian","key":"e_1_2_2_6_1"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00228-9"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3055399.3055409"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264284"},{"key":"e_1_2_2_10_1","volume-title":"Proc. of CAV 1992 (Lecture Notes in Computer Science)","volume":"663","author":"Cleaveland Rance","year":"1992"},{"volume-title":"Proc. of ICSE \u201912","year":"2012","author":"Cordy Maxime","key":"e_1_2_2_11_1"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1979.82.43"},{"volume-title":"Priestley","year":"2002","author":"Davey Brian A.","key":"e_1_2_2_14_1"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/646484.691759"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exq005"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/648065.747611"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1991.185392"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/161288.161295"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87531-4_12"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1961204.1961207"},{"volume-title":"Scott","year":"2003","author":"Gierz Gerhard","key":"e_1_2_2_22_1"},{"key":"e_1_2_2_23_1","volume-title":"Proc. of VMCAI \u201905 (Lecture Notes in Computer Science), Radhia Cousot (Ed.)","volume":"3385","author":"Grumberg Orna","year":"2005"},{"key":"e_1_2_2_24_1","volume-title":"Proc. of DALI \u201917 (Lecture Notes in Computer Science)","volume":"10669","author":"Hansen Helle Hvid","year":"2017"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837673"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80251-8"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/788019.788882"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/646514.695804"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/1779046.1779071"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1182613.1182616"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(2:7)2012"},{"key":"e_1_2_2_34_1","unstructured":"Matteo Mio and Alex Simpson. 2015. \u0141ukasiewicz \u00b5-calculus. https:\/\/arxiv.org\/abs\/1510.00797 arXiv:1510.00797.  Matteo Mio and Alex Simpson. 2015. \u0141ukasiewicz \u00b5-calculus. https:\/\/arxiv.org\/abs\/1510.00797 arXiv:1510.00797."},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2017-1472"},{"volume-title":"Hanne Riis Nielson, and Chris Hankin","year":"1999","author":"Nielson Flemming","key":"e_1_2_2_36_1"},{"key":"e_1_2_2_37_1","unstructured":"Katja Poltermann. 2017. A Modal Logic for Conditional Transition Systems. Bachelor\u2019s thesis. Universit\u00e4t Duisburg-Essen.  Katja Poltermann. 2017. A Modal Logic for Conditional Transition Systems. Bachelor\u2019s thesis. Universit\u00e4t Duisburg-Essen."},{"volume-title":"Advanced Topics in Bisimulation and Coinduction","author":"Pous Damien","key":"e_1_2_2_38_1"},{"volume-title":"Introduction to Bisimulation and Coinduction","author":"Sangiorgi Davide","key":"e_1_2_2_39_1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511777110"},{"volume-title":"Verification of Reactive Systems: Formal Methods and Algorithms","author":"Schneider Klaus","key":"e_1_2_2_40_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-10778-2"},{"volume-title":"Toposes, Algebraic Geometry and Logic (Lecture Notes in Mathematics)","author":"Scott Dana","key":"e_1_2_2_41_1"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(96)00130-5"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/646482.691452"},{"key":"e_1_2_2_44_1","volume-title":"Proc. of CONCUR \u201995 (Lecture Notes in Computer Science)","volume":"962","author":"Stirling Colin","year":"1995"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90110-4"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.09.035"},{"volume-title":"Lectures on the modal \u00b5-calculus. Lecture notes","author":"Venema Yde","key":"e_1_2_2_48_1"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00009-7"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290339","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290339","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290339"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":48,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290339"],"URL":"https:\/\/doi.org\/10.1145\/3290339","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}