Abstracts MLQA 2011

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

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.