Parametric Disjunctive Timed Networks

Let us show that the absence of invariants in the proof of Proposition 13 does not harm the encoding of the 2CM. The overall idea is that, if a process “chooses” to not take some outgoing transition in the absence of invariants, then we show that the whole computation is stuck, and $q_{\text{halt}}$ is unreachable. Put it differently, while the absence of invariants may add some runs, none of these runs can reach $q_{\text{halt}}$, and the final correctness argument of the proof of Proposition 14 still holds.

In the initial gadget in Figure 2(e), if the process encoding $x_1$ (resp. $x_2$) fails in taking the transition from ${\mathrm{\ell }}_0^t$ to ${\mathrm{\ell }}_1^1$ (resp. from ${\mathrm{\ell }}_0^t$ to ${\mathrm{\ell }}_1^2$) after exactly $p$ time units, then the first process encoding $t$ is stuck forever in ${\mathrm{\ell }}_1^t$, and $q_{\text{halt}}$ is unreachable.

Now, consider the subpart encoding the clock $t$ (in all gadgets): in the absence of invariants, no transition is forced to be taken. However, since all outgoing transitions from the $q_i^t$ locations are guarded by $t=0$, staying more than 0 time unit blocks this process forever, and $q_{\text{halt}}$ becomes unreachable. The same applies to intermediate locations, which all have tight guards (e.g., $t=p$). Therefore, to reach $q_{\text{halt}}$, then the process encoding clock $t$ must take all its guards at the appropriate time – which we assume from now on.

Then, consider the two subparts encoding clocks $x_1$ and $x_2$. For the same reason, failing in taking a transition will block the process forever and, due to the final gadget in Figure 2(f) ensuring transitions are guarded by $x=0$, will block the first process, and therefore $q_{\text{halt}}$ will be unreachable.

This concludes the proof. $◀$

The idea is to reuse the construction of the proof of Proposition 14, by “killing” any process except 3 by sending them to “sink” locations, from which they cannot interfere with the encoding of the 2-counter machine. Fix $n>3$. The modified initial gadget is given in Figure 5. The first three processes behave as in Figure 2(e). Then, all remaining processes are sent to “sink” locations (${\mathrm{\ell }}_s^3$ to ${\mathrm{\ell }}_s^{n-1}$); for one process $i$ to reach its sink location ${\mathrm{\ell }}_s^i$, its predecessor $i-1$ must have reached its own sink location ${\mathrm{\ell }}_s^{i-1}$, due to the location guard “$[{\mathrm{\ell }}_s^{i-1}]$”. Finally note that the first process (simulating $t$) must make sure that the last process has reached its sink location (location guard “$[{\mathrm{\ell }}_s^{n-1}]$”) before reaching the starting location $q_0^t$. This ensures that all processes $i>3$ are in sink locations, where they cannot interfere with the encoding.

The rest of the proof then follows the reasoning of the proof of Proposition 14. $◀$

First note that, in order to traverse the gadgets from the proof of Proposition 13, one needs (at least) 3 processes, due to the interdependency between the location guards. We will show that any process beyond the 3 required processes can only “mimic” the behaviour of one of the 3 required processes.

Consider a process beyond the first three processes. In the initial gadget (Figure 2(e)), it can “choose” any of the three branches leading to the three subparts, as the first three processes make them all available.

First assume this extra process follows the first subpart, simulating clock $t$: observe that, in all the gadgets of the first subpart (Figures 2(b), 3(b), and 4(b)), the behaviour is almost completely deterministic (e.g., all locations with invariant “$t\le p$” are followed by a transition guarded by “$t=p$”). The only exception is in the branching to either ${\mathrm{\ell }}_i^t$ or ${\mathrm{\ell }}_k^t$ in Figure 4(b); assuming exactly one of the location guards $[{\mathrm{\ell }}_{i1}^1]$ or $[{\mathrm{\ell }}_k^1]$ holds (which we discuss below), then this aforementioned extra process will follow exactly the behaviour of the first process.

Alternatively, assume that this extra process follows the second subpart (simulating $x_1$) and let us show that it will follow the second process (the third subpart is similar). In most locations of our gadgets (Figures 2(c), 3(c), and 4(c)), the outgoing guards are tight w.r.t. the invariant (e.g., invariant “$x_1\le p+1$” followed by a transition guarded by “$x_1=p+1$”), and this extra process is forced to follow the second process. In the remaining locations followed by non-tight guards (e.g., “$x_1\le p$” in the increment gadget in Figure 3(c)), the guard is always additionally guarded by the location guard $[q_j^t]$, which makes its behaviour deterministic since the processes simulating clock $t$ are deterministic. Therefore, this extra process is again forced to follow the second process. The 0-test and decrement gadget is similar, with one additional crucial observation: since the aforementioned extra process mimicked the second process so far, then in $q_i^1$, due to the location guard $[q_i^t]$ ensuring a transition in 0-time, then either $x_1=0$ or $x_1>0$ holds, and therefore either both processes simulating $x_1$ reach ${\mathrm{\ell }}_{i1}^1$, or both of them reach ${\mathrm{\ell }}_k^1$ – which justifies the assumption made earlier.

For these reasons, $q_{\text{halt}}$ is reachable only if the first three processes correctly simulate the 2CM; since any additional processes will just simulate one of the first three processes, we can just apply the correctness argument from the proof of Proposition 13. $◀$

We prove the result without invariants. (The case with invariants is simpler and follows immediately.)

The idea is that we ask whether all processes can reach the target location $q_{\text{halt}}$, which can only be done if the 2CM was properly simulated. First note that asking whether all processes can reach the target location $q_{\text{halt}}$ is a property satisfying the definition of global property in Section 4, by simply checking that the number of all locations but $q_{\text{halt}}$ is exactly 0 (called “target problem”).

As in the proof of Theorem 16, in order to traverse the gadgets from the proof of Proposition 13, one needs (at least) 3 processes, due to the interdependency between the location guards. We show here that any process beyond the 3 required processes can only “mimic” the behaviour of one of the 3 required processes, or block the system due to a timelock if it fails to correctly mimic it.

First note that if any of the first three processes does not correctly encode the 2CM (which is a possibility due to the absence of invariants), then an outgoing guard will not be firable, and therefore this process will be blocked forever in its current location, and the global property that all processes must reach $q_{\text{halt}}$ cannot hold. So we assume that the first three processes correctly encode the 2CM (w.l.o.g. we assume that process $i$ encodes the $i$-th subpart).

Now consider a process beyond the first three processes. In the initial gadget (Figure 2(e)), it can “choose” any of the three branches leading to the three subparts, as the first three processes make them all available. Due to the absence of invariants, the process can also choose to not pass the initial gadget – but failing to take such a guard will block it forever in a location due to the guards $x=0$, and the global property that all processes must reach $q_{\text{halt}}$ will never hold.

First assume this extra process follows the first subpart, simulating clock $t$: just as in the proof of Theorem 16, because in all the gadgets of the first subpart (Figures 2(b), 3(b), and 4(b)), the guards are always punctual (i.e., involve equalities), then this extra process will either follow exactly the behaviour of the first process, or fail in taking some guard – therefore remaining forever in its location and violating the global reachability property.

Alternatively, assume that this extra process follows the second subpart (simulating $x_1$). As in the former reasoning, either that extra process will exactly mimic the behaviour of the second process, or will fail in taking some guard, and therefore being blocked in its location, thus violating again the global reachability property.

The case of the final gadget is similar: if any of the processes arrive too early or too late, they will be blocked due to the urgent guards (of the form $x=0$ together with the location guards), and the global reachability will be violated.

For these reasons, $q_{\text{halt}}$ is reachable only if the first three processes correctly simulate the 2CM and if all additional processes simulate exactly one of the first three processes. Finally, we can again apply the correctness argument from the proof of Proposition 14. $◀$

Let $𝒜$ be a fully parametric gPTA with 1 parameter $p$. ${𝒜}^{\mathrm{\infty }}$ is therefore a fully parametric PDTN. Let $v_0$ and $v_1$ denote the valuations such that $v_0(p)=0$ and $v_1(p)=1$, a concept reused from the proof of [27, Corollary 4.8].

We prove the result for global reachability properties (PGR-emptiness), as local properties are a subcase. Fix a global property $\phi$. Let us show that PGR-emptiness does not hold iff $\phi$ is satisfied in a configuration reachable in ${(v_0(𝒜))}^{\mathrm{\infty }}$ or in ${(v_1(𝒜))}^{\mathrm{\infty }}$.

The following lemma derives easily from [27, Proposition 4.7], adapted to the semantics of NTAs (Section 3), and comes from the fact that, whenever no constant terms are used in a gPTA, then rescaling the parameter valuation does not impact the satisfaction of reachability properties.

We can now proceed to the proof of Theorem 18.

$\Rightarrow$

Assume PGR-emptiness does not hold for ${𝒜}^{\mathrm{\infty }}$, i.e., there exists $v$ such that there exists $n\in {\mathbb{N}}_{>0}$ such that $\phi$ is satisfied in a reachable configuration in ${(v(𝒜))}^n$. Let us show that $\phi$ is satisfiable in a configuration reachable in ${(v_0(𝒜))}^n$ or in ${(v_1(𝒜))}^n$.

If $v(p)=0$, then the result is immediate. If $v(p)\ne 0$, then from Lemma 21, $\phi$ is satisfied in a configuration reachable in ${(v_1(𝒜))}^n$ (by choosing some appropriate $t$, i.e., $\frac{1}{v(p)}$).

$\Leftarrow$

Assume $\phi$ is satisfied in a reachable configuration in ${(v_0(𝒜))}^{\mathrm{\infty }}$ or in ${(v_1(𝒜))}^{\mathrm{\infty }}$. That is, there exists $n\in {\mathbb{N}}_{>0}$ such that there is a computation $\pi$ of ${(v_0(𝒜))}^n$ or of ${(v_1(𝒜))}^n$ reaching a configuration $𝔠$ s.t. $𝔠\vDash \phi$. Therefore PGR-emptiness does not hold.

Therefore, it suffices to test the satisfaction of $\phi$ in ${(v_0(𝒜))}^{\mathrm{\infty }}$ and ${(v_1(𝒜))}^{\mathrm{\infty }}$.

Finally, the hardness argument is immediate, considering a PDTN without parameter, and replacing constants different from 1 with additional clocks and locations. $◀$

From the fact that any valuation $v^{\prime }⪯v$ will only add behaviours due to the enlarged guards. $◀$

We prove the result for global reachability properties (PGR-emptiness), as local properties are a subcase. Let $𝒜$ be an L/U-gPTA and $\phi$ a global reachability property over $𝒜$. ${𝒜}^{\mathrm{\infty }}$ is therefore an L/U-PDTN. Consider the DTN ${(v_{0/\mathrm{\infty }}(𝒜))}^{\mathrm{\infty }}$. Let us show that PGR-emptiness does not hold iff $\phi$ is satisfied in a configuration reachable in ${(v_{0/\mathrm{\infty }}(𝒜))}^{\mathrm{\infty }}$.

$\Rightarrow$

Assume PR-emptiness does not hold for ${𝒜}^{\mathrm{\infty }}$, i.e., there exists $v$ such that there exists $n\in {\mathbb{N}}_{>0}$ such that $\phi$ is satisfied in ${(v(𝒜))}^n$. That is, there exists a computation $\pi$ of ${(v(𝒜))}^n$ reaching a configuration $𝔠$ such that $𝔠\vDash \phi$. From Lemma 22, $\pi$ is a computation of ${(v^{\prime }(𝒜))}^n$, for any $v^{\prime }⪯v$. And by extension, completely removing the upper-bound guards (i.e., valuating upper-bound parameters with $\mathrm{\infty }$) only adds behaviour, and therefore $\pi$ is a computation of ${(v_{0/\mathrm{\infty }}(𝒜))}^n$. Hence $𝔠$ is reachable in ${(v_{0/\mathrm{\infty }}(𝒜))}^{\mathrm{\infty }}$, and hence $\phi$ is satisfied.

$\Leftarrow$

Assume there exists a configuration $𝔠$ reachable in ${(v_{0/\mathrm{\infty }}(𝒜))}^{\mathrm{\infty }}$ such that $𝔠\vDash \phi$. That is, there exists $n\in {\mathbb{N}}_{>0}$ such that there is a computation $\pi$ of ${(v_{0/\mathrm{\infty }}(𝒜))}^n$ reaching a configuration $𝔠$ s.t. $𝔠\vDash \phi$. Now, $v_{0/\mathrm{\infty }}$ is not a proper parameter valuation, so we need to exhibit a parameter valuation assigning to each parameter an integer value. We reuse the same concrete parameter valuation for upper-bound parameters as exhibited in [27, Proposition 4.4]: let $T^{\prime }$ be the smallest constant occurring in the L/U-gPTA $𝒜$, and let $T$ be the maximum clock valuation along $\pi$. Fix $D=T+|T^{\prime }|+1$. (We add $T^{\prime }$ to compensate for potentially negative constant terms “$d$” in guards and invariants of $𝒜$.) Since the maximum clock valuation along $\pi$ is $T$, any guard of the form $x\le {\sum }_{1\le i\le M}{\alpha }_i\times p_i+d$, that was replaced with in ${(v_{0/\mathrm{\infty }}(𝒜))}^n$, can be equivalently replaced with $x\le {\sum }_{1\le i\le M}{\alpha }_i\times D+d$ without harming the satisfaction of the guard. Therefore, $𝔠$ is reachable in ${(v_{0/D}(𝒜))}^n$, and hence in ${(v_{0/D}(𝒜))}^{\mathrm{\infty }}$. Therefore, since $𝔠\vDash \phi$, PGR-emptiness does not hold.

Therefore, deciding PGR-emptiness for L/U-PDTNs amounts to deciding satisfaction of $\phi$ in the DTN ${(v_{0/D}(𝒜))}^{\mathrm{\infty }}$.

The case of local properties follows a similar reasoning. $◀$