Automated Reasoning about Infinite Families of Stochastic Systems (InFamoSS)

• Applicant: Professor Dr. Christoph Matheja
• Subject Area: Theoretical Computer Science
• Term: since 2026
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 569960716

Large and highly configurable systems like networks, energy grids, or software product lines are fraught with uncertainty because their functional and non-functional behavior cannot be precisely specified. To analyze and optimize their performance, security, privacy, costs, and resource usage, one often describes such systems as Markovian models, which use probabilities to represent uncertainty. Probabilistic model checking is a popular push-button technique that provides provable guarantees on the expected behavior of Markovian models. Since assigning probabilities to complex system actions is also uncertain, it is common to consider Markovian families, that is, sets of Markovian models that cover different scenarios. Existing analysis techniques for Markovian families focus on sets of models that are (a) identical except for the chosen probabilities or (b) represent a selection of features of an all-in-one model with a fixed structure. However, the structure of realistic systems can dynamically change or even grow over time. For example, new clients may join a network or energy grid and request new features. To reason about such systems, one thus needs to consider infinite families of Markovian models whose underlying structure can evolve. The main objective of the project InFamoSS is to develop novel verification methods for the quantitative analysis of infinite families of Markovian models with changing state spaces. To this end, we will treat Markovian families as graph languages and use graph grammars to control how the topology of a family evolves. We will then develop sound algorithms and tools that compositionally analyze the rules of such graph grammars to reason about all family members simultaneously. Those techniques will leverage and combine the rich theory on graph languages and recent advances in certificates for reasoning about properties of probabilistic systems, such as quantitative invariants and supermartingales.

• DFG Programme: Research Grants
• International Connection: Denmark
• Cooperation Partner: Professor Dr. Alberto Lluch-Lafuente