A String Diagrammatic Approach to Structural Verification

Abstract: We present a string diagrammatic approach to structural (modular or compositional) verification. In this talk, we focus on probabilistic model checking of Markov decision processes and we show compositional algorithms that leverage multi-objective optimization. Finally, we introduce our ongoing work that extends this approach. This talk is based on joint work with Kazuyuki Asada, Clovis Eberhart, Ichiro Hasuo, Sebastian Junges, Satoshi Kura, Jurriaan Rot, Hiroshi Unno, and Marck van der Vegt.
Related References:

• Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada and Ichiro Hasuo. “Compositional Probabilistic Model Checking with String Diagrams of MDPs” CAV2023.
• Kazuki Watanabe*, Marck van der Vegt*, Ichiro Hasuo, Jurriaan Rot, and Sebastian Junges, “Pareto Curves for Compositionally Model Checking String Diagrams of MDPs.” TACAS2024. *Equally contributed.
• Kazuki Watanabe*, Marck van der Vegt*, Sebastian Junges, and Ichiro Hasuo, “Compositional Value Iteration with Pareto Caching.” CAV2024. *Equally contributed.
• Marck van der Vegt, Kazuki Watanabe, Ichiro Hasuo, and Sebastian Junges. “Compositional Verification of Almost-Sure Büchi Objectives in MDPs.” To Appear in RP2025.

Bio: Kazuki Watanabe is an Assistant Professor at the National Institute of Informatics (NII), Japan. He received his Ph.D. in Informatics from NII in March 2025 under the supervision of Professor Ichiro Hasuo. In 2023, he spent six months at Radboud University as a guest hosted by Professors Jurriaan Rot and Sebastian Junges. His research focuses on applied category theory and algorithms for formal verification.