Logical and probabilistic aspects of state estimation for Markovian systems

This paper is about state estimation in a class of labeled timed probabilistic automata. In detail, we consider continuous time Markov processes where the occurrence of some transitions produces observable events. Such observations can be used to update and refine the state estimation. In this setting, we discuss how a logical state estimation approach can be used to characterize the probabilistic state estimation whenever a new event is observed or when the system evolves without producing new observations (silent closure). The main results of the paper show that the final behaviour, as the silent closure goes to infinity, cannot be characterized only in terms of the graphical structure of the underlying automaton but also depends on the values of the firing rates.