Labelled Markov processes (LMPs) are a theoretical formalism that generalizes both process algebra as well as traditional Markov chains. LMPs are processes that combine nondeterminism with probabilistic transitions. LMPs provide a foundation for interacting with discrete probabilistic systems. The interaction is synchronized on labels, just as in process algebras. There have been significant theoretical advances recently with the development of a notion of bisimulation for continuous LMPs, a logical characterization of bisimulation, metrics and approximation theory. (Note: the reader should refer to the papers in pdf format for appropriate bibliographical references.) The approximation theory developed by Desharnais, Gupta, Jagadeesan and Panangaden has very appealing theoretical properties: it converges in the metric and also in the domain of LMPs and it captures exactly the logical properties of the original system in the limit. However, until now it has been unclear how to implement it in practice.
The initial study of labelled Markov processes in continuous state spaces was motivated by the potential for important practical applications in performance analysis and verification. This hope was based on the initial approximation schemes of Desharnais et al. cited above. Unfortunately, the development of concrete applications was slowed by obstacles that arose in the implementation of continuous state space approximation algorithms. Indeed, these algorithms are grounded in measuretheoretic ideas, some of which offer no direct algorithmic content. The biggest obstacle was that one had to invert an arbitrary measurable function. One could imagine that it was reasonable to assume conditions on the transition probability function-perhaps continuity or even piecewise linearity-in order to make progress. Indeed, a few examples were worked out by hand in this way. However, a general scheme to realize these approximations was lacking until recently.
So the first step of my research project with Prakash Panangaden and Doina Precup was to develop a working implementation of an approximation scheme for continous state space LMPs. It was completed around June 2005. The first weeks of my summer NSERC project were spent writting a paper describing the details of the implementation and the theoretical challenges that its conception implied. This paper was submitted to the QEST 2005 and accepted by the review comitte subsequently. The final version of this paper is available here. The implementation (currently poorly documented) relies heavily on techniques from probability theory, especially Monte Carlo methods, and eliminates the need for inverting exactly the transition probability function.
We observed, however, that the obtained approxiation has O(floor(1/e)^n) states, where n, e control respectively the depth and the precision of the approximation. Let us fix a precision e on the transitions and consider the increase of the cardinality of the state space in function of n. It is not surprising to find an exponential increase in this case since the obtained approximation is faithful to all formulas, while there are exponentially many formulas of depth n (modulo a fixed precision e on the parameter q of the diamond clauses <a>_q).
The next step was to check if this complexity can be improved, how it can be improved or approximated. I read this paper from Mansour and Even-Dar, which studies complexity and algorithm form MDPs rather than LMPs. Even though the question is not settled yet, I got one or two results using their paper.
In connection to the research on PSR going on in the group, we also studied HMMs with continous state space. The main task was to study the notion of bisimulation and trace equivalence in this setting.
Given the current state of an HMM, a transition will be characterized by a new state drawn from a transition kernel and an observation drawn from an observation kernel. The states visited are typically ``hidden'', and the only information available is the observations. Applying transitions inductively on the new state obtained, we can hence produce trajectories, i.e. strings over observables. In our work we considered the space of infinite trajectories and built a sigma algebra and measure on it.
The main result is that bisimulation is strictly stronger than trace equivalence. In other words, the intuitive relation
I also participated to the Canadian Undergraduate Mathematical Conference, where I did a talk on domain theory:
La théorie des domaines a été introduite dans les années 60 par Dana Scott pour modéliser le lambda-calcul. Cette discipline étudie certains types d'ensembles partiellement ordonnés et présente d'intéressantes connections avec la topologie et la théorie de la récursion. De récentes percées ont aussi démontré l'utilité des domaines pour étudier les processus de décision de Markov.
Je présenterai une petite introduction à la théorie des domaines en la motivant par le problème original sur le lambda-calcul étudié par Scott. Je mentionnerai aussi certaines applications de la théorie aux probabilités et à l'informatique.