Abstracts MLQA 2011

09:15 - 10:00 Y. Le Boudec, ODEs and discrete simulation 10:30 - 11:45 J. Hillston, ODE and Stochastic Process Algebras 11:45 - 12:30 L. Bortolussi, On the Relationship between ODE, Simulation and Stochastic Process Algebras 14:00 - 14:45 V. Wolf, Stochastic Hybrid Analysis of Markov Population Models 14:45 - 15:30 J. Desharnais, Approximation of continuous space systems and associated metrics and logics Thematic Small Working Group: Formal Aspects and Tools for Quantitative Information Hiding. Convened by Catuscia Palamidessi Thematic Small Working Group: Hidden Markov Chains and the languages/logics. Convened by Flemming Nielson

ODEs and discrete simulation

Y. Le Boudec

We consider a generic model of N interacting objects, where each object has a state and the evolution of the system depends only on the collection of states at any point in time. This is quite a general modeling framework, which was successfully applied to model many forms of distributed systems and communication protocols. When the number of objects N is large, one often uses simplifying assumptions called "mean field approximation", "fluid approximation", "fixed point method" or "decoupling assumption". In this talk we explain the meaning of these concepts, how they are related to Ordinary Differential Equations and how a fast simulation methods can be derived. We also show that the first two, namely mean field approximation and fluid approximation, are generally valid, whereas the last two, namely fixed point method and decoupling assumption, require more care, and may not hold even in simple cases. We give sufficient conditions under which they are valid. We illustrate the concepts with some easy-to-follow examples.

Stochastic process algebras and ODEs

Jane Hillston

Stochastic process algebras have been successfully applied to quantitative evaluation of systems for over a decade. Such models may be used to analyse the timeliness of response or the utilisation of resources of systems.

By modelling systems as collections of individual agents, the process algebra approach allows the modeller to capture the exact form of interactions and constraints between entities. At any given time the state of the system is the collection of states exhibited by the individual agents. Inevitably this approach suffers from the problem of state space explosion making analysis inefficient or even infeasible, particularly in systems where we are interested in collective dynamics. In these systems, although we model the behaviour of individuals, we aim to analyse the behaviour of the populations to which they belong. Examples include clients accessing a server, people moving through their physical environment, or molecules interacting within cells.

In this talk I will discuss recent work on such population-oriented models described in stochastic process algebra and interpreted as a set of ordinary differential equations, the so-called fluid approximation.

Small Thematic Working Group on Hidden Markov Models

Flemming Nielson

Markov Processes are perhaps the most widely used class of stochastic models for the quantitative analysis of IT Systems. They come in many forms; examples include DTMCs and CTMCs which admit no nondeterminism, and MDPs and CTMDPs which do admit nondeterminism. Logics derived from Computation Tree Logic has proved useful as "query languages" for such models; examples include the logics PCTL and CSL as well as their extensions. A number of state-of-the-art stochastic model checkers are able to check whether a logical formula holds on a given model.

A Hidden Markov Model is a stochastic model in which observations depend on a Markov Process that cannot be observed. They have many uses in applied statistics, speech recognition, bioinformatics, environmental processes, econometrics, image processing and computer vision, wind power forecasting, and has also been used in security. There has been much less focus on logics for Hidden Markov Models and indeed a study of the extent to which logics provide the appropriate "query language" for Hidden Markov Models. Therefore hardly any model checkers for Hidden Markov Models exist.

A main aim of this working group is to to identify a small consortium that would be interested in developing logics, "query languages", and model checkers that would be able to deal with some of the applications of Hidden Markov Models. Hopefully this would lead to useful tools in much the same way that existing stochastic model checkers make the analysis of Markov Processes available to a wider audience than applied statisticians.

A text books on Hidden Markov Models: Zucchini, W. and I. MacDonald. 2009. Hidden Markov Models for Time Series. Chapman & Hall/CRC, London.

A tutorial paper on Hidden Markov Models: Lawrence R. Rabiner: A tutorial on Hidden Markov Models and selected applications in Speech Recognition. Proceedings of the IEEE, 1989, pages 257-286.

A paper on a logic for Hidden Markov Models: Lijun Zhang, Holger Hermanns, David N. Jansen: Logic and Model Checking for Hidden Markov Models. FORTE 2005: 98-112