Abstract
Knaster-Tarski’s 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 \(\mathbb {M}^Y\), where Y is a finite set and \(\mathbb {M}\) 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.
Chapter PDF
Similar content being viewed by others
References
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–25 (2017)
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 ’19. LIPIcs, vol. 140, pp. 9:1–9:17. Schloss Dagstuhl– Leibniz Center for Informatics (2019)
Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)
Baldan, P., Bonchi, F., Kerstan, H., König, 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)
Baldan, P., Eggert, R., König, B., Padoan, T.: Fixpoint theory – upside down(2021), https://arxiv.org/abs/2101.08184, arXiv:2101.08184
Baldan, P., König, B., Padoan, T.: Abstraction, up-to techniques and games for systems of fixpoint equations. In: Proc. of CONCUR ’20. LIPIcs, vol. 171, pp. 25:1–25:20. Schloss Dagstuhl – Leibniz Center for Informatics (2020), https://doi.org/10.4230/LIPIcs.CONCUR.2020.25
Björklund, H., Vorobyov, S.: Combinatorial structure and randomized subexponential algorithms for infinite games. Theoretical Computer Science 349(3), 347–360 (2005)
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–118 (2011)
Cleaveland, R.: On automatically explaining bisimulation inequivalence. In: Proc. of CAV ’90. pp. 364–372. Springer (1990), LNCS 531
Condon, A.: On algorithms for simple stochastic games. In: Advances In Computational Complexity Theory. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 13, pp. 51–71 (1990)
Condon, A.: The complexity of stochastic games. Information and Computation 96(2), 203–224 (1992). https://doi.org/10.1016/0890-5401(92)90048-K, https://doi.org/10.1016/0890-5401(92)90048-K
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 ’12 (International Conference on Software Engineering). pp. 672–682. IEEE (2012)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model forstatic analysis of programs by construction or approximation of fixpoints. In: Proc. of POPL ’77 (Los Angeles, California). pp. 238–252. ACM (1977)
Cousot, P., Cousot, R.: Temporal abstract interpretation. In: Wegman, M.N., Reps, T.W. (eds.) Proc. of POPL ’00. pp. 12–25. ACM (2000)
de Alfaro, L., Faella, M., Stoelinga, M.: Linear and branching system metrics. IEEE Transactions on Software Engineering 35(2), 258–273 (2009)
Fu, H.: Computing game metrics on Markov decision processes. In: Proc. of ICALP ’12, Part II. pp. 227–238. Springer (2012), LNCS 7392
Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32, 137–161 (1985)
Karp, R.M., Hoffman, A.J.: On nonterminating stochastic games. Management Science 12(5), 359–370 (1966)
Kelmendi, E., Krämer, J., Křetínský, J., Weininger, M.: Value iteration for simple stochastic games: Stopping criterion and learning algorithm. In: Proc. of CAV ’18. pp. 623–642. Springer (2018), LNCS 10981
Mémoli, F.: Gromov-Wasserstein distances and the metric approach to object matching. Foundations of Computational Mathematics 11(4), 417–487 (2011)
Mundici, D.: MV-algebras. A short tutorial, available at http://www.matematica.uns.edu.ar/IXCongresoMonteiro/Comunicaciones/Mundici_tutorial.pdf
Mundici, D.: Advanced Łukasiewicz calculus and MV-algebras, Trends inLogic, vol. 35. Springer (2011)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer (2010)
Peyré, G., Cuturi, M.: Computational optimal transport (2020), https://arxiv.org/abs/2009.14817, arXiv:1803.00567
Pous, D.: Complete lattices and up-to techniques. In: Proc. of APLAS ’07. pp. 351–366. Springer (2007), LNCS 4807
Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press (2011)
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
Tarski, A.: A lattice-theoretical theorem and its applications. Pacific Journal of Mathematics 5, 285–309 (1955)
Tripathi, R., Valkanova, E., Kumar, V.A.: On strategy improvement algorithms for simple stochastic games. Journal of Discrete Algorithms 9, 263–278 (2011)
Villani, C.: Optimal Transport – Old and New, A Series of Comprehensive Studies in Mathematics, vol. 338. Springer (2009)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Baldan, P., Eggert, R., König, B., Padoan, T. (2021). Fixpoint Theory – Upside Down. In: Kiefer, S., Tasson, C. (eds) Foundations of Software Science and Computation Structures. FOSSACS 2021. Lecture Notes in Computer Science(), vol 12650. Springer, Cham. https://doi.org/10.1007/978-3-030-71995-1_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-71995-1_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-71994-4
Online ISBN: 978-3-030-71995-1
eBook Packages: Computer ScienceComputer Science (R0)