Probabilistic systems have increasingly become ubiquitous in many areas of computer science, including security protocols, artificial intelligence, planning and control, network analysis, and robotics, to name a few. To deploy them in practice, we must have formal and rigorous mathematical guarantees about the behavior of such systems. Formal methods are a well-known paradigm concerned with verification and correct-by-construction in design of software systems. The design and utilization of formal methods for probabilistic models and programs will enable researchers as well as practitioners to design software and intelligent systems that are more robust, trustworthy and safe, even in the presence of probabilistic uncertainty.
The goal of this meeting is to bring together international experts from all over the world in the areas of formal methods, program verification, probabilistic AI, reinforcement learning, Markov chains and Markov decision processes, who all build algorithmic and logical tools with mathematical guarantees for probabilistic systems. Our aim is to create synergy between different communities who share much of the theoretical and mathematical foundations of their research, but are otherwise quite separate, and to create an environment in which they can interchange ideas and learn about the most recent advances in each other’s fields. We believe and hope that this will help forge many new interdisciplinary collaborations and significantly benefit both the attendees and their research communities at large.
As three proposers spanning three top Asian universities in India (IIT Bombay), Hong Kong (HKUST) and Singapore (SMU), at different stages of our careers, our goal is to also foster new collaborations on the area of probabilistic verification, between top universities across Asia, including Japan, India, Singapore, China, Hong Kong, Taiwan and Korea. A seminar on similar topics was recently held in Dagstuhl, Germany in 2023 and was extremely well-received and successful. While a vast majority of the participants in that seminar were from EU countries or the US, in our Shonan proposal, we plan a more internationally-diverse audience, with participants from all continents, but also ensuring the participation of Asian researchers who are typically under-represented at the similar Dagstuhl meetings.

From Finite to Large and Infinite-state Probabilistic Models. Formal analysis of probabilistic models has received significant attention within the formal methods, program verification and AI communities. However, classical formal methods such as probabilistic model checking primarily focus on finite-state probabilistic systems. They are not applicable to infinite-state probabilistic systems, that naturally arise due to e.g. sampling from continuous distributions, reasoning about probabilistic programs, or planning and learning in continuous environments. Moreover, even in the case of finite-state
systems, classical methods face scalability issues. This limits their applicability to large probabilistic models that arise in the analysis of modern networks, security protocols and discrete planning problems.
In this seminar, we plan to study methods that have the promise to enable automated formal analysis of large and infinite-state probabilistic models. To that end, we will specifically include talks, discussions and problem-solving sessions focused on the following novel approaches and recent frontiers that have the potential to overcome the limitations of the classical methods, some of which have already proved themselves to be highly effective in the analysis of large and infinite-state non-probabilistic models. This includes parametrized algorithms, data-driven approaches and compositional approaches, as well as the study of probabilistic models under the distributional view.

Parametrized Algorithms. Parameterized algorithms have been widely studied in the context of program analysis, formal verification and model checking. For example, Courcelle showed that model checking for monadic second-order logic of graphs can be performed efficiently if the underlying graphs have bounded treewidth [7], while the classical result of Thorup shows that control-flow graphs of all structured programs have small treewidth [13]. Thus, treewidth is a parameter that captures sparsity of real-world programs while enabling efficient model checking. Similar results have also been obtained for mu-calculus model checking [11], and there are other well-known graph parameters such as pathwidth, treedepth, maximum degree. Despite its promise in model checking for non-probabilistic systems, parameterized complexity is under-developed when it comes to probabilistic systems. There are works that consider parameterized algorithms for qualitative and quantitative analysis of Markov chains and MDPs [5, 3], but no general parameterized model-checking approaches for probabilistic programs or systems exist. In this meeting our goal is to address this gap by bringing the current state-of-the-art and challenges to a wide audience of researchers in various related fields and encouraging the development of probabilistic counterparts of parameterized model checking algorithms in the problem-solving sessions.

Data-driven Approaches and Certificate Learning. A classical approach to formally verifying a property in a model or a program is to compute a certificate for the property. The certificate is a mathematical object which formally proves that the model satisfies the property. Examples of wellknown certificates include ranking functions and invariants in programs and Lyapunov functions in control systems. Recent years have seen increased interest and a number of successful approaches to learning certificates from data in non-probabilistic programs and control systems, while also providing formal guarantees on their correctness [8, 12, 6]. This synergy of machine learning and formal methods has demonstrated both impressive scalability and the ability to tackle complex infinite-state models and programs that were out of the reach of prior methods. Most existing works in this direction are restricted to non probabilistic models. However, promising initial steps have been made for probabilistic models as well, with recent works studying data-driven certificate learning for probabilistic programs [1, 4] and stochastic control [10, 15, 16]. Our aim in this meeting is to encourage more intensive research on datadriven methods for certificate learning in probabilistic models, towards utilizing this powerful synergy of machine learning and formal methods to improve the scalability of formal probabilistic system analysis.

Compositional Approaches. Compositionality is a highly desirable feature of automated formal methods that was instrumental for their success in model checking and static analysis of non-probabilistic programs. Compositional approaches to model checking of MDPs are a recent and highly successful development in the formal verification community [14]. They have their basis in category theory and provide a natural way of constructing larger MDPs from smaller parts using approaches such as string diagrams, while at the same time exploiting this well-defined structure to find faster analysis algorithms.
The meeting will include several invitees who are experts in this area. Both compositional and parameterized methods are fundamentally based on exploiting the underlying sparsity and well-structuredness of a probabilistic system. Hence, it would be intriguing to bring together experts on both streams to collaborate and come up with novel hybrid approaches together.

Distributional View of Probabilistic Verification. While Markov chains and Markov decision processes are typically viewed as state-transformers, a recent line of research (e.g., [2, 9]) views them as transformers of probability distributions over the states. This view lies closer to several AI and probabilistic programming applications, as it allows one to reason about distributional properties, that hold along the evolution of the probabilistic system. This added expressivity however comes with its costs. Unlike model checking algorithms for classical probabilistic logics (e.g., PCTL∗) which are known to be solvable in polynomial time, model checking distributional properties is much harder. In this seminar, we will examine the relation between these views, tackle the question of expressivity and work towards practical tools to verify distributional properties using parametrized and compositional approaches.

In summary, our goal is to focus on some of the most challenging problems in all of computer science which form the frontiers of probabilistic models and programs, by discussing approaches such as probabilistic model checking, probabilistic program analysis, planning in Markov models, inference, causality, reinforcement learning and stochastic control, and focusing on introducing the most novel and recent ideas of each field to an interdisciplinary audience. By featuring invited talks from top international researchers in all the directions above, as well as group discussions and problem-solving sessions, we hope to provide an opportunity for the participants to broaden their exposure to new and unconventional results which lie outside of their comfort zones and have the potential for high-risk high-reward research.

We aim to have a select set of talks on the specific topics of discussion with sufficient time to interact and create a shared understanding between communities. To introduce the participants to new state-of art
techniques, there will be specific tutorials given by experts in the area on the following topics.

1. Probabilistic Models and Verification: A survey of the state of the art.
2. Data Driven Approaches in Probabilistic models and reasoning.
3. An Introduction to Parametrized algorithms and their use in formal methods.

Participants will also have the opportunity to present their work in short bursts during the ‘Open talk’ slots. Since one of our main goals is fostering discussion between different communities, we will encourage smaller group discussions in specialized working groups. The structure and division into working groups would be identified on the first day, according to the broad specific goals of the workshop. These working groups will discuss via breakout sessions on their respective topic and update each other in the evening.

[1] Alessandro Abate, Mirco Giacobbe, and Diptarko Roy. Learning probabilistic termination proofs. In CAV (2), volume 12760 of Lecture Notes in Computer Science, pages 3–26. Springer, 2021.
[2] S. Akshay, Krishnendu Chatterjee, Tobias Meggendorfer, and Dorde Zikelic. Mdps as distribution transformers: Affine invariant synthesis for safety objectives. In Constantin Enea and Akash Lal, editors, Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III, volume 13966 of Lecture Notes in Computer Science, pages 86–112. Springer, 2023.
[3] Ali Asadi, Krishnendu Chatterjee, Amir Kafshdar Goharshady, Kiarash Mohammadi, and Andreas Pavlogiannis. Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth. In ATVA, pages 253–270, 2020.
[4] Jialu Bao, Nitesh Trivedi, Drashti Pathak, Justin Hsu, and Subhajit Roy. Data-driven invariant learning for probabilistic programs. In CAV (1), volume 13371 of Lecture Notes in Computer Science, pages 33–54. Springer, 2022.
[5] Krishnendu Chatterjee and Jakub Lacki. Faster algorithms for markov decision processes with low treewidth. In CAV, pages 543–558, 2013.
[6] Charles Dawson, Sicun Gao, and Chuchu Fan. Safe control with learned certificates: A survey of neural lyapunov, barrier, and contraction methods for robotics and control. IEEE Trans. Robotics, 39(3):1749–1767, 2023.
[7] Steffen Eger. Regular languages, tree width, and Courcelle’s theorem: an introduction. 2008.
[8] Pranav Garg, Christof Löding, P. Madhusudan, and Daniel Neider. ICE: A robust framework for learning invariants. In CAV, volume 8559 of Lecture Notes in Computer Science, pages 69–87. Springer, 2014.
[9] Vijay Anand Korthikanti, Mahesh Viswanathan, Gul Agha, and YoungMin Kwon. Reasoning about mdps as transformers of probability distributions. In QEST 2010, Seventh International Conference on the Quantitative Evaluation of Systems,
[10] Mathias Lechner, Dorde Zikelic, Krishnendu Chatterjee, and Thomas A. Henzinger. Stability verification in stochastic control systems via neural network supermartingales. In AAAI, pages 7326–7336. AAAI Press, 2022.
[11] Jan Obdrzálek. Fast mu-calculus model checking when tree-width is bounded. In CAV, volume 2725, pages 80–92, 2003.
[12] Xujie Si, Hanjun Dai, Mukund Raghothaman, Mayur Naik, and Le Song. Learning loop invariants for program verification. In NeurIPS, pages 7762–7773, 2018.
[13] Mikkel Thorup. All structured programs have small tree-width and good register allocation. Inf. Comput., 142(2):159–181, 1998.
[14] Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo. Compositional probabilistic model checking with string diagrams of MDPs. In CAV, pages 40–61, 2023.
[15] Dorde Zikelic, Mathias Lechner, Thomas A. Henzinger, and Krishnendu Chatterjee. Learning control policies for stochastic systems with reach-avoid guarantees. In AAAI, pages 11926–11935. AAAI Press, 2023.
[16] Dorde Zikelic, Mathias Lechner, Abhinav Verma, Krishnendu Chatterjee, and Thomas A. Henzinger. Compositional policy learning in stochastic control systems with formal guarantees. In NeurIPS, 2023.