A region-based approach for state estimation of timed automata under no event observation

In this paper we consider timed automata endowed with a single clock that is reset at each event occurrence. A time interval is associated with each transition specifying at which clock values it may occur. We assume that the (logical and timed) structure of a timed automaton is known, and event labels associated with transitions are not observable. The problem addressed in this paper is to estimate and update the set of possible current discrete states as time elapses without any observation being received. By a partitioning of time intervals into regions, we design a λ-observer (λ is the null observed sequence) that, for a given state and a current time value, estimates the set of possible current states and the corresponding regions to which the timer value associated with each possible current state may belong.