Document Open Access Logo

Real Equation Systems with Alternating Fixed-Points

Authors Jan Friso Groote , Tim A. C. Willemse

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2023.28.pdf
  • Filesize: 0.75 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Verification by model checking
Keywords
  • Real Equation System
  • Solution method
  • Gauß-elimination
  • Model checking
  • Quantitative modal mu-calculus

Metrics

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

Abstract

We introduce the notion of a Real Equation System (RES), which lifts Boolean Equation Systems (BESs) to the domain of extended real numbers. Our RESs allow arbitrary nesting of least and greatest fixed-point operators. We show that each RES can be rewritten into an equivalent RES in normal form. These normal forms provide the basis for a complete procedure to solve RESs. This employs the elimination of the fixed-point variable at the left side of an equation from its right-hand side, combined with a technique often referred to as Gauß-elimination. We illustrate how this framework can be used to verify quantitative modal formulas with alternating fixed-point operators interpreted over probabilistic labelled transition systems.

Cite As Get BibTex

Jan Friso Groote and Tim A. C. Willemse. Real Equation Systems with Alternating Fixed-Points. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.CONCUR.2023.28

Author Details

Jan Friso Groote
  • Department of Mathematics and Computer Science, Eindhoven University of Technology, The Netherlands
Tim A. C. Willemse
  • Department of Mathematics and Computer Science, Eindhoven University of Technology, The Netherlands

References

  1. Giorgio Bacci, Giovanni Bacci, Mathias Claus Jensen, and Kim G. Larsen. Convex lattice equation systems. In Jean-François Raskin, Krishnendu Chatterjee, Laurent Doyen, and Rupak Majumdar, editors, Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday, volume 13660 of Lecture Notes in Computer Science, pages 438-455. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-22337-2_21.
  2. Julian C. Bradfield and Colin Stirling. Modal mu-calculi. In Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning, pages 721-756. North-Holland, 2007. Google Scholar
  3. Julian C. Bradfield and Igor Walukiewicz. The mu-calculus and model checking. In Handbook of Model Checking, pages 871-919. Springer, 2018. Google Scholar
  4. Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasipolynomial time. In Hamed Hatami, Pierre McKenzie, and Valerie King, editors, Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2017, Montreal, QC, Canada, June 19-23, 2017, pages 252-263. ACM, 2017. URL: https://doi.org/10.1145/3055399.3055409.
  5. Sjoerd Cranen, Jan Friso Groote, and Michel A. Reniers. A linear translation from CTL* to the first-order modal μ-calculus. Theor. Comput. Sci., 412(28):3129-3139, 2011. URL: https://doi.org/10.1016/j.tcs.2011.02.034.
  6. Susmoy Das and Arpit Sharma. On the use of model and logical embeddings for model checking of probabilistic systems. In Marieke Huisman and António Ravara, editors, Formal Techniques for Distributed Objects, Components, and Systems - 43rd IFIP WG 6.1 International Conference, FORTE 2023, Held as Part of the 18th International Federated Conference on Distributed Computing Techniques, DisCoTec 2023, Lisbon, Portugal, June 19-23, 2023, Proceedings, volume 13910 of Lecture Notes in Computer Science, pages 115-131. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-35355-0_8.
  7. Thomas Gawlitza and Helmut Seidl. Precise fixpoint computation through strategy iteration. In Rocco De Nicola, editor, Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, Held as Part of the Joint European Conferences on Theory and Practics of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007, Proceedings, volume 4421 of Lecture Notes in Computer Science, pages 300-315. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-71316-6_21.
  8. Thomas Martin Gawlitza and Helmut Seidl. Solving systems of rational equations through strategy iteration. ACM Trans. Program. Lang. Syst., 33(3):11:1-11:48, 2011. URL: https://doi.org/10.1145/1961204.1961207.
  9. Maciej Gazda and Tim A. C. Willemse. Zielonka’s recursive algorithm: dull, weak and solitaire games and tighter bounds. In Gabriele Puppis and Tiziano Villa, editors, Proceedings Fourth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2013, Borca di Cadore, Dolomites, Italy, 29-31th August 2013, volume 119 of EPTCS, pages 7-20, 2013. URL: https://doi.org/10.4204/EPTCS.119.4.
  10. Jan Friso Groote and Erik P. de Vink. Problem solving using process algebra considered insightful. In Joost-Pieter Katoen, Rom Langerak, and Arend Rensink, editors, ModelEd, TestEd, TrustEd - Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday, volume 10500 of Lecture Notes in Computer Science, pages 48-63. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-68270-9_3.
  11. Jan Friso Groote and Mohammad Reza Mousavi. Modeling and Analysis of Communicating Systems. MIT Press, 2014. URL: https://mitpress.mit.edu/books/modeling-and-analysis-communicating-systems.
  12. Jan Friso Groote, Freek Wiedijk, and Hans Zantema. A probabilistic analysis of the game of the goose. SIAM Rev., 58(1):143-155, 2016. URL: https://doi.org/10.1137/140983781.
  13. Jan Friso Groote and Tim A. C. Willemse. Model-checking processes with data. Sci. Comput. Program., 56(3):251-273, 2005. URL: https://doi.org/10.1016/j.scico.2004.08.002.
  14. Jan Friso Groote and Tim A. C. Willemse. Parameterised boolean equation systems. Theor. Comput. Sci., 343(3):332-369, 2005. URL: https://doi.org/10.1016/j.tcs.2005.06.016.
  15. Thomas A. Henzinger. From boolean to quantitative notions of correctness. In Manuel V. Hermenegildo and Jens Palsberg, editors, Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, pages 157-158. ACM, 2010. URL: https://doi.org/10.1145/1706299.1706319.
  16. Thomas A. Henzinger and Joseph Sifakis. The embedded systems design challenge. In Jayadev Misra, Tobias Nipkow, and Emil Sekerinski, editors, FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006, Proceedings, volume 4085 of Lecture Notes in Computer Science, pages 1-15. Springer, 2006. URL: https://doi.org/10.1007/11813040_1.
  17. Marcin Jurdzinski and Ranko Lazic. Succinct progress measures for solving parity games. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-9. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005092.
  18. Kyriakos Kalorkoti. Solving Łiukasiewicz μ-terms. Theor. Comput. Sci., 712:38-49, 2018. URL: https://doi.org/10.1016/j.tcs.2017.11.002.
  19. Kim Guldstrand Larsen. Efficient local correctness checking. In Gregor von Bochmann and David K. Probst, editors, Computer Aided Verification, Fourth International Workshop, CAV '92, Montreal, Canada, June 29 - July 1, 1992, Proceedings, volume 663 of Lecture Notes in Computer Science, pages 30-43. Springer, 1992. URL: https://doi.org/10.1007/3-540-56496-9_4.
  20. Angelika Mader. Modal μ-calculus, model checking and gauß elimination. In Ed Brinksma, Rance Cleaveland, Kim Guldstrand Larsen, Tiziana Margaria, and Bernhard Steffen, editors, Tools and Algorithms for Construction and Analysis of Systems, First International Workshop, TACAS '95, Aarhus, Denmark, May 19-20, 1995, Proceedings, volume 1019 of Lecture Notes in Computer Science, pages 72-88. Springer, 1995. URL: https://doi.org/10.1007/3-540-60630-0_4.
  21. Angelika Mader. Verification of Modal Properties Using Boolean Equation Systems. PhD thesis, Technische Universität München, 1997. Google Scholar
  22. Radu Mateescu. Vérification des propriétés temporelles des programmes parallèles. PhD thesis, Institut National Polytechnique de Grenoble, 1998. Google Scholar
  23. Robert McNaughton. Infinite games played on finite graphs. Ann. Pure Appl. Logic, 65(2):149-184, 1993. URL: https://doi.org/10.1016/0168-0072(93)90036-D.
  24. Matteo Mio and Alex Simpson. Łukasiewicz μ-calculus. Fundam. Informaticae, 150(3-4):317-346, 2017. URL: https://doi.org/10.3233/FI-2017-1472.
  25. Tom van Dijk. Oink: An implementation and evaluation of modern parity game solvers. In Dirk Beyer and Marieke Huisman, editors, Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part I, volume 10805 of Lecture Notes in Computer Science, pages 291-308. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89960-2_16.
  26. Wieslaw Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci., 200(1-2):135-183, 1998. URL: https://doi.org/10.1016/S0304-3975(98)00009-7.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact