Observer design and opacity verification for a class of timed automata

We investigate partially observable timed discrete event systems with a single clock, modelling them using timed automata. The timing structure is defined by three components: a timing function (guard), which restricts transitions to occur when the clock takes a value in a given time interval; a clock resetting function, which indicates how the clock value is updated upon the occurrence of transitions; and a clock invariant function, which bounds the permissible clock values for which the system can remain in a given location. Assuming that the clock is reset whenever an observable event is measured, we propose an offline procedure to construct an observer for such a timed automaton as a deterministic finite automaton based on the reachability analysis of the region automaton, which provides a purely discrete description of the timed automaton. We consider timed observations generated by the system in the form of pairs, the first entry of which is a sequence of measured observable events and associated timestamps, and the second entry of which is the final time of the observation. We prove that the observer generates a string that encodes a timed observation and leads to an observer state, which provides the estimation of locations and a range of possible clock values. Furthermore, we demonstrate that the observer can be used to verify both current location opacity and current (timed) state opacity, where an intruder, with access to certain timed observations, attempts to infer whether the system is in secret locations or secret timed states.