State Estimation of Timed Automata Under Partial Observation

In this article, we consider partially observable timed automata endowed with a single clock. A time interval is associated with each transition specifying at which clock values it may occur. In addition, a resetting condition associated to a transition specifies how the clock value is updated upon its occurrence. This work deals with the estimation of the current state given a timed observation, i.e., a succession of pairs of an observable event and the time instant at which the event has occurred. The problem of state estimation for a timed automaton is reduced to the reachability analysis of an associated zone automaton, which provides a purely discrete event description of the behavior of the timed automaton. An algorithm is formulated to provide an approach for state estimation of a timed automaton based on the assumption that the clock is reset upon the occurrence of each observable transition.