Decidability of the Initial-State Opacity of Real-Time Automata

In this paper, we investigate the initial-state opacity of real-time automata. A system is called initial-state opaque if an intruder with partial observability is unable to determine whether or not the execution starts from a secret state. In order to prove that the initial-state opacity problem is decidable, we first calculate the lapse of time between each pair of observable events. Two real-time automata are constructed which accept the projection of languages from secret initial states and non-secret ones, respectively. Then, the two real-time automata are further transformed into trace-equivalent finite-state automata. Subsequently, we adapt complement and product on the finite-state automata, and check accepting language of the finally-obtained automaton. The system is initial-state opaque if it accepts nothing or only empty trace, and not initial-state opaque otherwise.