QUANTITATIVE MODEL CHECKING OF DISTRIBUTED PROBABILISTIC SYSTEMS

Abstract

Complex systems are prevalent in modern society. From software and hardware to other real-life processes, the systems are often inherently large, distributed in nature, and exhibit quantifiable qualities.

Our increasing reliance on such systems mandates not only ensuring correctness of the system but also rigorous quantitative analysis. For example for a pizza company preparing and delivering hundreds of pizzas everyday, it is not only important to ensure that every pizza ordered eventually gets delivered, but also analyze claims such as 'most of the orders in a given day are delivered within the deadline'.

This thesis focuses on using model checking techniques for performance evaluation of such real-life systems. We propose a general framework for distributed stochastic models which can be adopted to model various real-life systems that exhibit concurrency, probability and various quantitative aspects such as time and cost.

We also illustrate resource-constrained processes that can be used to model the workflow of operational processes. We then restrict the model to exclude nondeterminism and showcase how that paves the way for a succinct distributed representation of finite state Markov chains.