T6: Probabilistic model checking and Random neural nets
  This tutorial consists of two parts:
Probabilistic Model Checking
Marta Kwiatkowska
(Univ. of Birmingham, UK)
Duration: 90 minutes
Probability features increasingly often in software and hardware systems: it is used in distributed co-ordination and routing problems, to model fault-tolerance and performance, and to provide adaptive resource management strategies. Probabilistic model checking is an automatic procedure for establishing if a desired property holds in a probabilistic model, aimed at verifying probabilistic specifications such as "leader election is eventually resolved with probability 1", "the chance of shutdown occurring is at most 0.01%"', and "the probability that a message will be delivered within 30 ms is at least 0.75". A probabilistic model checker calculates the probability of a given temporal logic property being satisfied, as opposed to validity. In contrast to conventional model checkers, which rely on reachability analysis of the underlying transition system graph, probabilistic model checking additionally involves numerical solutions of linear equations and linear programming problems. This tutorial will introduce the theory and the practical details of automatic verification of probabilistic systems against temporal logic specifications. It will cover discrete- and continuous-time Markov chains, Markov decision processes and probabilistic timed automata, as well as the temporal logics PCTL, CSL and PTCTL. The usefulness of the techniques will be demonstrated through a number of case studies analysing real-world probabilistic protocols performed with PRISM, a probabilistic model checker developed at the University of Birmingham. Examples will include the dynamic configuration protocol for IPv4 link-local addresses, self-stabilising algorithms, power management, and CSMA/CD protocol.
Random Neural Networks and Applications
Gerardo Rubino
(INRIA Rennes, France)
Duration: 90 minutes
Random Neural Networks (RNN) are Neural Networks (NN) of a new kind, proposed by E. Gelenbe in the early 90s and having nice mathematical properties and very good performances. Another very specific property of these tools is that they are also Markovian open queuing networks with two different types of customers: positive and negative ones (negative ones actually behave as signals in the model; they are not observable, only their effects are). The previous sentence means that the same mathematical object can be seen as a particular NN or as an open network of queues. When we look at RNN as networks of queues, they are called G-networks. A critical feature of these models is that they belong to the product form family, that is, their steady-state distribution is a product of factors one for each node in the system. This is the key of their nice mathematical properties which allow for very efficient analysis.

As other NN, RNN have been used in many fields that can be roughly classified into two very different types: learning (pattern recognition, pattern synthesis, classification problems...) and optimization. In the first type of applications, the RNN is trained to perform some task (formally, a sequence of RNN is iteratively built that converges towards a RNN that "knows" -some way- how to do the task). In the second one, the RNN is tuned to allow finding a pseudo-optimum of some complex function f() (formally, again, a sequence of RNN is iteratively built in such a way that with each RNN is associated a new point x of f()'s domain such that f(x) is better than previous obtained values).

This tutorial will present the mathematical model and with some detail, one example of each of the two types of applications. Both examples come from the networking area and have been developed by the author and co-workers. Both examples address performance issues.

  • The first application example (in learning) describes how to use RNN in order to quantify the quality of a multimedia stream as perceived by the final user, after the stream was (perhaps) perturbed by an IP network. In other words, it deals with the performance of a streaming communication, focusing on the perceived final quality (and not on indirect -with respect to the user- performance metrics such as losses or delays).
  • The second example (in optimization) shows how to use the tool to design the topology of the access sub-network of a communication one, satisfying different constraints. In other words, it deals with designing a communication network having good performance or dependability properties at minimal costs.
Both examples illustrate the excellent performance of these tools.
Web Maintenance Person.