This story draft by @escholar has not been reviewed by an editor, YET.
E Proofs for Section 6
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
Dynamic Networks of Concurret Pushdown Systems (DCPS)
From Progressive Runs for VASSB to Reachability
Conclusion, Acknowledgment & References
A. Strengthening Fairness to Progressive Runs
E PROOFS FROM SECTION 6
E.1 Proof of Lemma 6.1
Lemma 6.1. A DCPS has a starving run if and only if it has a consistent run.
E.2 Proof of Lemma 6.4 E.3 Freezing DCPS
E.5 Proof of Lemma 6.7
In this section, we prove Lemma 6.7. It will be convenient to use a slightly modified definition of pushdown automata for this.
E.6 Proof of Lemma 6.11
E.7 Proof of Proposition 6.9
L O A D I N G
. . . comments & more!
. . . comments & more!
