Measuring and Synthesizing Systems in Probabilistic Environments

The traditional synthesis question given a specification asks for the automatic construction of a system that satisfies the specification, whereas often there exists a preference order among the different systems that satisfy the given specification. Under a probabilistic assumption about the possible inputs, such a preference order is naturally expressed by a weighted automaton, which assigns to each word a value, such that a system is preferred if it generates a higher expected value. We solve the following optimal synthesis problem: given an omega-regular specification, a Markov chain that describes the distribution of inputs, and a weighted automaton that measures how well a system satisfies the given specification under the input assumption, synthesize a system that optimizes the measured value. For safety specifications and quantitative measures that are defined by mean-payoff automata, the optimal synthesis problem reduces to finding a strategy in a Markov decision process (MDP) that is optimal for a long-run average reward objective, which can be achieved in polynomial time. For general omega-regular specifications along with mean-payoff automata, the solution rests on a new, polynomial-time algorithm for computing optimal strategies in MDPs with mean-payoff parity objectives. Our algorithm constructs optimal strategies that consist of two memoryless strategies and a counter. The counter is in general not bounded. To obtain a finite-state system, we show how to construct an epsilon-optimal strategy with a bounded counter, for all epsilon > 0. Furthermore, we show how to decide in polynomial time if it is possible to construct an optimal finite-state system (i.e., a system without a counter) for a given specification. We have implemented our approach and the underlying algorithms in a tool that takes qualitative and quantitative specifications and automatically constructs a system that satisfies the qualitative specification and optimizes the quantitative specification, if such a system exists. We present some experimental results showing optimal systems that were automatically generated in this way.

Propagation Models for Biochemical Reaction Networks

Maria-Emanuela-Canini Mateescu

In this thesis we investigate different ways of approximating the solution of the chemical master equation (CME). The CME is a system of differential equations that models the stochastic transient behaviour of biochemical reaction networks. It does so by describing the time evolution of probability distribution over the states of a Markov chain that represents a biological network, and thus its stochasticity is only implicit. The transient solution of a CME is the vector of probabilities over the states of the corresponding Markov chain at a certain time point t, and it has traditionally been obtained by applying methods that are general to continuous-time Markov chains: uniformization, Krylov subspace methods, and general ordinary differential equation (ODE) solvers such as the fourth order Runge-Kutta method. Even though biochemical reaction networks are the main application of our work, some of our results are presented in the more general framework of propagation models (PM), a computational formalism that we introduce in the first part of this thesis. Each propagation model N has two associated propagation processes, one in discrete-time and a second one in continuous-time. These propagation processes propagate a generic mass through a discrete state space. For example, in order to model a CME, N propagates probability mass. In the discrete-time case the propagation is done step-wise, while in the continuous-time case it is done in a continuous flow defined by a differential equation. Again, in the case of the chemical master equation, this differential equation is the equivalent of the chemical master equation itself where probability mass is propagated through a discrete state space. Discrete-time propagation processes can encode methods such as the uniformization method and the fourth order Runge-Kutta integration method that we have mentioned above, and thus by optimizing propagation algorithms we optimize both of these methods simultaneously. In the second part of our thesis, we define stochastic hybrid models that approximate the stochastic behaviour of biochemical reaction networks by treating some variables of the system deterministically. This deterministic approximation is done for species with large populations, for which stochasticity does not play an important role. We propose three such hybrid models, which we introduce from the coarsest to the most refined one: (i) the first one replaces some variables of the system with their overall expectations, (ii) the second one replaces some variables of the system with their expectations conditioned on the values of the stochastic variables, (iii) and finally, the third one, splits each variable into a stochastic part (for low valuations) and a deterministic part (for high valuations), while tracking the conditional expectation of the deterministic part. For each of these algorithms we give the corresponding propagation models that propagate not only probabilities but also the respective continuous approximations for the deterministic variables.

EPFL2011

Application of 3D range camera in virtual human-computer interfaces

Huan Du

In this work, we propose new ways to employ 3D-ranging systems in advanced human-computer interfaces and show that they can be used for precise hand-tracking systems aiming at virtual keyboard or mouse applications. We first implement a Structured Light (SL) based 3D-ranging system as the testbed for acquiring depth information. The ranging system uses an off-the-shelf projector combined with an industrial color camera, where the projector projects well-designed line patterns onto the scene and the camera captures the reflected light from the scene and the target. The depth information is recovered from the deformed line pattern and the pre-calibrated projector-camera system. With this system we can capture dense depth maps with moderate resolution and high frame rate as the simulated input to the hand-tracking system. We then explore an approach to 3D hand matching that combines a detailed 3D hand model (skeletal + polygonal model) with a Physical-based Model Fitting technique (PMF). Virtual forces are assigned between the depth measurements and the polygonal vertices of the model. The matching problem is formulated as the minimization of the distances between the measurement and the model surface with the guidance of virtual forces. This can employ 3D information simply and directly onto the parameter space, and yield good results under challenging conditions. To demonstrate the effectiveness of the approach we show that we can track hand motions such as typing or grasping frame by frame. The major limitation of this method is that it requires a good initialization of the hand model and the computation time to achieve convergence with good fitting results is quite long. We therefore investigated more complex hand models and feature-based matching techniques. A three-level hand model (skeletal + primitive + polygonal model) is proposed for the Multi-Level Feature Matching approach (MLFM). The matching is carried out from the bottom to top levels of different hand presentations, and distinctive features for each level extracted from both the measurements and the model are matched with Scaled Conjugate Gradient method (SCG). The matching result from lower level is used as the initial state of the model parameters for higher level matching. This hierarchical structure speeds up the optimization process and enhances the precision of the matching result. We demonstrate our approach with the same hand motion as in the previous method and compare the performance of these two methods. We show that the MLFM method is faster and more robust to hand occlusions than the PMF method. Finally, we present a more powerful approach based on the Back-Constrained Gaussian Process Latent Variable Model (BC-GPLVM) that import prior information of categorized hand motion such as typing. BC-GPLVM provides a low-dimensional embedding of hand motion data, with a density function that gives higher probability to gestures and motions close to normal typing motion. This model is learned from a small set of clusters of vast captured motion data. The prior model is then combined with the previous multi-level models and features to generate a uniform cost function for optimization. We show the tracking result to demonstrate that this method can be used for human-computer interfaces requiring precise 3D hand tracking.

EPFL2008

Application of 3D range camera in virtual human-computer interfaces

Huan Du

EPFL2008

Propagation Models for Biochemical Reaction Networks

Maria-Emanuela-Canini Mateescu

EPFL2011