Detectability notions for a class of finite labeled Markovian systems

This paper is about state estimation in a timed probabilistic setting. A reference model, namely a labeled timed probabilistic automaton, is used for this purpose and an a posteriori probability vector is defined based on a sequence of observations and their associated time stamps that have been collected thus far. The observable language of the considered system is assumed to be live. The main contribution of the paper is to introduce and characterize some basic detectability notions for timed stochastic systems: (i) event detectability, which implies that the system becomes detectable at the time instant of each new observation but may lose the detectability property between two observations, and (ii) silent detectability, which implies that the system becomes detectable when no observation is collected within an arbitrary large duration. Relaxed notions of detectability are also studied: first, assuming that, given a threshold, the a priori probability that an observed timed sequence leads to an exact reconstruction of the state, is larger than or equal to that threshold; second, by replacing the estimation of single states by the estimation of classes formed by several states.