On Decidability Timed Automata with 2 Parametric Clocks

TL;DR

The paper introduces non-resetting test Timed Automata (nrtTA) and their parametric variant to study ω-language emptiness for 2-clock, 1-parameter systems. It proves decidability by decomposing the parameter value space into two regimes, using a region-based analysis and an inductive compression of runs into a bounded number of one-reset sequences. The results extend known decidability from one-clock parametric TA on finite words to two clocks on infinite words, and clarify the expressive relationship between TA and nrtTA. This contributes to the theory of parametric timed languages and informs verification approaches for real-time systems with timing parameters.

Abstract

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.

Figures (18)

• Figure 1: \ref{['subfig:exnrtTA']} Fragment of nrtTA with 1 clock; \ref{['subfig:exTA']} fragment of TA with 1 clock; \ref{['subfig:exnrtTA2clock']} fragment of nrtTA with 2 clocks equivalent to the TA of \ref{['subfig:exTA']}.
• Figure 2: \ref{['subfig:exTA2clock']} Fragment of TA with 2 clocks; \ref{['subfig:exnrtTA3clock']} fragment of nrtTA with 3 clocks equivalent to the TA of \ref{['subfig:exTA2clock']}.
• Figure 3: Graphical depiction of examples of the cases of Proposition \ref{['prop:critval']}. In all cases, we have $m = 2$, $z_1 = x$ and $z_2 = y$. Valuations $v_i$ and $u_i$ are examples of case $i$. For instance, for valuation $v_3$ we have that $v = v_a$, $v' = v_3$, $c = 2$, $z_{2,0} = 0$ hold. For valuation $v_5$, instead, it holds that $v = v_b$, $v' = v_5$, $c = 1$, $z_{2,0} = 1$. Notice that multiple cases can hold for a critical valuation; for example, valuation $v_c$ corresponds to both cases 4 (with $c = 3$) and 5 (with $c = 2$).
• Figure 4: Graphical depiction of intervals ${\underline{0}}_{\bar{\mu}}$, ${\underline{0\ell}}_{\bar{\mu}}$, ${\underline{\ell}}_{\bar{\mu}}$, ${\underline{\ell\widehat{\ell}}}{\bar{\mu}}$, ${\underline{\widehat{\ell}}}_{\bar{\mu}}$, and ${\underline{\widehat{\ell}1}}_{\bar{\mu}}$ and example of one-reset sequence $v_0 v_1 v_2 v_3 v_4 v_5$ (notice that in this case the polarity is negative, as $\mathit{frac(\bar{\mu})} < \frac{1}{2}$ holds).
• Figure 5: Graphical depiction of cases of Lemma \ref{['lm:fracvalue']}, where $z_1 = x$ and $z_2 = y$. Cases in which the fractional value of $z_1$ is of interest are enclosed in brackets (e.g., (5) in the top left figure and (7a) in the bottom figure).

Theorems & Definitions (19)

• Definition 1
• Lemma 1
• Theorem 1
• Theorem 2
• proof
• Remark 1
• Proposition 1
• Lemma 2
• proof : Proof of Lemma \ref{['lm:agreement']}
• Proposition 2