State estimation of timed automata under partial observation [Draft version]

TL;DR

This paper introduces a method for estimating the current state of partially observable timed automata with a single clock, using zone automaton analysis and an offline algorithm assuming resets at each observable transition.

Contribution

It presents a novel approach for state estimation in timed automata under partial observation, reducing the problem to zone automaton reachability analysis.

Findings

Effective state estimation algorithm for timed automata

Reduction of the problem to discrete zone automaton analysis

Assumption of clock resets at each observable transition

Abstract

In this paper, 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 reachability in the timed automaton is reduced to the reachability analysis of the associated zone automaton, which provides a purely discrete event description of the behaviour of the timed automaton. An algorithm is formulated to provide an offline approach for state estimation of a timed automaton based on the assumption that the clock is reset upon the occurrence of each observable transition.