July 16 (Tue), 2024, 15:30-17:30
Ochanomizu University, Bldg. 1, the room 126
2-1-1 Ootsuka, Bunkyo-ku, Tokyo (zip:112-8610)
Transport and Direction | Ochanomizu University
Compositional Probabilistic Model Checking with String Diagram
I present our recent lines of work on compositional model checking with string diagrams.
Compositional model checking is a promising approach to verify information systems in a divide-and-conquer manner. In this talk, I present our compositional probabilistic model checking on Markov decision processes (MDPs) with string diagrams. String diagrams are a graphical language based on monoidal categories, in which we compositionally describe the MDP that we verify. We formulate our compositional probabilistic model checking as a compact closed functor from string diagrams of MDPs to the semantic category (in [1]). We further develop an approximation algorithm based on Pareto curves, and show a significant performance improvement (in [2]).
[1] Watanabe, K., Eberhart, C., Asada, K., Hasuo, I. (2023). Compositional Probabilistic Model Checking with String Diagrams of MDPs. In: Enea, C., Lal, A. (eds) Computer Aided Verification. CAV 2023. Lecture Notes in Computer Science, vol 13966. Springer, Cham. https://doi.org/10.1007/978-3-031-37709-9_3
[2] Watanabe, K., van der Vegt, M., Hasuo, I., Rot, J., Junges, S. (2024). Pareto Curves for Compositionally Model Checking String Diagrams of MDPs. In: Finkbeiner, B., Kovács, L. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2024. Lecture Notes in Computer Science, vol 14571. Springer, Cham.
https://doi.org/10.1007/978-3-031-57249-4_14
Compositional-distributional models of meaning
How does one account for linguistic structure in Natural Language Processing (NLP)? This rapidly growing field of research depends on huge amounts of data, but as we keep testing the limits of the size of data usage, perhaps looking closer at the structure of the data holds clues to better models of meaning. Compositional-distributional models of meaning combine strengths of modern NLP with classical logical models of language. This fusion has been made possible using category theory - the mathematics of composition. I will present the origins [1] of this research and how it has developed since its creation, including linguistic extensions [2] and contributions to transparency and quantum computing [3].