New Insights into the Decidability of Opacity in Timed Automata
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866908293794889728 |
|---|---|
| author | Deng, Weilin Qiu, Daowen Yang, Jingkai |
| author_facet | Deng, Weilin Qiu, Daowen Yang, Jingkai |
| contents | This paper investigates the decidability of opacity in timed automata (TA), a property that has been proven to be undecidable in general. First, we address a theoretical gap in recent work by J. An et al. (FM 2024) by providing necessary and sufficient conditions for the decidability of location-based opacity in TA. Based on these conditions, we identify a new decidable subclass of TA, called timed automata with integer resets (IRTA), where clock resets are restricted to occurring at integer time points. We also present a verification algorithm for opacity in IRTA. On the other hand, we consider achieving decidable timed opacity by weakening the capabilities of intruders. Specifically, we show that opacity in general TA becomes decidable under the assumption that intruders can only observe time in discrete units. These results establish theoretical foundations for modeling timed systems and intruders in security analysis, enabling an effective balance between expressiveness and decidability. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_00625 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | New Insights into the Decidability of Opacity in Timed Automata Deng, Weilin Qiu, Daowen Yang, Jingkai Systems and Control Formal Languages and Automata Theory This paper investigates the decidability of opacity in timed automata (TA), a property that has been proven to be undecidable in general. First, we address a theoretical gap in recent work by J. An et al. (FM 2024) by providing necessary and sufficient conditions for the decidability of location-based opacity in TA. Based on these conditions, we identify a new decidable subclass of TA, called timed automata with integer resets (IRTA), where clock resets are restricted to occurring at integer time points. We also present a verification algorithm for opacity in IRTA. On the other hand, we consider achieving decidable timed opacity by weakening the capabilities of intruders. Specifically, we show that opacity in general TA becomes decidable under the assumption that intruders can only observe time in discrete units. These results establish theoretical foundations for modeling timed systems and intruders in security analysis, enabling an effective balance between expressiveness and decidability. |
| title | New Insights into the Decidability of Opacity in Timed Automata |
| topic | Systems and Control Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2504.00625 |