Context-Bounded Verification of Liveness: Warm-up: Non-Termination

Table of Links

• Introduction
• Dynamic Networks of Concurret Pushdown Systems (DCPS)
• Warm-up: Non-Termination
• Fair Non-Termination
• From Progressive Runs for VASSB to Reachability
• Starvation
• Conclusion, Acknowledgment & References
• A. Strengthening Fairness to Progressive Runs
• B. Proofs from Section 4.1
• C. Proofs for Section 5
• D. Proofs for Section 5.3
• E. Proofs for Section 6

3 WARM-UP: NON-TERMINATION

In this section, we prove Theorem 2.2. The theorem follows easily from previous results for safety verification [Atig et al. 2011; Baumann et al. 2020]. We recall the main ideas as a step toward the more complex proof for fair termination.

Downward Closures: From DCPS to DCFS

The DCFS simulates the downward closure of the DCPS by simulating the composition of the automata for each downward closure. The construction is identical to [Atig et al. 2011, Lemma 5.3]. Thus, we can conclude with the following lemma.

Lemma 3.1. TheK-bounded non-termination problem for DCPS can be reduced in exponential time to the non-termination problem for DCFS. The resulting DCFS is of size at most exponential in the size of the DCPS.

From DCFS Non-Termination to VASS Non-Termination

Proof of Theorem 2.2.

The 2EXPSPACE upper bound follows by combining Lemmas 3.1, 3.2, and the EXPSPACE upper bound for the non-termination problem for VASS [Rackoff 1978].

The 2EXPSPACE lower bound follows from the observation made already in [Baumann et al. 2020] that the 2EXPSPACE-hardness of K-bounded reachability already holds for terminating DCPS, in which every run is terminating. It is now a simple reduction to take an instance of the 퐾-bounded state reachability problem for a terminating DCPS and add a “gadget” that produces an infinite run whenever the target global state is reached.