This paper is available on arxiv under CC BY-NC-SA 4.0 DEED license.
Authors:
(1) Pascal Baumann, Max Planck Institute for Software Systems (MPI-SWS), Germany;
(2) Rupak Majumdar, Max Planck Institute for Software Systems (MPI-SWS), Germany;
(3) Ramanathan S. Thinniyam, Max Planck Institute for Software Systems (MPI-SWS), Germany;
(4) Georg Zetzsche, Max Planck Institute for Software Systems (MPI-SWS), Germany.
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
