On the Verification of Detectability for Timed Systems

In this paper, we investigate the verification of detectability, a fundamental state estimation property, for partially-observed discrete event systems (DES). Existing works on this topic mainly focus on untimed DES. In many applications, however, real-time information is critical for the purpose of system analysis. To this end, in this paper, we investigate the verification of detectability for timed DES modeled by timed automata. Two notions of detectability, strong detectability and weak detectability, are studied in the dense-time setting, which characterize detectability by time elapsing rather than events steps. We show that verifying strong detectability for timed system is decidable by providing a verifiable necessary and sufficient condition. Furthermore, we show that weak detectability is undecidable in the timed setting by reducing the language universality problem for timed automata to this verification problem. Our results extend the detectability analysis of DES from the untimed setting to a timed setting.