Refined Probabilistic Abstraction

Abstract

Network technology enables smarter and more adaptive computing devices in the context of vehicles, communication and energy networks. Performance and quality-of-service guarantees are vital concerns for such systems. Meaningful guarantees are typically of a probabilistic nature due to the use of randomized algorithms inside network protocols and other phenomena like message loss. Probabilistic verification provides methods and tools to quantify the performance and quality of service of systems. A central problem in probabilistic verification is to determine the probability that a system enters a particular set of goal states, e.g., states in which packages have been transmitted successfully. Despite the remarkable versatility of existing methods, they are inherently limited to systems with very small state spaces. This dissertation proposes new methods that solve the problem of probabilistic reach- ability for large or even infinite state spaces. The key is to automatically obtain small abstractions of a system. To this end, we start with a very coarse abstraction and successively refine it. The process is fully automatic and has been implemented in the tool Pass. Pass achieves significant performance improvements compared to previous methods and, further, applies to infinite-state systems which could previously not be handled by any existing automatic method.