Validation of Stochastic Systems

We survey various notions of probabilistic automata and probabilistic bisimulation, accumulating in an expressiveness hierarchy of probabilistic system types. The aim of this paper is twofold: On the one hand it provides an overview of existing types of probabilistic systems and, on the other hand, it explains the relationship between these models. We overview probabilistic systems with discrete probabilities only. The expressiveness order used to built the hierarchy is defined via the existence of mappings between the corresponding system types that preserve and reflect bisimilarity. Additionally, we discuss parallel composition for the presented types of systems, augmenting the map of probabilistic automata with closedness under this compositional operator.

We report on the state of the art in the formal specification and analysis of concurrent systems whose activity duration depends on general probability distributions. First of all the basic notions and results introduced in the literature are explained and, on this basis, a conceptual classification of the different approaches is presented. We observe that most of the approaches agree on the fact that the specification of systems with general distributions has a three level structure: the process algebra level, the level of symbolic semantics and the level of concrete semantics. Based on such observations, a new very expressive model is introduced for representing timed systems with general distributions. We show that many of the approaches in the literature can be mapped into this model establishing therefore a formal framework to compare these approaches.

In order to describe probabilistic processes by means of a formal model, some considerations have to be taken into account. In this paper we present some of the ideas appeared in the literature that could help to define appropriate formal frameworks for the specification of probabilistic processes. First, we will explain the different interpretations of the probabilistic information included in this kind of models. After that, the different choice operators used in the most common probabilistic languages are enumerated. Once we have an appropriate language, we have to give its semantics. Thus, we will review some of the theories based on bisimulation and testing semantics. We will conclude by studying the extensions of the chosen languages with other operators such as parallel composition and hiding.

In this chapter, we present procedures for checking linear temporal logic and automata specifications of sequential and concurrent probabilistic programs. We follow two different approaches: For LTL and sequential probabilistic programs, our method proceeds in a tableau style fashion, while the remaining procedures are based on automata theory.

In this survey we motivate, define and explain model checking of probabilistic deterministic and nondeterministic systems using the probabilistic computation tree logics PCTL and PCTL ^*. Juxtapositions to non-deterministic computation tree logic are made and algorithms are presented.

Application areas such as multimedia equipment, communication protocols and networks often feature systems which exhibit both probabilistic and timed behaviour. In this paper, we consider analysis of such probabilistic timed systems using the technique of model checking, in which it is verified automatically whether a system satisfies a certain desired property. In order to describe formally probabilistic timed systems, we consider probabilistic extensions of timed automata, such as real-time probabilistic processes, probabilistic timed automata and continuous probabilistic timed automata, the underlying semantics of each of which is an infinite-state structure. For each formalism, we consider how the well-known region equivalence relation can be used to reduce the infinite state-space model into a finite-state system, which can then be used for model checking.

The paper presents a survey of out-of-core methods available for the analysis of large Markov chains on single workstations. First, we discuss the main sparse matrix storage schemes and review iterative methods for the solution of systems of linear equations typically used in disk-based methods. Next, various out-of-core approaches for the steady state solution of CTMCs are described. In this context, serial out-of-core algorithms are outlined and analysed with the help of their implementations. A comparison of time and memory requirements for typical benchmark models is given.

State-based analysis of discrete event systems notoriously suffers from the largeness of state spaces, which often grow exponentially with the size of the model. Since non-trivial models tend to be built by submodels in some hierarchical or compositional manner, one way to achieve a compact representation of the associated state-transition system is to use Kronecker representations that accommodate the structure of a model at the level of a state transition system. In this paper, we present the fundamental idea of Kronecker representation and discuss two different kinds of representations, namely modular representations and hierarchical representations. Additionally, we briefly outline how the different representations can be exploited in efficient analysis algorithms.

This paper describes symbolic techniques for the construction, representation and analysis of large, probabilistic systems. Symbolic approaches derive their efficiency by exploiting high-level structure and regularity in the models to which they are applied, increasing the size of the state spaces which can be tackled. In general, this is done by using data structures which provide compact storage but which are still efficient to manipulate, usually based on binary decision diagrams (BDDs) or their extensions. In this paper we focus on BDDs, multi-valued decision diagrams (MDDs), multi-terminal binary decision diagrams (MTBDDs) and matrix diagrams.

Several methods have been developed to validate the correctness and performance of hard- and software systems. One way to do this is to model the system and carry out a state space exploration in order to detect all possible states. In this paper, a survey of existing probabilistic state space exploration methods is given. The paper starts with a thorough review and analysis of bitstate hashing, as introduced by Holzmann. The main idea of this initial approach is the mapping of each state onto a specific bit within an array by employing a hash function. Thus a state is represented by a single bit, rather than by a full descriptor. Bitstate hashing is efficient concerning memory and runtime, but it is hampered by the non deterministic omission of states. The resulting positive probability of producing wrong results is due to the fact that the mapping of full state descriptors onto much smaller representatives is not injective. – The rest of the paper is devoted to the presentation, analysis, and comparison of improvements of bitstate hashing, which were introduced in order to lower the probability of producing a wrong result, but maintaining the memory and runtime efficiency. These improvements can be mainly grouped into two categories: The approaches of the first group, the so called multiple hashing schemes, employ multiple hash functions on either a single or on multiple arrays. The approaches of the remaining category follow the idea of hash compaction. I.e. the diverse schemes of this category store a hash value for each detected state, rather than associating a single or multiple bit positions with it, leading to persuasive reductions of the probability of error if compared to the original bitstate hashing scheme.

Randomization is of paramount importance in practical applications and randomized algorithms are used widely, for example in co-ordinating distributed computer networks, message routing and cache management. The appeal of randomized algorithms is their simplicity and elegance. However, this comes at a cost: the analysis of such systems become very complex, particularly in the context of distributed computation. This arises through the interplay between probability and nondeterminism. To prove a randomized distributed algorithm correct one usually involves two levels: classical, assertion-based reasoning, and a probabilistic analysis based on a suitable probability space on computations. In this paper we describe a number of approaches which allows us to verify the correctness of randomized distributed algorithms.

We study abstraction techniques for model checking systems that combine non-deterministic with probabilistic behavior, emphasizing the discrete case. Existing work on abstraction offers a host of isolated techniques which we discuss uniformly through the formulation of abstracted model-checking problems (MCPs). Although this conceptualization is primarily meant to be a useful focal point for surveying the literature on abstraction-based model checking even beyond such combined systems, it also opens up new research opportunities and challenges for abstract model checking of mixed systems. In particular, we sketch how quantitative domain theory may be used to specify the precision of answers obtained from abstract model checks.

Lossy channel systems (LCS’s) are systems of finite state automata that communicate via unreliable unbounded fifo channels. Several probabilistic versions of these systems have been proposed in recent years, with the two aims of modeling more faithfully the losses of messages, and circumventing undecidabilities by some kind of randomization. We survey these proposals and the verification techniques they support.