QEST 2011 Tutorials
Stochastic Games |
|
 |
Krishnendu Chatterjee (IST Austria, Vienna, Austria) |
| Abstract: | |
| Game theory is the study of interaction between agents in the rich spectrum of relationships ranging between conflict and cooperation. The study of game theory was originally proposed as the mathematical foundation for behavior of rational agents in economics, and over the last few decades has proved its usefulness by providing new techniques and insights in logic and set theory, auction design and implementation, the design and study of the internet, verification, and biology. Dynamic games are used to model competitive processes evolving over time. Stochastic transitions are used for abstraction in modeling or to formalize inherent uncertainty, leading to quantitative statistical analysis. Stochastic games are dynamic games with stochastic transitions. They have a wide range of applications including economics, cell, population and evolutionary biology, queueing theory and performance evaluation, and quantitative temporal model checking. In this tutorial we explore the spectrum of stochastic game models ranging from Markov chains, to Markov decision processes, to 2-player perfect-information stochastic games. We will focus on the application of stochastic games in verification, and consider omega-regular objectives encompassing safety, liveness and parity objectives used in temporal logic model checking. The tutorial will describe some of the key techniques in analysis of stochastic games. | |
Markov Models in Systems Biology |
|
 |
Verena Wolf (Saarland University, Germany) |
| Abstract: | |
| Systems biology is an exciting interdisciplinary field where researchers from a wide range of academic backgrounds investigate complex biological systems and unravel their underlying principles. During the last decade Markov models have become very well-established in this field. This tutorial focuses on a class of Markov models that is used to model networks of chemical reactions. Besides a detailed introduction into this model class, we present recent techniques for their transient and steady-state analysis based on state space truncations, fluid approximations, time-scale separations, and aggregation methods. Various examples from biology are used to illustrate the ideas and intuitions behind the algorithms. The tutorial will close with a discussion of the main challenges in the field of Markovian modelling in systems biology. | |
Adding Recursion to Markov Chains, Markov Decision Processes, and Stochastic Games: Algorithms and Complexity |
|
 |
Kousha Etessami (LFCS University of Edinburgh, UK) |
| Abstract: | |
| I will describe a family of finitely presented, but infinite-state, stochastic models, and stochastic games, that arise by adding a natural recursion feature to Markov Chains, Markov decision processes, and stochastic games. I will describe some algorithms for analysing and model checking these models, and I will discuss the decidability and computational complexity of key analysis problems. These recursive models subsume, in precise senses, a number of classic and heavily studied stochastic processes, including (multi-type) branching processes, (discrete-time) quasi-birth-death processes (QBDs), stochastic context-free grammars, among others. They also provide a natural abstract model of probabilistic procedural programs with recursion, and they are expressively equivalent to probabilistic/game extensions of pushdown automata. The algorithmic theory for analyzing these recursive models, which has been developed over the last few years, has turned out to be a very rich subject with connections to a number of research areas. A key role is played in some of the analysis by fixed point computation problems for algebraically defined monotone functions over basis {+, *, max, min}, and there are connections to some long standing open problems in the complexity of numerical computation. Variants of (decomposed) Newton's method play a key role in numerical algorithms for their analysis. I will survey some of the main algorithmic and complexity results, and discuss some key open questions. I will also briefly describe a tool called PReMo (developed by Dominik Wojtczak) which implements some of the analysis algorithms for these models. (This tutorial surveys joint work with Mihalis Yannakakis in a series of papers, as well as some more recent joint work together with other colleagues: Thomas Brazdil, Vaclav Brozek, Antonin Kucera, and Dominik Wojtczak.) | |
Quantitative Information-Flow Analysis |
|
 |
Boris Köpf (IMDEA Software, Madrid, Spain) |
| Abstract: | |
| Quantitative information-flow analysis (QIF) is an emerging method for establishing information-theoretic confidentiality guarantees. Such guarantees are attractive because they enable one to certify the security of systems that reveal only small amounts of information. Moreover, QIF provides a formal basis for reasoning about the ubiquitous trade-off between security and functionality/performance. In this tutorial I will give an overview of the state-of-the-art in research on QIF. In the first part, I will present the most influential measures of confidentiality and will compare them in terms of their underlying assumptions and the security guarantees they deliver. In the second part of the tutorial, I will present techniques for computing and enforcing corresponding quantitative security guarantees for real systems. | |
Continuous Time Markov Decision Processes: Theory, Applications and Computational Algorithms |
|
 |
Peter Buchholz (University of Dortmund, Germany) |
| Abstract: | |
| Continuous Time Markov Decision Processes (CTMDPs) are used in various areas like Operations Research, Artificial Intelligence, Optimization, Control Theory and more recently also in Theoretical Computer Science as a flexible and analyzable model type. An enormous number of papers and books are available on CTMDPs. However, most papers take a specific viewpoint and do not explicitly consider computational algorithms which are essential for the use of the models in practice. The tutorial aims to give an overview of CTMDPs with a strong focus on numerical algorithms for the computation of optimal policies and rewards with a given accuracy. After a brief introduction of the basic theory, we consider CTMDPs with a finite state space, finite rewards and finite transition rates. For these models methods are introduced to compute epsilon-optimal policies for the finite and infinite horizon case. We show that the proposed numerical methods can be used to solve optimization and control problems from various application areas and can be applied as kernels for model checking algorithms to verify CSL formulas over CTMDPs. Some applications from different applications are given. If time permits some advanced topics like the analysis of CTMDPs with countable state spaces or with bounds on the rewards or transition rates are considered. | |
Probabilistic Models and Tools for Information Security Decisions |
|
 |
Aad van Moorsel (Newcastle University, UK) |
| Abstract: | |
| In this lecture we discuss the quantitative assessment of security and trust in information systems. If successful, quantitative assessment allows one to make objective investment decisions in information security. We review the established research in the area of security and trust assessment and discuss the open research challenges. In depth we will discuss model-based approaches that are based on the trust economics methodology, which establishes probabilistic models that include human and economic factors. The trust economics methodology provides basic tools for objective decision-making, and opens up a range of interesting applications and use cases and decision-making tools. | |
