Automated Reasoning For Uncertain Markov Processes

Markov processes are a ubiquitous modeling tool used to model a variety of probabilistic phenomena across a range of disciplines. In this thesis, we develop algorithms for studying Markov processes using tools from the field of automated reasoning. First, we tackle a variant of sensitivity analysis, where we want to obtain all possible parameters for a Markov process such that the total reward achieves a fixed threshold. The set of such parameters forms a semialgebraic set, and so we use cylindrical algebraic decomposition, an algorithm developed for the existential theory of the reals, to describe this set. By exploiting properties of our polynomial system, we develop a variant that runs in singly exponential time, instead of the doubly exponential complexity in the general case. Next, we study properties of Markov processes where the parameters are functions, given as machine learning models, of exogenous variables. Using ideas from formal verification of machine learning models and probabilistic model checking, we show how to obtain guaranteed bounds on the behavior of such processes. For a wide selection of machine learning models, we show that obtaining such guarantees is equivalent to solving a bilinear program, which are classically NP-hard problems. We develop a special decomposition algorithm that solves the bilinear program orders-of-magnitude faster than state-of-the-art solvers. Our algorithmic developments are implemented in two software packages: markovag, which implements our variant of cylindrical algebraic decomposition; and markovml, which provides a domain-specific language for constructing Markov processes, embedding pretrained machine learning models, and then solving the resulting bilinear program with our decomposition scheme. Lastly, we perform a comprehensive cost-effectiveness analysis using data from nearly 25,000 real cardiac arrests in Ontario, Canada. Using drones to deliver defibrillators to the site of cardiac arrests has been trialled, but a cost-effectiveness analysis has been lacking. Our detailed analysis shows that drones are a cost-effective solution, and our findings are robust to modeling assumptions. The richness of this analysis makes it a fertile case study for our novel algorithms, and we show how our techniques provide deeper insights than usual cost-effectiveness methods.

Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.