Jean-Marc Vincent, INRIA, France

• Abstract:
  Perfect generation, also called perfect or exact simulation, provides a new technique to sample steady-state and avoids the burn-in time period. When the simulation algorithm stops, the returned state value is in steady-state. 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 steady-state. 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 non-monotone 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:
  Jean-Marc 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 INRIA-IMAG APACHE project-team at the University of Grenoble in the performance evaluation group. He is now member of MESCAL INRIA project-team 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 on-line 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 (Tape-PVM), Visualization (Paje), simulation (PSI and PSI2), dynamic Web servers (Hypercarte) and directed about 12 thesis in computer science.

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 semi-circular 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 (Gif-sur-Yvette, France), holder of the Alcatel-Lucent 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.

Enrico Vicario, Università di Firenze, Italy

• Abstract:
  This tutorial addresses the integration of correctness verification and quantitative evaluation of timed systems, based on the stochastic extension of the theory of DBM state classes. In the first part, we recall symbolic state space analysis of non-deterministic 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 Ing-Inf05) 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 real-time systems. In the years 1992-2000, 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.

James Worrell, Oxford, UK

• Abstract:
  Finite-state 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 language-emptiness (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 infinite-state 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 real-time, probabilistic and infinite-state systems; he is particularly interested in the computational complexity of temporal-logic 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..