Model checking stochastic hybrid systems

Abstract

The interplay of random phenomena with discrete-continuous dynamics deserves increased attention in many systems of growing importance. Their verification needs to consider both stochastic behaviour and hybrid dynamics. In the verification of classical hybrid systems, one is often interested in deciding whether unsafe system states can be reached. In the stochastic setting, we ask instead whether the probability of reaching particular states is bounded by a given threshold. In this thesis, we consider stochastic hybrid systems and develop a general abstraction framework for deciding such problems. This gives rise to the first mechanisable technique that can, in practice, formally verify safety properties of systems which feature all the relevant aspects of nondeterminism, general continuous-time dynamics, and probabilistic behaviour. Being based on tools for classical hybrid systems, future improvements in the effectiveness of such tools directly carry over to improvements in the effectiveness of our technique. We extend the method in several directions. Firstly, we discuss how we can handle continuous probability distributions. We then consider systems which we are in partial control of. Next, we consider systems in which probabilities are parametric, to analyse entire system families at once. Afterwards, we consider systems equipped with rewards, modelling costs or bonuses. Finally, we consider all orthogonal combinations of the extensions to the core model.

In vielen Systemen wachsender Bedeutung tritt zufallsabhängiges Verhalten gleichzeitig mit diskret-kontinuierlicher Dynamik auf. Um solche Systeme zu verifizieren, müssen sowohl ihr stochastisches Verhalten als auch ihre hybride Dynamik betrachtet werden. In der Analyse klassischer hybrider Systeme ist eine wichtige Frage, ob unsichere Zustände erreicht werden können. Im stochastischen Fall fragen wir stattdessen nach garantierten Wahrscheinlichkeitsschranken. In dieser Arbeit betrachten wir stochastische hybride Systeme und entwickeln eine allgemeine Abstraktionsmethode um Probleme dieser Art zu entscheiden. Dies ermöglicht die erste automatische und praktisch anwendbare Methode, die Sicherheitseigenschaften von Systeme beweisen kann, in denen Nichtdeterminismus, komplexe Dynamik und probabilistisches Verhalten gleichzeitig auftreten. Da die Methode auf Analysetechniken für nichtstochastische hybride Systeme beruht, profitieren wir sofort von zukünftigen Verbesserungen dieser Verfahren. Wir erweitern diese Grundmethode in mehrere Richtungen: Zunächst ergänzen wir das Modell um kontinuierliche Wahrscheinlichkeitsverteilungen. Dann betrachten wir partiell kontrollierbare Systeme. Als nächstes untersuchen wir parametrische Systeme, um eine Klasse ähnlicher Modelle gleichzeitig behandeln. Anschließend betrachten wir Eigenschaften, die auf der Abwägung von Kosten und Nutzen beruhen. Schließlich zeigen wir, wie diese Erweiterungen orthogonal kombiniert werden können.