Context-Bounded Verification of Liveness: From Progressive Runs for VASSB to Reachability

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

5 FROM PROGRESSIVE RUNS FOR VASSB TO REACHABILITY

In this section, we prove Theorems 4.1 and 4.2. We outline the main ideas and technical lemmas used to obtain the proofs. The formal proofs can be found in the full version of the paper.

We first establish that finite witnesses exist for infinite progressive runs. As a byproduct, this yields Theorem 4.2. Then, we show that finding finite witnesses for progressive runs reduces to reachability in VASSB. Finally, we prove that reachability is decidable for VASSB.

5.1 From Progressive Runs to Shallow Progressive Runs

The zero-base property is easily obtained by making sure that the portion of tokens transferred which correspond to the base vector are separately transferred using Ep -edges. The addition of the types into the global state can be done by expanding the set of balloon states exponentially. A proof of the lemma is given in the full version.

5.2 Reduction to Reachability

5.3 From Reachability in VASSB to Reachability in VASS