Document Open Access Logo

On-The-Fly Verification: Advancements in Dependency Graphs (Invited Talk)

Author Jiří Srba

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CONCUR.2025.3.pdf
  • Filesize: 467 kB
  • 5 pages
HTML5 Logo HTML (experimental)
LIPIcs.CONCUR.2025.3.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • dependency graphs
  • Boolean equation systems
  • on-the-fly algorithms
  • fixed-point computation
  • applications

Metrics

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

Abstract

Dependency graphs have emerged as a versatile and powerful formalism with wide-ranging applications in formal verification. In this extended abstract, we provide an overview of selected advancements in on-the-fly verification techniques based on dependency graphs, focusing on the recent developments, optimizations and generalizations of this generic verification framework.

Cite As Get BibTex

Jiří Srba. On-The-Fly Verification: Advancements in Dependency Graphs (Invited Talk). In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 3:1-3:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CONCUR.2025.3

Author Details

Jiří Srba
  • Department of Computer Science, Aalborg University, Denmark

Acknowledgements

I want to thank many of my co-authors for their contributions to the development of the dependency graph framework and its applications, including J.R. Andersen, N. Andersen, A.E. Dalsgaard, S. Enevoldsen, P. Fogh, M.M. Hansen, L.S. Jensen, M.C. Jensen, N.O. Jensen, P.G. Jensen, T.S. Jepsen, I. Kaufmann, K.G. Larsen, D. Lime, A. Mariegaard, S.M. Nielsen, S.R. Olesen, M.Chr. Olesen and S. Pastva.

References

  1. Henrik Reif Andersen. Model checking and Boolean graphs. In Bernd Krieg-Brückner, editor, ESOP '92, 4th European Symposium on Programming, Rennes, France, February 26-28, 1992, Proceedings, volume 582 of Lecture Notes in Computer Science, pages 1-19. Springer, 1992. URL: https://doi.org/10.1007/3-540-55253-7_1.
  2. Henrik Reif Andersen. Model checking and Boolean graphs. Theoretical Computer Science, 126(1):3-30, 1994. URL: https://doi.org/10.1016/0304-3975(94)90266-6.
  3. Henrik Reif Andersen and Glynn Winskel. Compositional checking of satisfaction. In Kim Guldstrand Larsen and Arne Skou, editors, Computer Aided Verification, 3rd International Workshop, CAV '91, Aalborg, Denmark, July, 1-4, 1991, Proceedings, volume 575 of Lecture Notes in Computer Science, pages 24-36. Springer, 1991. URL: https://doi.org/10.1007/3-540-55179-4_4.
  4. J.R. Andersen, N. Andersen, S. Enevoldsen, M.M. Hansen, K.G. Larsen, S.R. Olesen, J. Srba, and J.K. Wortmann. CAAL: Concurrency workbench, Aalborg edition. In Proceedings of the 12th International Colloquium on Theoretical Aspects of Computing (ICTAC'15), volume 9399 of LNCS, pages 573-582. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-25150-9_33.
  5. Julian C. Bradfield and Colin Stirling. Local model checking for infinite state spaces. Theor. Comput. Sci., 96(1):157-174, 1992. URL: https://doi.org/10.1016/0304-3975(92)90183-G.
  6. Falke B. Ø. Carlsen, Lars Bo P. Frydenskov, Nicolaj Ø. Jensen, Jener Rasmussen, Mathias M. Sørensen, Asger G. Weirsøe, Mathias C. Jensen, and Kim G. Larsen. CGAAL: Distributed on-the-fly ATL model checker with heuristics. Electronic Proceedings in Theoretical Computer Science, 390:99-114, September 2023. URL: https://doi.org/10.4204/eptcs.390.7.
  7. Franck Cassez, Alexandre David, Emmanuel Fleury, Kim G. Larsen, and Didier Lime. Efficient on-the-fly algorithms for the analysis of timed games. In Martín Abadi and Luca de Alfaro, editors, CONCUR 2005 - Concurrency Theory, volume 3653 of LNCS, pages 66-80, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/11539452_9.
  8. Peter Christoffersen, Mikkel Hansen, Anders Mariegaard, Julian Trier Ringsmose, Kim Guldstrand Larsen, and Radu Mardare. Parametric Verification of Weighted Systems. In Étienne André and Goran Frehse, editors, 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15), volume 44 of OpenAccess Series in Informatics (OASIcs), pages 77-90, Dagstuhl, Germany, 2015. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/OASIcs.SynCoP.2015.77.
  9. A.E. Dalsgaard, S. Enevoldsen, P. Fogh, L.S. Jensen, P.G. Jensen, T.S. Jepsen, I. Kaufmann, K.G. Larsen, S.M. Nielsen, M.Chr. Olesen, S. Pastva, and J. Srba. A distributed fixed-point algorithm for extended dependency graphs. Fundamenta Informaticae, 161(4):351-381, 2018. URL: https://doi.org/10.3233/FI-2018-1707.
  10. A.E. Dalsgaard, S. Enevoldsen, P. Fogh, L.S. Jensen, T.S. Jepsen, I. Kaufmann, K.G. Larsen, S.M. Nielsen, M.Chr. Olesen, S. Pastva, and J. Srba. Extended dependency graphs and efficient distributed fixed-point computation. In Proceedings of the 38th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets'17), volume 10258 of LNCS, pages 139-158. Springer-Verlag, 2017. URL: https://doi.org/10.1007/978-3-319-57861-3_10.
  11. A.E. Dalsgaard, S. Enevoldsen, K.G. Larsen, and J. Srba. Distributed computation of fixed points on dependency graphs. In Proceedings of Symposium on Dependable Software Engineering: Theories, Tools and Applications (SETTA'16), volume 9984 of LNCS, pages 197-212. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-47677-3_13.
  12. A. David, L. Jacobsen, M. Jacobsen, K.Y. Jørgensen, M.H. Møller, and J. Srba. TAPAAL 2.0: Integrated development environment for timed-arc Petri nets. In Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'12), volume 7214 of LNCS, pages 492-497. Springer-Verlag, 2012. URL: https://doi.org/10.1007/978-3-642-28756-5_36.
  13. S. Enevoldsen, M.C. Jensen, K.G. Larsen, A. Mariegaard, and J. Srba. Verification of multiplayer stochastic games via abstract dependency graphs. In Proceedings of the 30th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'20), volume 12561 of LNCS, pages 249-268. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-68446-4_13.
  14. S. Enevoldsen, K.G. Larsen, A. Mariegaard, and J. Srba. Dependency graphs with applications to verification. International Journal on Software Tools for Technology Transfer (STTT), 22:635-654, 2020. URL: https://doi.org/10.1007/s10009-020-00578-9.
  15. S. Enevoldsen, K.G. Larsen, and J. Srba. Abstract dependency graphs and their application to model checking. In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19), volume 11427 of LNCS, pages 316-333. Springer-Verlag, 2019. URL: https://doi.org/10.1007/978-3-030-17462-0_18.
  16. S. Enevoldsen, K.G. Larsen, and J. Srba. Model verification through dependency graphs. In Proceedings of the 26th International SPIN Symposium on Model Checking of Software (SPIN'19), volume 11636 of LNCS, pages 1-19. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-30923-7_1.
  17. S. Enevoldsen, K.G. Larsen, and J. Srba. Extended abstract dependency graphs. International Journal on Software Tools for Technology Transfer (STTT), 24:49-65, 2022. URL: https://doi.org/10.1007/s10009-021-00638-8.
  18. J.F. Jensen, K.G. Larsen, J. Srba, and L.K. Oestergaard. Local model checking of weighted CTL with upper-bound constraints. In Proceedings of International SPIN Symposium on Model Checking of Software (SPIN'13), volume 7976 of LNCS, pages 178-195. Springer-Verlag, 2013. URL: https://doi.org/10.1007/978-3-642-39176-7_12.
  19. J.F. Jensen, K.G. Larsen, J. Srba, and L.K. Oestergaard. Efficient model checking of weighted CTL with upper-bound constraints. International Journal on Software Tools for Technology Transfer (STTT), 18(4):409-426, 2016. URL: https://doi.org/10.1007/s10009-014-0359-5.
  20. J.S. Jensen, I. Kaufmann, K.G. Larsen, S.M. Nielsen, and J. Srba. Model checking and synthesis for branching multi-weighted logics. Journal of Logical and Algebraic Methods in Programming, 105(1):28-46, 2019. URL: https://doi.org/10.1016/j.jlamp.2019.02.001.
  21. Mathias Claus Jensen, Anders Mariegaard, and Kim Guldstrand Larsen. Symbolic model checking of weighted PCTL using dependency graphs. In Julia M. Badger and Kristin Yvonne Rozier, editors, NASA Formal Methods - 11th International Symposium, NFM 2019, Houston, TX, USA, May 7-9, 2019, Proceedings, volume 11460 of Lecture Notes in Computer Science, pages 298-315. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-20652-9_20.
  22. Nicolaj Ø. Jensen, Kim G. Larsen, Didier Lime, and Jiří Srba. On-the-fly symbolic algorithm for timed ATL with abstractions. In 36th International Conference on Concurrency Theory (CONCUR'25), pages 1-18. Schloss Dagstuhl, 2025. To appear. Google Scholar
  23. N.O. Jensen, K.G. Larsen, and J. Srba. Token elimination in model checking of Petri nets. In Proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'25), volume 15696 of LNCS, pages 211-230. Springer-Verlag, 2025. URL: https://doi.org/10.1007/978-3-031-90643-5_11.
  24. P.G. Jensen, K.G. Larsen, and J. Srba. Real-time strategy synthesis for timed-arc Petri net games via discretization. In Proceedings of the 23rd International SPIN Symposium on Model Checking of Software (SPIN'16), volume 9641 of LNCS, pages 129-146. Springer-Verlag, 2016. URL: https://doi.org/10.1007/978-3-319-32582-8_9.
  25. P.G. Jensen, K.G. Larsen, and J. Srba. Discrete and continuous strategies for timed-arc Petri net games. International Journal on Software Tools for Technology Transfer (STTT), 20(5):529-546, 2018. URL: https://doi.org/10.1007/s10009-017-0473-2.
  26. P.G. Jensen, K.G. Larsen, J. Srba, and N.J. Ulrik. Elimination of detached regions in dependency graph verification. In Proceedings of the 29th International SPIN Symposium on Model Checking of Software (SPIN'23), volume 13872 of LNCS, pages 163-179. Springer-Verlag, 2023. URL: https://doi.org/10.1007/978-3-031-32157-3_9.
  27. I. Kaufmann, K.G. Larsen, and J. Srba. Synthesis for multi-weighted games with branching-time winning conditions. In Proceedings of the 41st International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets'20), volume 12152 of LNCS, pages 46-66. Springer-Verlag, 2020. URL: https://doi.org/10.1007/978-3-030-51831-8_3.
  28. Kim Guldstrand Larsen. Proof system for hennessy-milner logic with recursion. In Max Dauchet and Maurice Nivat, editors, CAAP '88, 13th Colloquium on Trees in Algebra and Programming, Nancy, France, March 21-24, 1988, Proceedings, volume 299 of Lecture Notes in Computer Science, pages 215-230. Springer, 1988. URL: https://doi.org/10.1007/BFb0026106.
  29. Kim Guldstrand Larsen. Proof systems for satisfiability in Hennessy-Milner logic with recursion. Theor. Comput. Sci., 72(2&3):265-288, 1990. URL: https://doi.org/10.1016/0304-3975(90)90038-J.
  30. Xinxin Liu, C. R. Ramakrishnan, and Scott A. Smolka. Fully local and efficient evaluation of alternating fixed points. In Proceedings of TACAS'98, volume 1384 of LNCS, pages 5-19. Springer, 1998. URL: https://doi.org/10.1007/BFb0054161.
  31. Xinxin Liu and Scott A. Smolka. Simple linear-time algorithms for minimal fixed points (extended abstract). In Proceedings of ICALP'98, volume 1443 of LNCS, pages 53-66, London, UK, UK, 1998. Springer-Verlag. URL: https://doi.org/10.1007/BFB0055040.
  32. Anders Mariegaard and Kim Guldstrand Larsen. Symbolic dependency graphs for PCTL model-checking. In Alessandro Abate and Gilles Geeraerts, editors, 15th Internation Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'17), volume 10419 of LNCS, pages 153-169. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-65765-3_9.
  33. Colin Stirling and David Walker. Local model checking in the modal mu-calculus. Theor. Comput. Sci., 89(1):161-177, 1991. URL: https://doi.org/10.1016/0304-3975(90)90110-4.
  34. Glynn Winskel. A note on model checking the modal nu-calculus. Theor. Comput. Sci., 83(1):157-167, 1991. URL: https://doi.org/10.1016/0304-3975(91)90043-2.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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