
QEST 2008: Tutorials
There will be a coffee break in the morning, 10:3011:00, and another coffee break in the afternoon, 15:3016:00.


Sunday morning, September 14, 2008


09:0012:30

Tutorial T1: Perfect generation, monotonicity and finite queueing networks

JeanMarc Vincent, INRIA, France


Abstract:
Perfect generation, also called perfect or exact simulation, provides a new technique to sample steadystate and avoids the burnin time period. When the simulation algorithm stops, the returned state value is in steadystate. Initiated by Propp and Wilson in the context of statistical
physics, this technique is based on a coupling from the past scheme that, provided some conditions on the system, ensures convergence in a finite time to steadystate. Recently, this approach have been successfully applied in various domains including stochastic geometry, interacting particle systems, statistical physics, networking.
The aim of this tutorial is to introduce the concept of perfect generation and discuss about the algorithmic design of perfect samplers. To improve the efficiency of such samplers, structural properties of models such as monotonicity are enforced in the algorithm to improve drastically the complexity. Such samplers could then been used in brute force to estimate low probability events in finite queueing networks.
The tutorial organized as follows. The first part is devoted to the ``perfect simulation'' principle for Markov chains on finite state space. The contracting backward scheme is explained and main convergence results are established. Moreover some algorithmic considerations illustrate how this scheme could be used in practical situations. The second part of the talk deals with the combination of monotonicity structure and the backward scheme in order to accelerate the simulations. A discussion will follow for nonmonotone systems and how to manage non monotone events. In the third part we apply these ideas in the context of queueing networks with finite capacities and complex routing strategies (overflow, blocking, join the shortest queue,...). We detail the time complexity of such simulations and show that the simulation time is usually linear in the number of queues. Finally in the last part we propose some variance reduction schemes based on coupled antithetic trajectories.
All of these concepts are illustrated with the software tools PSI (for Markov chains in a sparse matrix representation) and PSI2 (finite queuing networks perfect simulator). Implementation difficulties are discussed with regards to simulation efficiency.

Short bio:
JeanMarc VINCENT is associate professor in computer science at University of Grenoble. He received the "agregation" in mathematics in 1986 and a PhD thesis is Computer Science in 1990 from the University of Paris XI (FRANCE). In 1991, he joined the INRIAIMAG APACHE projectteam at the University of Grenoble in the performance evaluation group. He is now member of MESCAL INRIA projectteam in the Laboratory of Informatics in Grenoble.
His research interests concern stochastic modelling and analysis of massively parallel or distributed computer systems. It includes: fundamental studies on dynamics of stochastic discrete event systems (Markovian models, (max,+)algebra, stochastic ordering, stochastic automata networks); software simulation techniques with application to high speed networks (rare event estimation, quality of service...); measurment software tools that provide agregated or disaggregated informations on the behaviour of parallel or distributed program executions (software tracers, statistical online analysers....).
The application fields of such researchs concerns scientific computations, parallel efficient algorithms, with a specific focus on statistical analysis tools. He participates to software developments projects on parallel tracing (TapePVM), Visualization (Paje), simulation (PSI and PSI2), dynamic Web servers (Hypercarte) and directed about 12 thesis in computer science.

09:0012:30

Tutorial T2: Randomness in Wireless Networks: how to deal with it?

Merouane Debbah, SUPELEC, France


Abstract:
The asymptotic behaviour of the eigenvalues of large random matrices has been extensively studied since the fifties. One of the first related result was the work of Eug~ne Wigner in 1955 who remarked that the eigenvalue distribution of a standard Gaussian hermitian matrix converges to a deterministic probability distribution called the semicircular law when the dimensions of the matrix converge to infinity. Since that time, the study of the eigenvalue distribution of random matrices has triggered numerous works, in the theoretical physics as well as probability theory communities. However, as far as communications systems are concerned, until 1996, exhaustive simulations were thought to be the only hope to get some hints on how communications systems with many users/antennas behave even with respect to very basic performance measures such as bit error probability. All this changed in 1997 when large system analysis based on random matrix theory was discovered as an appropriate tool to regain intuitive insight into communication systems, even if their performance measures happened to depend on thousand of parameters. The results led to very active research in many fields such as MIMO, CDMA and Relay networks. In this tutorial, we will describe recent advances in the field and show the potential of random matrix theory as a tool design of wireless networks.

Short bio:
Prof. Mérouane Debbah was born in Madrid, Spain. He entered the Ecole Normale Suprieure de Cachan (France) in 1996 where he received the M.Sc and the Ph.D. degrees respectively in 1999 and 2002. From 1999 to 2002, he worked for Motorola Labs on Wireless Local Area Networks and prospective fourth generation systems. From 2002 until 2003, he was appointed Senior Researcher at the Vienna Research Center for Telecommunications (FTW) (Vienna, Austria) working on MIMO wireless channel modeling issues. From 2003 until 2007, he joined the Mobile Communications department of the Institute Eurecom (Sophia Antipolis, France) as an Assistant Professor. He is presently a Professor at Supelec (GifsurYvette, France), holder of the AlcatelLucent Chair on Fexible Radio. His research interests are in information theory, signal processing and wireless communications. Mérouane Debbah is the recipient of the 2007 Globecom best paper award as well as the Valuetools 2007 best student paper award.



12:3014:00

Lunch at "La Table d'Henri"


Sunday afternoon, September 14, 2008


14:0017:30

Tutorial T3: Correctness veriﬁcation and quantitative evaluation
of timed systems based on stochastic state classes

Enrico Vicario, Università di Firenze, Italy


Abstract:
This tutorial addresses the integration of correctness veriﬁcation and quantitative evaluation of
timed systems, based on the stochastic extension of the theory of DBM state classes.
In the ﬁrst part, we recall symbolic state space analysis of nondeterministic models based
on DBM state classes, describing the algorithms for state space enumeration and for timing
analysis of individual traces. We also discuss the extension to deal with suspension mechanisms
encountered in the analysis of real time preemptive systems.
In the second part, we extend the theory to support quantitative evaluation of stochastic models.
To this end, state classes are decorated with a state density function, and the enumeration of DBM
domains is coupled with symbolic manipulation of probability density functions supported within
DBM domains. This expands the graph of state classes into a stochastic graph, that supports
evaluation of the relative probability of individual execution sequences and opens the way to
steady state analysis based on Markov Renewal Theory.
In the conclusions, we discuss potential and limits of the theory, pointing out domains of
application and open issues for future research.

Short bio:
Enrico Vicario is a Full Professor of Informatics Engineering (Sistemi di Elaborazione delle Informazioni IngInf05) at the dipartimento di Sistemi e Informatica of the University of Florence.
He received the Doctoral Degree in Electronics Engineering and the Ph.D. in Information and Telecommunications Engineering from the University of Florence, in 1990 and 1994, respectively. From 1990 to 1992 he was a Software Scientist with the Center for the Quality of Software (CQ_Ware) of the University of Florence. From 1994 to 1998 he was an Assistant Professor at the University of Florence. From 1998 to 2002, he was Associate Professor at the University of Ancona and then at the University of Florence. He has been a full Professor since November 2002.
Enrico Vicario is the information deputy for the course of Informatics Engineering of the University of Florence (delegato all'orientamento per il Corso di Laurea in Ingegneria Informatica dell'Università di Firenze) .
His present research activity is mainly focused on correctness verification and performance/dependability evaluation of reactive realtime systems. In the years 19922000, he also worked on the application of formal methods in modelling and comparison of spatial relationships for retrieval by similarity in image and video archives.

14:0017:30

Tutorial T4: Model checking and decision procedures for probabilistic automata and Markov chains

James Worrell, Oxford, UK


Abstract:
Finitestate probabilistic automata were introduced by Michael Rabin in the 1960s and have recently been the subject of renewed interest. In the first half of this tutorial we review classical results and open problems on the complexity of decision problems for probabilistic automata, including the analogs of language inclusion, language equivalence and language emptiness. In particular we outline a recent undecidability proof for the languageemptiness (threshold) problem due to Condon and Ladner.
The second part of the tutorial concerns model checking probabilistic systems. We review classical results about model checking LTL and pCTL on finite Markov chains. Finally, time permitting, we survey more recent developments on model checking infinitestate Markov chains arising from Petri nets, counter machines and lossy channel systems.

Short bio:
James Worrell is a University Lecturer in Computer Science at Oxford University. His research interests are in the verification of realtime, probabilistic and infinitestate systems; he is particularly interested in the computational complexity of temporallogic model checking on such systems.
He obtained a PhD in Computer Science in 2001 from Oxford University Computing Laboratory. From 2001 to 2005 he was a research assistant working for Michael Mislove at Tulane University Mathematics Department on the semantics of probabilistic concurrent systems..



18:0019:30

Welcome reception


