The language preservation problem is undecidable for parametric event-recording automata

TL;DR

This paper proves that the language preservation problem remains undecidable for parametric event-recording automata, even under various restrictions and different definitions of the language, highlighting fundamental computational limits.

Contribution

It extends the undecidability results from parametric timed automata to the more restricted class of PERAs, showing the problem's robustness.

Findings

Language preservation problem is undecidable for PERAs.

Undecidability persists under various language definitions.

Results highlight fundamental limits in parametric automata analysis.

Abstract

Parametric timed automata (PTA) extend timed automata with unknown constants ("parameters"), at the price of undecidability of most interesting problems. The (untimed) language preservation problem ("given a parameter valuation, can we find at least one other valuation with the same untimed language?") is undecidable for PTAs. We prove that this problem remains undecidable for parametric event-recording automata (PERAs), a subclass of PTAs that considerably restrains the way the language can be used; we also show it remains undecidable even for slightly different definitions of the language, i.e., finite sequences of actions ending in or passing infinitely often through accepting locations, or just all finite untimed words (without accepting locations).

Full text

††journal: Information Processing Letters

url]https://lipn.univ-paris13.fr/ andre/

1 Introduction

Timed automata (TAs) [1] are a useful formalism to model and formally verify systems involving timing hard constraints and concurrency. TAs benefit from numerous decidability results, including the emptiness of the accepted language. However, the universality and the language inclusion are undecidable for timed automata [1]. Therefore, subclasses have been proposed. The language inclusion becomes decidable for event-recording automata (ERAs) [2].

Parametric timed automata (PTAs) [3] extend TAs with timing parameters: this very expressive formalism can model systems where timing constants are uncertain or unknown, at the cost of most interesting problems to be undecidable [6]. The mere emptiness of the valuation set for which a given location is reachable (“reachability-emptiness”) is undecidable [3].

Restricting the syntax of a formalism may bring decidability: the language inclusion undecidable for TAs [1] becomes decidable for ERAs [2]. In contrast, the reachability emptiness problem for PTAs remains undecidable for a subclass of PTAs with only open inequalities [7].

In [4], we proposed parametric event-recording automata (PERAs), and showed that the reachability-emptiness problem remains undecidable for PERAs. Although it seems that our proof idea can be extended to most problems where the language (i. e., the transition labels) does not play a role (which would include unavoidability-emptiness [8]), it remains open whether language problems undecidable for PTAs become or not decidable for PERAs. In [5], we showed that the following language preservation problem is undecidable for PTAs: “given a PTA and a reference parameter valuation, does there exist another valuation with the same untimed language?”. This problem has connections with the robustness of timed systems, as it asks whether other valuations of the timing constants may lead to the same discrete behavior. The set of valuations with the same untimed language can also be used to perform optimization of some constants without impacting the system’s (untimed) behavior.

We show here that the language preservation problem is undecidable for PERAs, and remains undecidable for different definitions of the language. This quite surprising result comes in contrast with the difference of decidability between TAs and ERAs in the non-parametric setting.

2 Preliminaries

2.1 Clocks, parameters and constraints

Let ${\mathbb{N}}$, ${\mathbb{Z}}$, ${\mathbb{Q}}_{+}$ and ${\mathbb{R}}_{+}$ denote the sets of non-negative integers, integers, non-negative rational and non-negative real numbers respectively.

Throughout this paper, we assume a set $X$ of clocks, i. e., real-valued variables that evolve at the same rate. A clock valuation is a function $\mu:X\rightarrow{\mathbb{R}}_{+}$. We write $\vec{0}$ for the clock valuation that assigns [math] to all clocks. Given $d\in{\mathbb{R}}_{+}$, $\mu+d$ denotes the valuation such that $(\mu+d)(x)=\mu(x)+d$, for all $x\in X$. Given $x\in X$, we define the reset of a valuation $\mu$, denoted by $[\mu]_{x}$, as follows: $[\mu]_{x}(x^{\prime})=0$ if $x^{\prime}=x$, and $[\mu]_{x}(x^{\prime})=\mu(x^{\prime})$ otherwise.

We assume a set $P$ of parameters, i. e., unknown rational-valued constants. A parameter valuation $v$ is a function $v:P\rightarrow{\mathbb{Q}}_{+}$.

A guard $g$ is a constraint over $X\cup P$ defined by a conjunction of inequalities of the form $x\bowtie\eta$, where $\eta$ is either a parameter or a constant in ${\mathbb{Z}}$, and ${\bowtie}\in\{<,\leq,\geq,>\}$. Given $v$, $v(g)$ denotes $g$ where all occurrences of each parameter $p_{i}\in P$ have been replaced by $v(p_{i})$.

2.2 Parametric Event-Recording Automata

Parametric event-recording automata (PTAs) extend event-recording automata with parameters within guards and invariants in place of integer constants [4]; they can also be seen as a syntactic subclass of parametric timed automata [3].

Definition 1** (PERA)**

*A parametric event-recording automaton (hereafter PERA) $\mathsf{A}$ is a tuple $(\Sigma,L,l_{0},P,I,E)$, where:

i) $\Sigma$is a finite set of actions,

ii) $L$is a finite set of locations,

iii) $l_{0}\in L$is the initial location,

iv) $P$is a finite set of parameters,

v) $I$is the invariant, assigning to every $l\in L$ a guard $I(l)$,

vi) $E$is a finite set of edges $e=(l,g,a,l^{\prime})$ where $l,l^{\prime}\in L$ are the source and target locations, $a\in\Sigma$, and $g$ is a guard.

A PERA has a one-to-one mapping between clocks and actions. Given a set of actions $\Sigma$, let $X_{\Sigma}$ denote the set of associated clocks. Similarly, we denote by $x_{a}$ the clock associated with $a$. On any transition labeled with $a$, $x_{a}$ is implicitly reset.

Given a PERA $\mathsf{A}$ and a parameter valuation $v$, we denote by $v(\mathsf{A})$ the non-parametric event-recording automaton where all occurrences of a parameter $p_{i}$ have been replaced by $v(p_{i})$, for each $p_{i}\in P$.

Definition 2** (Concrete semantics of an ERA)**

Given a PERA $\mathsf{A}=(\Sigma,L,l_{0},P,I,E)$, and a parameter valuation $v$, the concrete semantics of $v(\mathsf{A})$ is given by the timed transition system $(S,s_{0},{\rightarrow})$, with $S=\{(l,\mu)\in L\times{\mathbb{R}}_{+}^{|X_{\Sigma}|}\mid\mu\models v(I(l))\}$, $s_{0}=(l_{0},\vec{0})$, and ${\rightarrow}$ consists of the discrete and (continuous) delay transition relations:

• •

discrete transitions: $(l,\mu)\stackrel{{\scriptstyle e}}{{\rightarrow}}(l^{\prime},\mu^{\prime})$, if $(l,\mu),(l^{\prime},\mu^{\prime})\in S$, there exists $e=(l,g,a,l^{\prime})\in E$, $\mu^{\prime}=[\mu]_{x_{a}}$, and $\mu\models v(g)$.

• •

delay transitions: $(l,\mu)\stackrel{{\scriptstyle d}}{{\rightarrow}}(l,\mu+d)$, with $d\in{\mathbb{R}}_{+}$, if $\forall d^{\prime}\in[0,d],(l,\mu+d^{\prime})\in S$.

A run is a sequence $\rho=s_{0}\gamma_{0}s_{1}\gamma_{1}\cdots s_{n}\gamma_{n}\cdots$ such that $\forall i,s_{i}\stackrel{{\scriptstyle\gamma_{i}}}{{\rightarrow}}s_{i+1}$. We consider as usual that runs strictly alternate delays $d_{i}$ and discrete transitions $e_{i}$ and we thus write runs in the form $\rho=s_{0}\stackrel{{\scriptstyle(d_{0},e_{0})}}{{\rightarrow}}s_{1}\stackrel{{\scriptstyle(d_{1},e_{1})}}{{\rightarrow}}\cdots$. The corresponding timed word is $(a_{0},t_{0}),(a_{1},t_{1}),\cdots$ where $a_{i}$ is the action of $e_{i}$ and $t_{i}=\sum_{j=0}^{i}d_{i}$. The corresponding untimed word is $a_{0}a_{1}\cdots$. A maximal run is a run that is either infinite, or that cannot be extended by a discrete transition.

As in [5], we define the language of $v(\mathsf{A})$, denoted by $\mathsf{UL}(v(\mathsf{A}))$ as the set of all untimed words associated with a maximal run of $\mathsf{A}$.

3 Encoding a 2-counter machine into a PERA

We propose in this section an encoding of a 2-counter machine (2CM) into a PERA. This encoding is adapted from the PTA encoding of [5] to our setting of PERAs, and is therefore not a main contribution of this work.

Fix a deterministic 2CM $\mathbf{M}$. Recall that such a machine has two non-negative counters $\mathbf{C}_{1}$ and $\mathbf{C}_{2}$ (the value of which is initially 0), and a finite number of states and of transitions of the form:

• •

when in state $\mathbf{s}_{i}$, increment $\mathbf{C}_{k}$ and go to $\mathbf{s}_{j}$;

• •

when in state $\mathbf{s}_{i}$, if $\mathbf{C}_{k}=0$ then go to $\mathbf{s}_{j}$ else decrement $\mathbf{C}_{k}$ and go to $\mathbf{s}_{j^{\prime}}$.

The machine starts in state $\mathbf{s}_{0}$ and halts when it reaches a particular state $\mathbf{s}_{\mathrm{halt}}{}$. The halting problem for 2-counter machines is undecidable [9].

Our encoding requires a single parameter $p$ and four actions $a_{t}$, $a_{1}$, $a_{2}$, and $a_{z}$ (associated with clocks $t$, $x_{1}$, $x_{2}$ and $z$ respectively). Clock $t$ serves as a tick (it is reset exactly every $p$ time units). We encode a configuration of the 2CM as follows: whenever $t=0$, then $x_{1}=c_{1}$ and $x_{2}=c_{2}$, where $c_{1},c_{2}$ are the current values of $\mathbf{C}_{1},\mathbf{C}_{2}$. Finally, $z$ is used to count the number of steps of the 2CM: we use $p$ to bound the length of the computation of the 2CM. The PERA $\mathsf{A}$ associated with $\mathbf{M}$ is defined as follows:

• •

its set of locations has two copies of the set $\mathbf{S}$ of states of $\mathbf{M}$: for each $\mathbf{s}_{i}\in\mathbf{S}$, there is a main location $l_{i}$, and an intermediary location named $\bar{l_{i}}$;

• •

Each location of $\mathsf{A}$ carries three self-loops, associated with each of the three clocks $t$, $x_{1}$, and $x_{2}$, and resetting that clock when it reaches value $p$, i. e., associated with actions $a_{t}$, $a_{1}$, and $a_{2}$ respectively. This requires a global invariant enforcing that all four clocks $t$, $x_{1}$, $x_{2}$, and $z$ remain below $p$.

Then each transition $(\mathbf{s}_{i},c_{k}++,\mathbf{s}_{j})$ incrementing counter $\mathbf{C}_{k}$ in $\mathbf{M}$ gives rise to a transition from location $l_{i}$ to $\bar{l_{j}}$, with guard $x_{k}=p-1$, and labeled with $a_{k}$ (therefore resetting $x_{k}$) (see Fig. 1(a)). Each transition of the form $(\mathbf{s}_{i},c_{k}--,\mathbf{s}_{j},\mathbf{s}_{j^{\prime}})$ is handled similarly, but gives rise to two transitions: one transition from $l_{i}$ to $\bar{l_{j}}$ with guard $t=0\land x_{k}=0$ (the actual 0-test for $\mathbf{C}_{k}$), and one transition from $l_{i}$ to $\bar{l_{j^{\prime}}}$ with guard $x_{k}=1$ and labeled with $a_{k}$ (therefore resetting $x_{k}$). Then, from each location $\bar{l}$ of $\mathsf{A}$, there is a transition to the corresponding location $l$ with guard $z=p-1$ and resetting $z$ due to action $a_{z}$ (see Fig. 1(b)).

Clock $z$ counts the number of steps (when considering the value of this clock when $t=0$, it encodes a counter that is incremented at every transition of $\mathbf{M}$). Notice that clock $z$ counts, but for the moment, it does not impose any constraint on the length of the simulation. Let us now add condition $0<t<p$ to the guards $z=p-1$ of the transitions leaving the intermediary locations. This way, when $z$ (seen as a counter) has value $p-1$ (when $t=0$ or $p$), no transition is available from any location $\bar{s}$, so that the encoding stops after mimicking $p-1$ steps of the execution of $\mathbf{M}$. As a consequence, our encoding $v(\mathsf{A})$ only encodes properly the $v(p)$ first steps of $\mathbf{M}$, and then blocks (therefore steps beyond $v(p)$ steps are not encoded at all).

4 Undecidability of the language preservation

4.1 Main result

We now show our main result below.

Theorem 1

The language preservation problem for PERAs is undecidable.

The proof of undecidability of [5] for PTAs strongly relies on the fact that all transitions were labeled with the same action $a$. This reasoning cannot be kept here, as the transitions of our modified encoding in Section 3 are labeled with different actions so as to reset different clocks. Therefore, it is not possible to know in advance the language of the accepting run of the 2CM (if any).

For example, assume a run of the 2CM made of the following two instructions: when in state $\mathbf{s}_{0}$, increment $\mathbf{C}_{1}$ and go to $\mathbf{s}_{3}$; when in state $\mathbf{s}_{3}$, if $\mathbf{C}_{2}=0$ then go to $\mathbf{s}_{5}$ else decrement $\mathbf{C}_{2}$ and go to $\mathbf{s}_{0}$. The sequence of states and actions in our PERA will be $(l_{0},\mu_{0})\stackrel{{\scriptstyle a_{1}}}{{\rightarrow}}(\bar{l_{3}},\mu_{1})\stackrel{{\scriptstyle a_{z}}}{{\rightarrow}}(l_{3},\mu_{2})\stackrel{{\scriptstyle a_{t}}}{{\rightarrow}}(\bar{l_{5}},\mu_{3})\stackrel{{\scriptstyle a_{z}}}{{\rightarrow}}(l_{5},\mu_{4})$, for some $\mu_{0},\cdots,\mu_{4}$. (In this sequence, we write $a_{i}$ instead of $(d_{i},e_{i})$ to make clear the action $a_{i}$ used in edge $e_{i}$). Therefore, the untimed language corresponding to these two instructions is $a_{1}a_{z}a_{t}a_{z}$.

In order to prove Theorem 1, we reduce from the halting problem of a 2CM, using the encoding of Section 3. We will allow all possible infinite (untimed) words for the reference valuation, and will rely on the difference between finite and infinite words to perform a distinction between the halting or the non-halting case.

Our proof relies on the PERA $\mathsf{A}$ given in Fig. 2, that contains the encoding of a 2CM $\mathbf{M}$, denoted by $\mathsf{A}_{2CM}$. A transition labeled with $\Sigma$ denotes 4 transitions labeled with $a_{t},a_{1},a_{2},a_{z}$ respectively. Let $v_{0}$ be the valuation s.t. $v_{0}(p)=0$. Given $\mathsf{A}$ and $v_{0}$, we will show that there exists $v\neq v_{0}$ s.t. $\mathsf{UL}(v_{0}(\mathsf{A}))=\mathsf{UL}(v(\mathsf{A}))$ iff $\mathbf{M}$ halts. First, let us study $v_{0}(\mathsf{A})$: this TA can take the transitions to either $l_{\mathrm{acc}}^{1}$ (which is ungarded) or $l_{\mathrm{acc}}^{2}$ (which requires $p=0$), but not that to $l_{0}$ as the guard requires $p>0$. Therefore, $\mathsf{UL}(v_{0}(\mathsf{A}))=(a_{t}|a_{1}|a_{2}|a_{z})^{\omega}$, i. e., the language made of exactly all infinite words, hereafter $\Sigma^{\omega}$.

Now, assume the machine halts after $n$ steps. There exists a parameter valuation $v$ (typically s.t. $v(p)>n$) s.t. the machine is correctly simulated. The (unique) run going through the gadget $\mathsf{A}_{2CM}$ is non-blocking and reaches location $l_{\mathrm{halt}}$, from which it goes to $l_{\mathrm{acc}}^{2}$ and can perform any action an infinite number of times. The corresponding possible runs are therefore included into $\Sigma^{\omega}$. Since this valuation can also take the transition from $l_{\mathrm{start}}$ to $l_{\mathrm{acc}}^{1}$, then the language is $\Sigma^{\omega}$. Hence there exists $v\neq v_{0}$ s.t. $\mathsf{UL}(v_{0}(\mathsf{A}))=\mathsf{UL}(v(\mathsf{A}))$.

Assume the machine does not halt, and consider any valuation $v\neq v_{0}$. As in the previous case, the transition from $l_{\mathrm{start}}$ to $l_{\mathrm{acc}}^{1}$ can be taken, giving (at least) $\Sigma^{\omega}$. In addition, for this valuation, the transition to $l_{0}$ can be taken (since $v(p)>0$), and the 2CM starts to be simulated. However, from our encoding in Section 3, this run will stop after $v(p)$ steps, and will block (without reaching $l_{\mathrm{halt}}$ as the 2CM does not halt). This blocking run is a finite blocking run, therefore is a maximal run, and is therefore part of the language. Hence the language contains all infinite runs ($\Sigma^{\omega}$) plus one finite blocking run—which was not part of $v_{0}(\mathsf{A})$. Therefore, for all $v\neq v_{0}$, $\mathsf{UL}(v_{0}(\mathsf{A}))\subsetneq\mathsf{UL}(v(\mathsf{A}))$.

This gives that there exists $v\neq v_{0}$ s.t. $\mathsf{UL}(v_{0}(\mathsf{A}))=\mathsf{UL}(v(\mathsf{A}))$ iff $\mathbf{M}$ halts. $\blacksquare$

4.2 Varying the definition of language

We can wonder whether the undecidability comes from our definition of the language (consistent with [5]). We briefly discuss other cases to show that it does not. To prove undecidability of the three cases below, we need to perform a common modification to the 2CM encoding. From any intermediary location $\bar{l}$ of $\mathsf{A}_{2CM}$, we add a transition guarded with $t=p\land z=p-1$ leading to a new location $l_{\mathrm{sink}}{}$ with actions $\Sigma$. This transition can only be taken after exactly $v(p)$ steps of the 2CM, i. e., instead of blocking after $v(p)$ steps, the run goes to $l_{\mathrm{sink}}$.

4.2.1 Büchi condition or reachability condition

Let us redefine the untimed language as the set of all words associated with a run passing infinitely often through an accepting location. In that case, our scheme in Fig. 2 can be kept with only mild modifications: let $l_{\mathrm{acc}}^{1}$, $l_{\mathrm{acc}}^{2}$ and $l_{\mathrm{sink}}$ be the accepting locations. Let us add a self-loop on $l_{\mathrm{sink}}$ with a new action, say $a_{3}$. For $v_{0}$, the untimed language is $\Sigma^{\omega}$ (the notation $\Sigma$ remains unchanged, i. e., does not contain $a_{3}$). If the 2CM halts, some valuations will reach $l_{\mathrm{halt}}$, and the untimed language is $\Sigma^{\omega}$. If the 2CM does not halt, $\Sigma^{\omega}$ is part of the language but, for all $v\neq v_{0}$, the run will block, and end in $l_{\mathrm{sink}}$ where it will perform an infinite word with suffix $(a_{3})^{\omega}$, which differs from the discrete behavior of $v_{0}(\mathsf{A})$.

The case of the language defined as the set of finite words ending in an accepting location is similar.

4.2.2 Safety untimed language

Finally, let us redefine the untimed language as the set of untimed words associated with any finite run (no accepting locations are considered). In that case, we relabel the transitions to $l_{\mathrm{sink}}$ with the fresh action $a_{3}$. For $v_{0}$, the language becomes $\Sigma^{*}$. If the 2CM halts, the language is again $\Sigma^{*}$ for some valuations. However, if the 2CM does not halt, for $v\neq v_{0}$ the (unique) run will block, and end in $l_{\mathrm{sink}}$ with $a_{3}$ as suffix—yielding a word not part of $\mathsf{UL}(v_{0}(\mathsf{A}))$.

5 Conclusion

We proved that the language preservation remains undecidable for a subclass of PTAs, namely parametric event-recording automata. We believe that the L/U-automata restrictions considered in the additional undecidability results of [5] could apply to our setting, and undecidability would still hold for “L/U-PERAs”. A more challenging future work is to study the trace preservation problem of [5] that considers not only the actions but also the locations.