Symbolic Algorithms for the Analysis of Quantitative Systems

Modern infrastructure is increasingly governed by complex, software-driven systems whose failure can have severe consequences. Formal methods offer a rigorous framework for analyzing the reliability and correctness of such systems.

In this thesis, we focus specifically on the analysis of quantitative transition systems. These are systems where states and transitions carry values (e.g., probabilities), enabling the analysis of not only whether certain outcomes are possible but also, for example, how likely they are. This includes applications in probabilistic safety analysis and quantum computing.

However, analyzing such systems is computationally difficult due to the exponential growth of the state space. To tackle this hurdle, people have turned to symbolic algorithms, which aim to represent and manipulate large state spaces efficiently without explicitly enumerating them. We particularly focus on decision diagrams (DDs) and satisfiability solving (SAT).

In this thesis, we make contributions in three different directions. We improve the scalability of DD and SAT-based approaches in various settings. We study the issues caused by floating-point imprecision in DDs, and provide mitigation strategies. And we investigate how DDs can contribute to the efficient discretization of continuous domains.