Decision algorithms for probabilistic simulations

Abstract

Probabilistic phenomena arise in embedded, distributed, networked, biological and security systems, and are accounted for by various probabilistic modeling formalisms based on labelled transition systems. Among the most popular ones are homogeneous discretetime and continuous-time Markov chains (DTMCs and CTMCs) and their extensions with nondeterminism, which we will consider in this thesis. Simulation relations admit comparing the behavior of two models and provide the principal ingredients to perform abstractions of the models while preserving interesting properties. Intuitively, one model simulates another model if it can imitate all of its moves. Simulation preorders are compositional, thus allowing hierarchical verification and decomposition of difficult verification tasks into several subproblems. Recently, variants of simulation relations, such as simulatability and polynomially accurate probabilistic simulations, have been introduced to prove soundness of security protocols. The focus of this thesis lies in decision algorithms for various simulation preorders of probabilistic systems. We propose efficient decision algorithms and provide also experimental comparisons of these algorithms.

In einem breiten Spektrum von Systemen, etwa bei eingebetteten, verteilten, netzwerkbasierten und biologischen System sowie im Bereich Security, treten Phänomene auf, die sich sehr gut durch Probabilismus beschreiben lassen. Als Modellierungsformalismus dienen dabei verschiedene probabilistische Erweiterungen von Transitionssystemen. Zu den wohl populärsten Formalismen dieser Art zählen hier homogene Markovketten (Markov chains) mit diskreter Zeit und Markovketten mit kontinuierlicher Zeit, bzw. deren Erweiterungen mit Nichtdeterminismus. Genau diese Klasse von Modellen betrachten wir in dieser Dissertation. Simulationsrelationen erlauben es, das Verhalten zweier Modelle in Beziehung zu setzen und liefern den grundlegenden Baustein, um Abstraktionen so zu betreiben, daß interessante Eigenschaften erhalten bleiben. Intuitiv gesprochen simuliert ein Modell ein anderes, wenn es alle Zustandsübergänge des anderen imitieren kann. Derartige Simulationsordnungen sind kompositional, daher erlauben sie hierarchische Verifikation und Zerlegung von Verifikationsaufgaben in kleinere Unterprobleme. Kürzlich wurden Simulationsrelationen eingeführt, wie etwa Simulatability und Polynomiell Akkurate Probabilstische Simulationen, um Korrektheit von Sicherheitsprotokollen zu zeigen. Der Schwerpunkt dieser Dissertation liegt auf Entscheidungsalgorithmen für verschiedene Simulationsordnungen auf probabilistischen Systemen. Wir stellen neue, effiziente Entscheidungsalgorithmen vor und vergleichen diese in Experimenten mit existierenden Algorithmen.