ABSTRACT. We consider the problem of bounding mean first passage times and reachability probabilities for the class of population continuous-time Markov chains, which capture stochastic interactions between groups of identical agents. The quantitative analysis of such models is notoriously difficult since typically neither state-based numerical approaches nor methods based on stochastic sampling give efficient and accurate results. Here, we propose a novel approach that leverages techniques from martingale theory and stochastic processes to generate constraints on the statistical moments of first passage time distributions. These constraints induce a semi-definite program that can be used to compute exact bounds on reachability probabilities and mean first passage times without numerically solving the transient probability distribution of the process or sampling from it. We showcase the method on some test examples and tailor it to models exhibiting multimodality, a class of particularly challenging scenarios from biology.

[presentation video]. [preprint].

ABSTRACT. Phase Type Distributions (PHDs) and Markovian Arrival Processes (MAPs) are established models in computational probability to describe random processes in stochastic models. In this paper we extend MAPs to Multi-Dimensional MAPs (MDMAPs) which are a model for random vectors that may be correlated in different dimensions. The computation of different quantities like joint moments or conditional densities is introduced and a first approach to compute parameters with respect to measured data is presented.

[presentation video]. [preprint].

ABSTRACT. There is an imminent demand to understand the relationship between correctness and performance to deliver highly scalable multiprocessor programs. The motivation for this relationship is that relaxed correctness conditions provide performance benefits by reducing contention on data structure hot spots. Previous approaches propose metrics for characterizing relaxed correctness conditions that measure the number of method calls or state transitions to be shifted to arrive at a legal sequential history. The reason the existing metrics cannot measure the performance effects of a correctness condition is that they ignore delays in method calls since delayed responses from method calls yield correct behavior in even the strictest correctness conditions. We observe that method call delays can be captured by measuring the disorder in method call ordering using a metric from information theory known as entropy. We propose entropy as the first metric for multiprocessor programs that evaluates the trade-offs between correctness and performance. We measure entropy for a variety of concurrent stacks, queues, and sets from the Synchrobench micro-benchmark suite and correlate entropy, correctness, and performance. Our main insight is that lower entropy corresponds to better performance for strict correctness conditions and higher entropy corresponds to better performance for relaxed correctness conditions.

[presentation video].

ABSTRACT. This paper presents the formal modelling and verification of the Ad-hoc On-demand Distance Vector (AODV) routing protocol. Our study focuses on the quantitative aspects of AODV, in particular the influence of uncertainty (such as packet loss rates, collisions) on the probability to establish short routes. We present a compositional model of AODV's functionality using probabilistic timed automata. The strength of this model is that it combines hard real-time constraints with randomised protocol behaviour and can deal with non-determinism (due to e.g., queue behaviours at network nodes). An automated analysis by probabilistic model checking provides useful insights on the sensitivity of AODV's ability to establish shortest/longest routes and deliver data packets via such routes.

[presentation video].

ABSTRACT. For nondeterministic and probabilistic processes, the validity of some desirable properties of probabilistic trace semantics depends both on the class of schedulers used to resolve nondeterminism and on the capability of suitably limiting the power of the considered schedulers. Inclusion of probabilistic bisimilarity, compositionality with respect to typical process operators, and backward compatibility with trace semantics over fully nondeterministic or fully probabilistic processes, can all be achieved by restricting to coherent resolutions of nondeterminism. Here we provide alternative characterizations of probabilistic trace post-equivalence and pre-equivalence in the case of coherent resolutions. The characterization of the former is based on fully coherent trace distributions, whereas the characterization of the latter relies on coherent weighted trace sets.

[presentation video].

ABSTRACT. This paper applies probabilistic model checking techniques for discrete Markov chains to inference in Bayesian networks. We present a simple translation from Bayesian networks into tree-like Markov chains such that inference can be reduced to computing reachability probabilities. Using a prototypical implementation on top of the Storm model checker, we show that symbolic data structures such as multi-terminal BDDs (MTBDDs) are very effective to perform inference on large Bayesian network benchmarks. We compare our result to inference using sentential decision diagrams and vtrees, a scalable symbolic technique in AI inference tools.

[presentation video]. [preprint].

ABSTRACT. As distributed systems dramatically grow in terms of scale, complexity, and usage, understanding the hidden interactions among system and workload properties becomes an exceedingly difficult task. Machine learning models for prediction of system behavior (and analysis) are increasingly popular but their effectiveness in answering what and why is not always the most favorable. In this talk I will present two reliability analysis studies from two large, distributed systems: one that looks into GPGPU error prediction at the Titan, a large scale high-performance-computing system at ORNL, and one that analyzes the failure characteristics of solid state drives at a Google data center and hard disk drives at the Backblaze data center. Both studies illustrate the difficulty of untangling complex interactions of workload characteristics that lead to failures and of identifying failure root causes from monitored symptoms. Nevertheless, this difficulty can occasionally manifest in spectacular results where failure prediction can be dramatically accurate.