Symbolic algorithms for the analysis of quantitative systems

Abstract

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 on quantitative transition 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). We investigate three challenges.

First is improving the scalability of DD and SAT-based approaches. We make four contributions towards addressing this challenge. We present a novel DD algorithm for analyzing reachability in transition systems that avoids large intermediate DDs. Unlike the state-of-the-art algorithm, which only works for partitioned transition systems, our new algorithm can analyze monolithic transition systems. We also develop a parallel implementation of edge-valued DDs (that are used for analyzing quantum systems), which shows significant performance gains compared to previous work.

When using a SAT-based approach to tackle the analysis of quantum graph states, we show that over-constraining the formulas using domain-specific knowledge leads to orders-of-magnitude improvement.

We also show how Grover's quantum search algorithm can be used to speed up PPSZ---the best-known asymptotic algorithm for SAT-solving---in both a purely quantum setting as well as a hybrid-quantum classical setting. The second challenge is handling floating-point imprecision in DDs, which can compromise both performance and correctness in DD computations. Towards this challenge, we present an in-depth study on the effect of numerical imprecision in computations that use multi-terminal binary DDs. This study includes theoretical bounds, an empirical case study, and practical mitigation strategies. In the third challenge, we investigate how DDs can contribute to the efficient discretization of continuous domains. To this end, we evaluate the encoding of continuous Bayesian networks into DDs using various discretization methods. We demonstrate that high-quality discretizations are achievable with manageable computational costs, and that our DD-based approach often outperforms traditional inference methods.