Quantitative Evaluation of Systems

Probabilistic programs provide a convenient formalism for defining probability distributions and have numerous applications in computer science. In particular, they are used pervasively in code-based provable security for modeling security properties of cryptographic constructions as well as cryptographic assumptions. Thanks to their well-defined semantics, probabilistic programming languages provide a natural framework to prove the correctness of probabilistic computations. Probabilistic program logics are program logics that allow to reason formally about executions of probabilistic programs, and can be used to verify complex probabilistic algorithms.

Peer-to-peer swarming, as used by BitTorrent, is one of the

de facto

solutions for content dissemination in today’s Internet. By leveraging resources provided by users, peer-to-peer swarming is a simple and efficient mechanism for content distribution. In this paper we survey recent work on peer-to-peer swarming, relating content popularity to three performance metrics of such systems: fairness, content availability/ self-sustainability and scalability.

This paper studies a difference operator for stochastic systems whose specifications are represented by Abstract Probabilistic Automata (APAs). In the case refinement fails between two specifications, the target of this operator is to produce a specification APA that represents all witness PAs of this failure. Our contribution is an algorithm that allows to approximate the difference of two deterministic APAs with arbitrary precision. Our technique relies on new quantitative notions of distances between APAs used to assess convergence of the approximations as well as on an in-depth inspection of the refinement relation for APAs. The procedure is effective and not more complex than refinement checking.

Providing compact and understandable counterexamples for violated system properties is an essential task in model checking. Existing works on counterexamples for probabilistic systems so far computed either a large set of system runs or a subset of the system’s states, both of which are of limited use in manual debugging. Many probabilistic systems are described in a guarded command language like the one used by the popular model checker

PRISM

. In this paper we describe how a minimal subset of the commands can be identified which together already make the system erroneous. We additionally show how the selected commands can be further simplified to obtain a well-understandable counterexample.

Markov automata (MA) constitute an expressive continuous-time compositional modelling formalism. They appear as semantic backbones for engineering frameworks including dynamic fault trees, Generalised Stochastic Petri Nets, and AADL. Their expressive power has thus far precluded them from effective analysis by probabilistic (and statistical) model checkers, stochastic game solvers, or analysis tools for Petri net-like formalisms. This paper presents the foundations and underlying algorithms for efficient MA modelling, reduction using static analysis, and most importantly, quantitative analysis. We also discuss implementation pragmatics of supporting tools and present several case studies demonstrating feasibility and usability of MA in practice.

Probabilistic automata (

PA

) are a prominent compositional concurrency model. As a way to justify property-preserving abstractions, in the last years, bisimulation relations over

probability distributions

have been proposed both in the strong and the weak setting. Different to the usual bisimulation relations, which are defined over

states

, an algorithmic treatment of these relations is inherently hard, as their carrier set is uncountable, even for finite

PA

s. The coarsest of these relation, weak distribution bisimulation, stands out from the others in that no equivalent state-based characterisation is known so far. This paper presents an equivalent state-based reformulation for weak distribution bisimulation, rendering it amenable for algorithmic treatment. Then, decision procedures for the probability distribution-based bisimulation relations are presented.

Continuous time Markov Chains (CTMCs) are a convenient mathematical model for a broad range of natural and computer systems. As a result, they have received considerable attention in the theoretical computer science community, with many important techniques such as model checking being now mainstream. However, most methodologies start with an assumption of complete specification of the CTMC, in terms of both initial conditions and parameters. While this may be plausible in some cases (e.g. small scale engineered systems) it is certainly not valid nor desirable in many cases (e.g. biological systems), and it does not lead to a constructive approach to rational design of systems based on specific requirements. Here we consider the problems of learning and designing CTMCs from observations/ requirements formulated in terms of satisfaction of temporal logic formulae. We recast the problem in terms of learning and maximising an unknown function (the likelihood of the parameters) which can be numerically estimated at any value of the parameter space (at a non-negligible computational cost). We adapt a recently proposed, provably convergent global optimisation algorithm developed in the machine learning community, and demonstrate its efficacy on a number of non-trivial test cases.

In systems biology, an interesting problem is to analyze and characterize the oscillatory and periodic behavior of a chemical reaction system. Traditionally, those systems have been treated deterministically and continuously via ordinary differential equations. In case of high molecule counts with respect to the volume this treatment is justified. But otherwise, stochastic fluctuations can have a high influence on the characteristics of a system as has been shown in recent publications.

In this paper we develop an efficient numerical approach for analyzing the oscillatory and periodic character of user-defined observations on Markov population models (MPMs). MPMs are a special kind of continuous-time Markov chains that allow for a discrete representation of unbounded population counts for several population types and transformations between populations. Examples are chemical species and the reactions between them.

In this paper we investigate the use of Central Limit Approximation of Continuous Time Markov Chains to verify collective properties of large population models, describing the interaction of many similar individual agents. More precisely, we specify properties in terms of individual agents by means of deterministic timed automata with a single global clock (which cannot be reset), and then use the Central Limit Approximation to estimate the probability that a given fraction of agents satisfies the local specification.

We consider the Machine Repairman Model with

N

working units that break randomly and independently according to a phase-type distribution. Broken units go to one repairman where the repair time also follows a phase-type distribution. We are interested in the behavior of the number of working units when

N

is large. For this purpose, we explore the fluid limit of this stochastic process appropriately scaled by dividing it by

N

.

This problem presents two main difficulties: two different time scales and discontinuous transition rates. Different time scales appear because, since there is only one repairman, the phase at the repairman changes at a rate of order

N

, whereas the total scaled number of working units changes at a rate of order 1. Then, the repairman changes

N

times faster than, for example, the total number of working units in the system, so in the fluid limit the behavior at the repairman is averaged. In addition transition rates are discontinuous because of idle periods at the repairman, and hinders the limit description by an ODE.

We prove that the multidimensional Markovian process describing the system evolution converges to a deterministic process with piecewise smooth trajectories. We analyze the deterministic system by studying its fixed points, and we find three different behaviors depending only on the expected values of the phase-type distributions involved. We also find that in each case the stationary behavior of the scaled system converges to the unique fixed point that is a global attractor. Proofs rely on martingale theorems, properties of phase-type distributions and on characteristics of piecewise smooth dynamical systems. We also illustrate these results with numerical simulations.

We describe a novel tool for model checking

ω

-regular specifications on interval Markov chains, recursive interval Markov chains and interval stochastic context-free grammars. The core of the tool is an iterative expectation maximisation procedure to compute values for the unknown probabilities in a parametrised system, which maximises the probability of satisfying the specification. The tool supports specifications given as LTL formulas or unambiguous Büchi automata.

We present PLASMA-lab, a statistical model checking (SMC) library that provides the functionality to create custom statistical model checkers based on arbitrary discrete event modelling languages. PLASMA-lab is written in Java for maximum cross-platform compatibility and has already been incorporated in various performance-critical software and embedded hardware platforms. Users need only implement a few simple methods in a simulator class to take advantage of our efficient SMC algorithms.

PLASMA-lab may be instantiated from the command line or from within other software. We have constructed a graphical user interface (GUI) that exposes the functionality of PLASMA-lab and facilitates its use as a standalone application with multiple ‘drop-in’ modelling languages. The GUI adds the notion of projects and experiments, and implements a simple, practical means of distributing simulations using remote clients.

We present STRONG, a MATLAB toolbox for hybrid system verification. The toolbox addresses the problem of reachability/safety verification for bounded time. It simulates a finite number of trajectories and computes robust neighborhoods around their initial states such that any trajectory starting from these robust neighborhoods follows the same sequence of locations as the simulated trajectory does and avoids the unsafe set if the simulated trajectory does. Numerical simulation and computation of robust neighborhoods for linear dynamics scale well with the size of the problem. Moreover, the computation can be readily parallelized because the nominal trajectories can be simulated independently of each other. This paper showcases key features and functionalities of the toolbox using some examples.

Stochastic performance models are widely used to analyse the performance of systems that process customers and resources. However, the construction of such models is traditionally manual and therefore expensive, intrusive and prone to human error. In this paper we introduce PEPERCORN, a Petri Net Performance Model (PNPM) construction tool, which, given a dataset of raw location tracking traces obtained from a customer-processing system, automatically formulates and parameterises a corresponding Coloured Generalised Stochastic Petri Net (CGSPN) performance model.

ADTool is free, open source software assisting graphical modeling and quantitative analysis of security, using attack–defense trees. The main features of ADTool are easy creation, efficient editing, and automated bottom-up evaluation of security-relevant measures. The tool also supports the usage of attack trees, protection trees and defense trees, which are all particular instances of attack–defense trees.

Quantitative information flow analysis (QIF) is a portfolio of security techniques quantifying the flow of confidential information to public ports. In this paper, we advance the state of the art in QIF for imperative programs. We present both an abstract formulation of the analysis in terms of verification condition generation, logical projection and model counting, and an efficient concrete implementation targeting ANSI C programs. The implementation combines various novel and existing SAT-based tools for bounded model checking, #SAT solving in presence of projection, and SAT preprocessing. We evaluate the technique on synthetic and semi-realistic benchmarks.

Prinsys

(pronounced “princess”) is a new software-tool for

pr

obabilistic

in

variant

sy

nthesi

s

. In this paper we discuss its implementation and improvements of the methodology which was set out in previous work. In particular we have substantially simplified the method and generalised it to non-linear programs and invariants.

Prinsys

follows a constraint-based approach. A given parameterised loop annotation is speculatively placed in the program. The tool returns a formula that captures precisely the invariant instances of the given candidate. Our approach is sound and complete.

Prinsys

’s applicability is evaluated on several examples. We believe the tool contributes to the successful analysis of sequential probabilistic programs with infinite-domain variables and parameters.

The spectrum of branching-time relations for probabilistic systems has been investigated thoroughly by Baier, Hermanns, Katoen and Wolf (2003, 2005), including weak simulation for systems involving substochastic distributions. Weak simulation was proven to be sound w.r.t. the liveness fragment of the logic PCTL

$_{\setminus \mathcal{X}}$

, and its completeness was conjectured. We revisit this result and show that soundness does not hold in general, but only for Markov chains without divergence. It is refuted for some systems with substochastic distributions. Moreover, we provide a counterexample to completeness. In this paper, we present a novel definition that is sound for live PCTL

$_{\setminus \mathcal{X}}$

, and a variant that is both sound and complete.

A long version of this article containing full proofs is available from [11].

Data stream processing systems have become popular due to their effectiveness in applications in large scale data stream processing scenarios. This paper compares and contrasts performance characteristics of three stream processing softwares System S, S4, and Esper. We study about which software aspects shape the characteristics of the workloads handled by these software. We use a micro benchmark and different real world stream applications on System S, S4, and Esper to construct 70 different application scenarios. We use job throughput, CPU, Memory consumption, and network utilization of each application scenario as performance metrics. We observed that S4’s architectural aspect which instantiates a Processing Element (PE) for each keyed attribute is less efficient compared to the fixed number of PEs used by System S and Esper. Furthermore, all the Esper benchmarks produced more than 150% increased performance in single node compared to S4 benchmarks. S4 and Esper are more portable compared to System S and could be fine tuned for different application scenarios easily. In future we hope to widen our understanding of performance characteristics of these systems by investigating in to the code level profiling.

Modern data storage systems employ advanced erasure codes to protect data from storage node failures because of their ability to provide high data reliability at high storage efficiency. In contrast to previous studies, we consider the practical case where the length of codewords in an erasure coded system is much smaller than the number of storage nodes in the system. In this case, there exists a large number of possible ways in which different codewords can be stored across the nodes of the system. In this paper, it is shown that a declustered placement of codewords can significantly improve system reliability compared to other placement schemes. A detailed reliability analysis is presented that accounts for the rebuild times involved, the amounts of partially rebuilt data when additional nodes fail during rebuild, and an intelligent rebuild process that attempts to rebuild the most critical codewords first.

In this paper we derive fault-impact models for wireless network traffic as it could be used in the control traffic for smart grid nodes. We set up experiments using a testbed with 116 nodes which uses the protocol IEEE 802.11g. We develop models for packet loss, the length of consecutive packet loss or non-loss as well as for packet transmission time. The latter is a known challenge and we propose a sampling technique that benefits from the wireless as well as wired connections between the nodes in the testbed. The data obtained shows similarity with previous measurements. However, we progress the state of the art in two ways: we show measurements of packet transmission times and fit models to those and we provide some more detailed insight in the data. We find that with increasing link quality, the distributions of lossy and loss-free periods show major fluctuation. It is shown that in those cases, phase-type distributions can approximate the data better than traditional Gilbert models. In addition, the medium access time is also found to be approximated well with a PH distribution.

VeriSiMPL

(“very simple”) is a software tool to obtain finite abstractions of Max-Plus-Linear (MPL) models. MPL models (Sect. 2), specified in MATLAB, are abstracted to Labeled Transition Systems (LTS). The LTS abstraction is formally put in relationship with the concrete MPL model via a (bi)simulation relation. The abstraction procedure (Sect. 3) runs in MATLAB and leverages sparse representations, fast manipulations based on vector calculus, and optimized data structures such as Difference-Bound Matrices. LTS abstractions can be exported to structures defined in the PROMELA. This enables the verification of MPL models against temporal specifications within the SPIN model checker (Sect. 4). The toolbox is available at

http://sourceforge.net/projects/verisimpl/

This paper presents a library for exactly computing the bisimilarity Kantorovich-based pseudometrics between Markov chains and between Markov decision processes. These are distances that measure the behavioral discrepancies between non-bisimilar systems. They are computed by using an on-the-fly greedy strategy that prevents the exhaustive state space exploration and does not require a complete storage of the data structures. Tests performed on a consistent set of (pseudo)randomly generated instances show that our algorithm improves the efficiency of the previously proposed iterative algorithms, on average, with orders of magnitude. The tool is available as a Mathematica package library.

The Möbius modeling environment is a mature, multi-formalism modeling and solution tool. Möbius provides a user-friendly graphical interface for creating discrete-event models, defining metrics, and solving for the metrics using a variety of solution techniques. For certain research needs, the graphical interface can become a limiting use pattern. This paper describes recent work that adds a comprehensive text-based interface for interacting with the Möbius tool, called the Möbius Shell. The Möbius Shell provides an interactive command shell and scriptable command language that can leverage all the existing and future features of Möbius.

Stochastic Automata Networks (SAN) is a Markovian formalism devoted to the quantitative evaluation of concurrent systems. Unlike other Markovian formalisms and despite its interesting features, SAN does not count with the support of model checking. This paper discusses the architecture, the main features and the initial results towards the construction of a symbolic CTL Model Checker for SAN. A parallel version of this model checker is also briefly discussed.

This paper addresses a control problem for probabilistic models in the setting of Markov decision processes (

MDP

). We are interested in the

steady-state control problem

which asks, given an ergodic

MDP

$\mathcal{M}$

and a distribution

δ

goal

, whether there exists a (history-dependent randomized) policy

π

ensuring that the steady-state distribution of

$\mathcal{M}$

under

π

is exactly

δ

goal

. We first show that stationary randomized policies suffice to achieve a given steady-state distribution. Then we infer that the steady-state control problem is decidable for

MDP

, and can be represented as a linear program which is solvable in PTIME. This decidability result extends to labeled

MDP

(

LMDP

) where the objective is a steady-state distribution on labels carried by the states, and we provide a PSPACE algorithm. We also show that a related

steady-state language inclusion problem

is decidable in EXPTIME for

LMDP

. Finally, we prove that if we consider

MDP

under partial observation (

POMDP

), the steady-state control problem becomes undecidable.

Stochastic switched systems are a class of continuous-time dynamical models with probabilistic evolution over a continuous domain and control-dependent discrete dynamics over a finite set of modes. As such, they represent a subclass of general stochastic hybrid systems. While the literature has witnessed recent progress in the dynamical analysis and controller synthesis for the stability of stochastic switched systems, more complex and challenging objectives related to the verification of and the synthesis for logic specifications (properties expressed as formulas in linear temporal logic or as automata on infinite strings) have not been formally investigated as of yet. This paper addresses these complex objectives by constructively deriving approximately equivalent (bisimilar) symbolic models of stochastic switched systems. More precisely, a finite symbolic model that is approximately bisimilar to a stochastic switched system is constructed under some dynamical stability assumptions on the concrete model. This allows to formally synthesize controllers (switching signals) over the finite symbolic model that are valid for the concrete system, by means of mature techniques in the literature.

We study strategy synthesis for stochastic two-player games with multiple objectives expressed as a conjunction of LTL and expected total reward goals. For stopping games, the strategies are constructed from the Pareto frontiers that we compute via value iteration. Since, in general, infinite memory is required for deterministic winning strategies in such games, our construction takes advantage of randomised memory updates in order to provide compact strategies. We implement our methods in PRISM-games, a model checker for stochastic multi-player games, and present a case study motivated by the DARPA Urban Challenge, illustrating how our methods can be used to synthesise strategies for high-level control of autonomous vehicles.

We give an algorithm for solving stochastic parity games with almost-sure winning conditions on

lossy channel systems

, for the case where the players are restricted to finite-memory strategies. First, we describe a general framework, where we consider the class of

$2\frac{1}{2}$

-player games with almost-sure parity winning conditions on possibly infinite game graphs, assuming that the game contains a

finite attractor

. An attractor is a set of states (not necessarily absorbing) that is almost surely re-visited regardless of the players’ decisions. We present a scheme that characterizes the set of winning states for each player. Then, we instantiate this scheme to obtain an algorithm for

stochastic game lossy channel systems

.

Stochastic Timed Automata (STA) associate logical locations with continuous, generally distributed sojourn times. In this paper, we introduce Networks of Stochastic Timed Automata (NSTA), where the components interact with each other by message broadcasts. This results in an underlying stochastic process whose state is made of the vector of logical locations, the remaining sojourn times, and the value of clocks. We characterize this general state space Markov process through transient stochastic state classes that sample the state and the absolute age after each event. This provides an algorithmic approach to transient analysis of NSTA models, with fairly general termination conditions which we characterize with respect to structural properties of individual components that can be checked through straightforward algorithms.

We introduce an automated approach for applying rare event simulation to stochastic Petri net (SPN) models of highly reliable systems. Rare event simulation can be much faster than standard simulation because it is able to exploit information about the typical behaviour of the system. Previously, such information came from heuristics, human insight, or analysis on the full state space. We present a formal algorithm that obtains the required information from the high-level SPN-description, without generating the full state space. Essentially, our algorithm reduces the state space of the model into a (much smaller) graph in which each node represents a set of states for which the most likely path to failure has the same form. We empirically demonstrate the efficiency of the method with two case studies.

The performance and reliability of wireless network protocols heavily depend on the network and its environment. In wireless networks node mobility can affect the overall performance up to a point where, e.g. route discovery and route establishment fail. As a consequence any formal technique for performance analysis of wireless network protocols should take node mobility into account. In this paper we propose a topology-based mobility model, that abstracts from physical behaviour, and models mobility as probabilistic changes in the topology. We demonstrate how this model can be instantiated to cover the main aspects of the random walk and the random waypoint mobility model. The model is not a stand-alone model, but intended to be used in combination with protocol models. We illustrate this by two application examples: first we show a brief analysis of the Ad-hoc On demand Distance Vector (AODV) routing protocol, and second we combine the mobility model with the Lightweight Medium Access Control (LMAC).