Initial-Location Opacity and Infinite-Step Opacity of Timed Automata With Integer Resets

Our prior work established the decidability of current-location timed opacity (CLTO) in timed automata with integer resets (IRTA). This letter considers initial-location timed opacity (ILTO) and infinite-step timed opacity (ISTO) in timed automata (TA). These properties are shown undecidable in general TA. However, their decidability in IRTA is demonstrated by providing the corresponding verification algorithms. Specifically, ILTO verification in IRTA is shown to be reducible to the language inclusion problem of finite automata (FA), a well-known decidable problem. To mitigate the state-space explosion effect, a state-reduction method is proposed, which reduces the state space via bisimilar state merging and reverse-automata-based strategies for ILTO verification. An analogous algorithm extends these state-reduction techniques for ISTO verification. Experiments evaluate the proposed algorithms, showing their effectiveness in verifying moderate-scale IRTA.