On Decidability Timed Automata with 2 Parametric Clocks
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916645227724800 |
|---|---|
| author | Bersani, Marcello M. Rossi, Matteo Pietro, Pierluigi San |
| author_facet | Bersani, Marcello M. Rossi, Matteo Pietro, Pierluigi San |
| contents | In this paper, we introduce a restriction of Timed Automata (TA), called non-resetting test Timed Automata (nrtTA). An nrtTA does not allow to test and reset the same clock on the same transition. The model has the same expressive power of TA, but it may require one more clock than an TA to recognize the same language. We consider the parametric version of nrtTA, where one parameter can appear in clock guards of transitions. The focus of this draft is to prove that the $ω$-language emptiness problem for 2-clock parametric nrtTA is decidable. This result can be compared with the parametric version of TA, where the emptiness problem for 2-clock TA with one parameter is not known to be decidable. Our result, however, extends the known decidability of the case of TA with one clock and one parameter from finite words to infinite words. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_04374 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | On Decidability Timed Automata with 2 Parametric Clocks Bersani, Marcello M. Rossi, Matteo Pietro, Pierluigi San Formal Languages and Automata Theory In this paper, we introduce a restriction of Timed Automata (TA), called non-resetting test Timed Automata (nrtTA). An nrtTA does not allow to test and reset the same clock on the same transition. The model has the same expressive power of TA, but it may require one more clock than an TA to recognize the same language. We consider the parametric version of nrtTA, where one parameter can appear in clock guards of transitions. The focus of this draft is to prove that the $ω$-language emptiness problem for 2-clock parametric nrtTA is decidable. This result can be compared with the parametric version of TA, where the emptiness problem for 2-clock TA with one parameter is not known to be decidable. Our result, however, extends the known decidability of the case of TA with one clock and one parameter from finite words to infinite words. |
| title | On Decidability Timed Automata with 2 Parametric Clocks |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2503.04374 |