This talk will be about the design of a distributed algorithm to monitor the availability of nodes in self-configuring networks. It is intended as extension to service discovery protocols such as SSDP, SLP, Rendezvous and Jini that allow for fast node detection. The simple scheme to regularly probe a node---"are you still there?"---may easily lead to over- or underloading. The essence of our algorithm is therefore to automatically adapt the probing frequency. We show that a self-adaptive scheme to control the probe load, originally proposed as an extension to the UPnP (Universal Plug and Play) standard, leads to an unfair treatment of nodes: some nodes probe fast while others almost starve. An alternative distributed algorithm is proposed that overcomes this problem and that tolerates highly dynamic network topology changes. The algorithm is very simple and can be implemented on large networks of small computing devices such as mobile phones, PDAs, and so on. The distributed algorithms are modeled using the formal modeling language MoDeST and are analyzed by means of the discrete-event simulator of the Mobius tool.
In an anonymous ring, where nodes do not have unique identities, no terminating algorithm for leader election exists. Probabilities can be used to break the symmetry in anonymous rings. Probabilistic leader election algorithms for anonymous rings are presented, based on an earlier algorithm from Itai and Rodeh. We used the probabilistic model checker PRISM to verify, for rings up to size four, that eventually a unique leader is elected with probability one.
Markovian models have been used for about a century now for the evaluation of the performance and dependability of computer and communication systems. In this paper, we give a concise overview of the most widely used classes of Markovian models, their solution and application. After a brief introduction to performance and dependability evaluation in general, we introduce discrete-time Markov chains, continuous-time Markov chains and semi-Markov chains. Stepwisely, we develop the main equations that govern the steady-state and the transient behaviour of such Markov chains. We thereby emphasise on intuitively appealing explanations rather than on mathematical rigor. The relation between the various Markov chain types is explained in detail. Then, we discuss means to numerically solve the systems of linear equations (both direct and iterative ones) and the systems of differential equations that arise when solving for the steady-state and transient behaviour of Markovian models.
The talk considers algorithms for counterexample generation of bounded and unbounded probabilistic reachability properties in fully probabilistic systems. We consider two problems that are aimed to provide useful diagnostic feedback for the violation: generating strongest evidences and smallest, most indicative counterexamples. Finding a strongest evidence (i.e., the most probable path) violating (bounded) until formula is shown to be reducible to a single-source (hop-constrained) shortest path problem. Counterexamples of smallest size that are mostly deviating from the requited probability bound can be computed by adopting (partially new hop-constrained) k shortest paths algorithms that dynamically determine k.
We present an in-depth treatment of model checking algorithms for a class of infinite-state continuous-time Markov chains known as quasi-death processes. The model class is described in detail, as well as the logic CSL to express properties of interest. Using a new property-independent concept, we provide model checking algorithms for all CSL operators. Special emphasis is given to the time-bounded until operator for which we have developed a new and efficient computational procedure named uniformization with representatives. By the use of an application-driven dynamic stopping criterion the algorithm stops whenever the property to be checked can be certified (or falsified). A comprehensive case study of a connection management system shows the versatility of our new algorithms.
Joint work with Boudewijn Haverkort and Lucia Cloth.
A silent step in a dynamic system is a step that is considered unobservable and that can be eliminated. We define a Markov chain with silent steps as a class of Markov chains parameterized with a real variable tau. When tau goes to infinity silent steps become immediate, i.e. timeless, and therefore unobservable. To facilitate the elimination of these steps while preserving performance measures, we introduce a notion of lumping for the new setting. To justify the lumping we first extend the standard notion of ordinary lumping to the setting of discontinuous Markov chains, processes that can do infinitely many transitions in finite time. Then, we give a direct connection between the two lumpings for the case when tau is infinite. The results of this paper can serve as a correctness criterion and a method for the elimination of silent tau steps in Markovian process algebras.
Continuous-Time Markov Chains (CTMCs) have shown to be applicable for performance and dependability evaluation. The most recent approach to analyse CTMCs is checking them for properties formulated in the Continuous Stochastic Logic (CSL). Efficient algorithms for CSL-model-checking of CTMCs have been developed several years ago and there is a solid tool support (Prism, MRMC, ...). One of the most important problems nowadays is how to handle state spaces of real life models. Since engineers usually do not want to describe their models on a Markov chain level but in some high-level modeling language (production rule systems, Petri nets, ...) and since deriving CTMCs from high-level models usually result in a state space explosion, rather simple high-level models may yield huge and even infinite state spaces in the underlying Markov chain.
We will discuss simple Petri net examples and show, how infinite state spaces of the underlying CTMCs can get abstracted such that we only have to deal with finite state spaces. In contrast to the given infinite CTMCs where standard model checking techniques are not applicable, those abstractions are suitable for model checking an important subset of CSL. The downside of this approach is that loss of information may occur, possibly yielding indefinite results when applying (adapted) model checking.
StoCharts, a slight variant of UML StateCharts, serve to model a specific kind of stochastic system, namely generalised semi-Markov decision processes. The session will introduce StoCharts interactively with some examples and show how they can be analysed using model-checking and simulation.
This talk focuses on probabilistic transition systems or probabilistic automata. In the literature there exist many different types of probabilistic automata. Most of them can be viewed as some sort of labelled transition systems enriched with probabilistic information.
We will give an overview and an expressiveness comparison of various probabilistic models with respect to strong bisimilarity semantics. In the background of the expressiveness result, as well as in the presentation of the systems, there is the theory of coalgebras providing a unified framework for treating various dynamic systems. We will also briefly discuss other behavior equivalences rather than bisimilarity.
This talk presents an algorithm for cost-bounded probabilistic reachability in timed automata extended with prices (on edges and locations) and discrete probabilistic branching. The algorithm determines whether the probability to reach a (set of) goal location(s) within a given price bound (and time bound) can exceed a threshold p in [0,1]. We prove that the algorithm is partially correct and show an example for which termination cannot be guaranteed.
One of the hallmarks of process theory is the notion of abstraction. Abstractions allow one to reason about systems in which details, unimportant to the purposes at hand, have been hidden. It is an invaluable tool when dealing with complex systems. Research in process theory has made great strides in coping with abstraction in areas that focus on functional behaviours of systems. However, when it comes to theories focusing on functional behaviours and extra-functional behaviours, such as probabilistic behaviour, we suddenly find that many issues are still unresolved.
This talk will addresses abstraction in the setting of systems that have both non-deterministic and probabilistic traits, referred to as probabilistic systems. The model that is use to describe such systems is that of graphs that adhere to the strictly alternating regime as studied by Hansson [1]. In particular, I will discuss the notion of branching bisimilarity for this model.
The need for this particular equivalence relation is already convincingly argued by e.g. Van Glabbeek and Weijland in [2], and by Groote and Vaandrager in [3]. It is interesting that in the alternating model for probabilistic systems, branching bisimilarity can be given two alternative characterizations, as a coloured trace equivalence and a branching bisimilarity using maximal probabilities. The alternative characterizations have their own merits and focus on different aspects of branching bisimilarity.
Van Glabbeek and Weijland showed that a key property of branching bisimilarity is that it preserves the branching structure of processes, i.e. it preserves computations together with the potentials in all intermediate states of a system that are passed through, even when unobservable events are involved. Roughly speaking, the potentials are the options the system has to branch and behave. This property sets branching bisimilarity apart from weak bisimilarity, which does not have the property. They illustrated this property by defining coloured trace equivalence (in a setting with abstraction), which uses colours to code for the potentials. They showed that branching bisimilarity and coloured trace equivalence coincide, and both are strictly finer than weak bisimilarity.
Although the probabilistic setting is considerably more complex than the non-probabilistic setting, the key concept of preservation of potentials should still hold. It is shown that this is indeed the case by defining probabilistic counterparts of coloured trace equivalence which coincides with branching bisimilarity. A major advantage of coloured trace equivalence is that it can be understood without knowledge of probability theory and without appealing to schedulers.
Another property of branching bisimilarity, is the preservation of maximal probabilities. Thus, branching bisimilarity can be rephrased in terms of such maximal probabilities, thus yielding another alternative definition of branching bisimulation. Apart from the more appetizing phrasing that this yields, this result is also at the basis of the complexity results for deciding branching bisimilarity. We also provide the algorithm for deciding branching bisimilarity.
The branching bisimularity (in the alternating model) can be completely axiomatized. The completeness result is only for closed (recursion free) expressions. In addition to the axioms, a set of sound verification rules has been identified. The verification rules are sound with respect to the branching bisimulation and can be used to remove inert transitions and loops. Thus, the process algebra comprising the axioms and the verification rules can be used for specifying, as well as for verifying, probabilistic systems.
| [1] | H. Hansson, Time and probability in formal design of distributed systems, Ph.D.thesis, University of Uppsala (1991) |
| [2] | R. van Glabbeek, W. Weijland, Branching time and abstraction in bisimulation semantics, Journal of the ACM 43 (3) (1996) 555--600 |
| [3] | J. Groote, F. Vaandrager, An efficient algorithm for branching bisimulation and stuttering equivalence in: M.Paterson (Ed.), Proceedings 17th ICALP, Warwick, Vol. 443 of LNCS, Springer-Verlag, 1990, pp. 626--638. |
We present a stochastic process algebra including immediate actions, deadlock and termination, and explicit stochastic delays, in the setting of weak choice between immediate actions and passage of time. The operational semantics is a spent time semantics, avoiding explicit clocks. We discuss the embedding of weak-choice real-time process theories and analyze the behavior of parallel composition in the weak choice framework.
This talk presents MoDeST (MOdeling and DEscription language for Stochastic Timed systems), a formalism to support (i) the modular description of reactive systems' behavior while covering both (ii) functional and (iii) nonfunctional system aspects such as timing and quality-of-service constraints in a single specification.
This unique expressiveness has been exploited in three recent industrial case studies of rather different nature, ranging from (i) schedule synthesis and evaluation for a lacquer production plant, to (ii) device detection in a plug-and-play infotainmentprotocol, and to (iii) dependability assessment of an emerging standard for future high-speed cross-European trains. The talk describes the design rationales and details of syntax, semantics and tool support, and the above case studies.
Joint work with H.C. Bohnenkamp, P.R. D'Argenio, J.P. Katoen, A. Mader, D.N. Jansen, Y. Usenko
One feature that characterizes systems is their design. For embedded computer systems (which are computer systems ‘embedded’ in e.g.
telephones, cars, etc.) as well as biological systems there exists a vastly large design space to make a system that performs a given function.
However, in contrast to the cell, embedded computer systems in general are well-mapped systems and their behavior can effectively be characterized.
This could be a result of:
Computational modelling of large networks of biochemical reactions has become increasingly important and is a main challenge in systems biology. Stochastic approaches have emerged as a significant alternative to the classical deterministic approaches for quantitative analysis of intracellular dynamics because stochastic models take into account the discrete character of quantities of components (i.e. the individual populations of the involved chemical species) and the inherent probabilistic nature of microscopic molecular collisions. The complexity of the highly interacting biological processes leads to intricate models with problems of state space size explosion. Recently, compositional techniques for both modelling and analysis have been applied to biological systems.
We show how to construct a continuous-time Markov chain that models a biochemical reaction network and illustrate our approach with examples. We identify problems occurring during modelling and analysis and based on ongoing work in systems biology we present some approaches to tackle these problems.
We present several case studies of modeling biological networks with the probabilistic model checker PRISM. Biological networks, like metabolic pathways, genetic networks, and signal transduction pathways, play a crucial role in the functioning of the living organisms. We give some stochastic models of such networks that behave like switches, oscillators, or signaling cascades and show how they can be analyzed with PRISM's model checking and simulation options. Also, we discuss the (probabilistic) model checking approach as an alternative to the more traditional methods that are used in the emerging field of systems biology.
The first part will briefly introduce to the modelling language ProbMela which is a simple, but expressive guarded command language for specifying parallel systems with communication over shared variables or message passing along perfect or unreliable channel and probabilistic choice operators. The operational semantics of ProbMela programs is provided by means of Markov decision processes.
The second part of the talk summarizes the main steps of the model checking algorithm for the quantitative analysis of Markov decision processes against linear time properties, and explains the criteria that are required to apply the concept of partial order reduction for Markov decision processes.
In both the theory and practice of computer security, probability theory plays an important role. It applicability ranges from quantifying risk assessment (where probabilities are used to express the likelyhood of 'bad' events happening), through probabilities used in security protocols (e.g., anonymizing protocols), to probability theory used to theoretically define and prove the security of encryption schemes. In this talk I will give an overview of these aspects, giving the fundamental concepts and definitions that involve probability theory in computer security.
There is a growing concern on anonymity and privacy on the Internet, resulting in lots of work on formalization and verification of anonymity. Especially, the importance of probabilistic aspects of anonymity is claimed recently by by many authors. Among them are Bhargava and Palamidessi who present the definition of probabilistic anonymity for which, however, proof methods are not yet elaborated.
In this paper we introduce a simulation-based proof method for probabilistic anonymity. It is a probabilistic adaptation of the method by Kawabe et al. for nondeterministic anonymity: anonymity of a protocol is proved by finding out a forward/backward simulation between certain automata. For the jump from non-determinism to probability we fully exploit a generic, coalgebraic theory of traces and simulations developed by Hasuo, Jacobs and Sokolova. In particular, an appropriate notion of probabilistic simulations is obtained by instantiating a generic definition with suitable parameters.
The case study described in this presentation focuses on verification of system properties such as deadlock freeness, liveness, safety, and temporal properties using the Chi to Uppaal translation scheme and Uppaal model checker. The verification was done as a part of a method of model-based integration and testing (MBI&T), developed in the TANGRAM project. In the presentation we show the potential of the verification techniques to reduce the integration and test effort of industrial systems. We investigate the applicability and the advantages of using verfication techniques for industrial systems.
In the case study a system is formally specified by means of a process algebraic language Chi. The Chi language is supported by a toolset that allows simulation of the obtained Chi model, e.g. for the analysis of system performance and exceptional behaviour handling. The formal semantics of Chi enable funcitional analysis of Chi models, e.g. verification of the correctness of a system model. Combining performance analysis and functional analysis in the Chi environment is the objective of the TIPSy project. As a part of this project, a translation scheme from Chi to Uppaal timed automata has been developed and integrated into the Chi toolset, allowing verification of the translated models by the Uppaal model checker.
The Uppaal tool has been used in a number of industrial case studies. Mostly, the case studies concerned verifying real-time controllers and communication protocols. The other case studies concerned such problems like synthesizing production schedules and control programs for the mock-up of the batch production plant or analyzing the throughput of an ASML wafer scanner.
Joint work with N.C.W. Braspenning, J.M. van de Mortel-Fronczak, and J.E. Rooda.
Traditionally, model checking concerns modelling systems and checking properties, which either hold or not, in other words, the checks can be answered with either "yes" or "no". In more recent years, however, the awareness has grown that often other kinds of checks, which cannot be answered in such a manner, are as important. For these checks, one is usually interested in some measurements, such as the throughput or efficiency of a particular system. Markov Chains, for instance, have shown to be useful when one needs to do performance analysis of a system. Although not common yet, sometimes scheduling problems are also addressed using model checking techniques, since the tools are usually equipped with highly expressive languages, making it possible to specify complex industrial scheduling questions. Comparing the two kinds of property checks, one could label traditional model checking as qualitative model checking and the latter one as quantitative model checking.
Furthermore, as state explosion is a big problem in model checking, research is being done to efficiently explore state spaces to find deadlocks fast, particularly using Artificial Intelligence (AI) heuristic techniques, such as A* and genetic algorithms. This approach is referred to as directed model checking. Although mostly used for qualitative model checking, techniques like beam search can be applied for quantitative model checking, in particular to solve scheduling problems.
In this talk, we will first give an overview of the current field of Directed Model Checking, presenting a number of typical DMC algorithms. Next, we consider a group of algorithms, derived from classical beam search, which can be considered related to the DMC algorithms, and show how these algorithms can be used for quantitative model checking.