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
D PROOFS FOR SECTION 5.3
The proofs of Lemmas 5.4 and 5.5 both assume that the VASSB considered is both zero-base (by Lemma C.7) and typed (by Lemma C.6). Further, the notion of runs-with-id introduced in Appendix C is used in the proof of Lemma 5.4.
D.1 Proof of Lemma 5.4
D.2 Proof of Lemma 5.5