{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:48:01Z","timestamp":1742914081496,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030719944"},{"type":"electronic","value":"9783030719951"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Knaster-Tarski\u2019s theorem, characterising the greatest fix- point of a monotone function over a complete lattice as the largest post-fixpoint, naturally leads to the so-called coinduction proof principle for showing that some element is below the greatest fixpoint (e.g., for providing bisimilarity witnesses). The dual principle, used for showing that an element is above the least fixpoint, is related to inductive invariants. In this paper we provide proof rules which are similar in spirit but for showing that an element is above the greatest fixpoint or, dually, below the least fixpoint. The theory is developed for non-expansive monotone functions on suitable lattices of the form<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathbb {M}^Y$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msup><mml:mrow><mml:mi>M<\/mml:mi><\/mml:mrow><mml:mi>Y<\/mml:mi><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>, where<jats:italic>Y<\/jats:italic>is a finite set and<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathbb {M}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>M<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>an MV-algebra, and it is based on the construction of (finitary) approximations of the original functions. We show that our theory applies to a wide range of examples, including termination probabilities, behavioural distances for probabilistic automata and bisimilarity. Moreover it allows us to determine original algorithms for solving simple stochastic games.<\/jats:p>","DOI":"10.1007\/978-3-030-71995-1_4","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T17:03:39Z","timestamp":1616432619000},"page":"62-81","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Fixpoint Theory \u2013 Upside Down"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9357-5599","authenticated-orcid":false,"given":"Paolo","family":"Baldan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9901-7392","authenticated-orcid":false,"given":"Richard","family":"Eggert","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4193-2889","authenticated-orcid":false,"given":"Barbara","family":"K\u00f6nig","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7814-1485","authenticated-orcid":false,"given":"Tommaso","family":"Padoan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"4_CR1","unstructured":"Bacci, G., Bacci, G., Larsen, K.G., Mardare, R.: On-the-fly exact computation of bisimilarity distances. Logical Methods in Computer Science 13(2:13), 1\u201325 (2017)"},{"key":"4_CR2","unstructured":"Bacci, G., Bacci, G., Larsen, K.G., Mardare, R., Tang, Q., van Breugel, F.: Computing probabilistic bisimilarity distances for probabilistic automata. In: Proc. of CONCUR \u201919. LIPIcs, vol.\u00a0140, pp. 9:1\u20139:17. Schloss Dagstuhl\u2013 Leibniz Center for Informatics (2019)"},{"key":"4_CR3","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)"},{"key":"4_CR4","unstructured":"Baldan, P., Bonchi, F., Kerstan, H., K\u00f6nig, B.: Coalgebraic behavioral metrics. Logical Methods in Computer Science 14(3) (2018), selected Papers of the 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)"},{"key":"4_CR5","unstructured":"Baldan, P., Eggert, R., K\u00f6nig, B., Padoan, T.: Fixpoint theory \u2013 upside down(2021), https:\/\/arxiv.org\/abs\/2101.08184, arXiv:2101.08184"},{"key":"4_CR6","unstructured":"Baldan, P., K\u00f6nig, B., Padoan, T.: Abstraction, up-to techniques and games for systems of fixpoint equations. In: Proc. of CONCUR \u201920. LIPIcs, vol.\u00a0171, pp. 25:1\u201325:20. Schloss Dagstuhl \u2013 Leibniz Center for Informatics (2020), https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2020.25"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Bj\u00f6rklund, H., Vorobyov, S.: Combinatorial structure and randomized subexponential algorithms for infinite games. Theoretical Computer Science 349(3), 347\u2013360 (2005)","DOI":"10.1016\/j.tcs.2005.07.041"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Brim, L., Chaloupka, J., Doyen, L., Gentilini, R., Raskin, J.F.: Faster algorithms for mean-payoff games. Formal Methods in System Design 38(2), 97\u2013118 (2011)","DOI":"10.1007\/s10703-010-0105-x"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Cleaveland, R.: On automatically explaining bisimulation inequivalence. In: Proc. of CAV \u201990. pp. 364\u2013372. Springer (1990), LNCS 531","DOI":"10.1007\/BFb0023750"},{"key":"4_CR10","unstructured":"Condon, A.: On algorithms for simple stochastic games. In: Advances In Computational Complexity Theory. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol.\u00a013, pp. 51\u201371 (1990)"},{"key":"4_CR11","doi-asserted-by":"publisher","unstructured":"Condon, A.: The complexity of stochastic games. Information and Computation 96(2), 203\u2013224 (1992). https:\/\/doi.org\/10.1016\/0890-5401(92)90048-K, https:\/\/doi.org\/10.1016\/0890-5401(92)90048-K","DOI":"10.1016\/0890-5401(92)90048-K"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Cordy, M., Classen, A., Perrouin, G., Schobbens, P.Y., Heymans, P., Legay, A.: Simulation-based abstractions for software product-line model checking. In: Proc. of ICSE \u201912 (International Conference on Software Engineering). pp. 672\u2013682. IEEE (2012)","DOI":"10.1145\/2364412.2364425"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model forstatic analysis of programs by construction or approximation of fixpoints. In: Proc. of POPL \u201977 (Los Angeles, California). pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Temporal abstract interpretation. In: Wegman, M.N., Reps, T.W. (eds.) Proc. of POPL \u201900. pp. 12\u201325. ACM (2000)","DOI":"10.1145\/325694.325699"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Faella, M., Stoelinga, M.: Linear and branching system metrics. IEEE Transactions on Software Engineering 35(2), 258\u2013273 (2009)","DOI":"10.1109\/TSE.2008.106"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Fu, H.: Computing game metrics on Markov decision processes. In: Proc. of ICALP \u201912, Part\u00a0II. pp. 227\u2013238. Springer (2012), LNCS 7392","DOI":"10.1007\/978-3-642-31585-5_23"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32, 137\u2013161 (1985)","DOI":"10.1145\/2455.2460"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Karp, R.M., Hoffman, A.J.: On nonterminating stochastic games. Management Science 12(5), 359\u2013370 (1966)","DOI":"10.1287\/mnsc.12.5.359"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Kelmendi, E., Kr\u00e4mer, J., K\u0159et\u00ednsk\u00fd, J., Weininger, M.: Value iteration for simple stochastic games: Stopping criterion and learning algorithm. In: Proc. of CAV \u201918. pp. 623\u2013642. Springer (2018), LNCS 10981","DOI":"10.1007\/978-3-319-96145-3_36"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"M\u00e9moli, F.: Gromov-Wasserstein distances and the metric approach to object matching. Foundations of Computational Mathematics 11(4), 417\u2013487 (2011)","DOI":"10.1007\/s10208-011-9093-5"},{"key":"4_CR21","unstructured":"Mundici, D.: MV-algebras. A short tutorial, available at http:\/\/www.matematica.uns.edu.ar\/IXCongresoMonteiro\/Comunicaciones\/Mundici_tutorial.pdf"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Mundici, D.: Advanced \u0141ukasiewicz calculus and MV-algebras, Trends inLogic, vol.\u00a035. Springer (2011)","DOI":"10.1007\/978-94-007-0840-2"},{"key":"4_CR23","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer (2010)"},{"key":"4_CR24","unstructured":"Peyr\u00e9, G., Cuturi, M.: Computational optimal transport (2020), https:\/\/arxiv.org\/abs\/2009.14817, arXiv:1803.00567"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Pous, D.: Complete lattices and up-to techniques. In: Proc. of APLAS \u201907. pp. 351\u2013366. Springer (2007), LNCS 4807","DOI":"10.1007\/978-3-540-76637-7_24"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press (2011)","DOI":"10.1017\/CBO9780511777110"},{"key":"4_CR27","unstructured":"Stirling, C.: Bisimulation, model checking and other games. Notes for Mathfit instructional meeting on games and computation, Edinburgh (June 1997), http:\/\/homepages.inf.ed.ac.uk\/cps\/mathfit.pdf"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A lattice-theoretical theorem and its applications. Pacific Journal of Mathematics 5, 285\u2013309 (1955)","DOI":"10.2140\/pjm.1955.5.285"},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"Tripathi, R., Valkanova, E., Kumar, V.A.: On strategy improvement algorithms for simple stochastic games. Journal of Discrete Algorithms 9, 263\u2013278 (2011)","DOI":"10.1016\/j.jda.2011.03.007"},{"key":"4_CR30","unstructured":"Villani, C.: Optimal Transport \u2013 Old and New, A Series of Comprehensive Studies in Mathematics, vol.\u00a0338. Springer (2009)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-71995-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,22]],"date-time":"2022-12-22T04:34:12Z","timestamp":1671683652000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-71995-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030719944","9783030719951"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-71995-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FOSSACS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"88","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3,2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}