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