* [3] Nissim Francez.  Fairness.  Texts and Monographs in Computer Science. Springer, 1986.
  * [4] Zohar Manna and Amir Pnueli.  The temporal logic of reactive and concurrent systems - specification.  Springer, 1992.
  * [5] Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O. Myreen.  x86-tso: a rigorous and usable programmer’s model for x86 multiprocessors.  Commun. ACM, 53(7):89–97, 2010.
  * [6] M.Z. Kwiatkowska.  Survey of fairness notions.  Information and Software Technology, 31(7):371–386, 1989.
  * [7] Alberto Ros and Stefanos Kaxiras.  Racer: TSO consistency via race detection.  In 49th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2016, Taipei, Taiwan, October 15-19, 2016, pages 33:1–33:13. IEEE Computer Society, 2016.
  * [8] Marco Elver and Vijay Nagarajan.  TSO-CC: consistency directed cache coherence for TSO.  In HPCA 2014, pages 165–176. IEEE, 2014.
  * [9] Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell.  Litmus: Running tests against hardware.  In Parosh Aziz Abdulla and K. Rustan M. Leino, editors, Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, volume 6605 of Lecture Notes in Computer Science, pages 41–44. Springer, 2011.
  * [10] Changhui Lin, Vijay Nagarajan, and Rajiv Gupta.  Efficient sequential consistency using conditional fences.  In Valentina Salapura, Michael Gschwind, and Jens Knoop, editors, 19th International Conference on Parallel Architectures and Compilation Techniques, PACT 2010, Vienna, Austria, September 11-15, 2010, pages 295–306. ACM, 2010.
  * [11] Luca de Alfaro.  From fairness to chance.  Electron. Notes Theor. Comput. Sci., 22:55–87, 1999.
  * [12] Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi.  On the verification problem for weak memory models.  In Manuel V. Hermenegildo and Jens Palsberg, editors, Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, pages 7–18. ACM, 2010.
  * [13] Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo.  A load-buffer semantics for total store ordering.  Logical Methods in Computer Science, 14(1), 2018.
  * [14] W. Feller.  An Introduction to Probability Theory and Its Applications, volume 1 of Texts in Statistical Science.  John Wiley, 3rd edition, 1968.
  * [15] V. G. Kulkarni.  Modeling and Analysis of Stochastic Systems.  Texts in Statistical Science. CRC Press, 2nd edition, 2009.
  * [16] Parosh Aziz Abdulla, Noomene Ben Henda, and Richard Mayr.  Decisive markov chains.  LMCS, 3(4), 2007.
  * [17] Parosh Aziz Abdulla, Noomene Ben Henda, Richard Mayr, and Sven Sandberg.  Eager markov chains.  In Susanne Graf and Wenhui Zhang, editors, Automated Technology for Verification and Analysis, 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006., volume 4218 of Lecture Notes in Computer Science, pages 24–38. Springer, 2006.
  * [18] Pante Stǎnicǎ.  Good lower and uper bounds on binomial coefficients.  Journal of Inequalities in Pure and Applied Mathematics, 2(3), 2001\.
  * [19] Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi.  What’s decidable about weak memory models?  In Helmut Seidl, editor, Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, volume 7211 of Lecture Notes in Computer Science, pages 26–46. Springer, 2012.
  * [20] Christel Baier and Joost-Pieter Katoen.  Principles of Model Checking (Representation and Mind Series).  The MIT Press, 2008.
  * [21] Carl G. Ritson and Scott Owens.  Benchmarking weak memory models.  In Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP ’16, New York, NY, USA, 2016. Association for Computing Machinery.
  * [22] Changhui Lin, Vijay Nagarajan, and Rajiv Gupta.  Fence scoping.  In SC ’14: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, pages 105–116, 2014\.
  * [23] Yuelu Duan, Abdullah Muzahid, and Josep Torrellas.  Weefence: Toward making fences free in tso.  In Proceedings of the 40th Annual International Symposium on Computer Architecture, ISCA ’13, page 213–224, New York, NY, USA, 2013. Association for Computing Machinery.
  * [24] Changhui Lin, Vijay Nagarajan, and Rajiv Gupta.  Efficient sequential consistency using conditional fences.  In Proceedings of the 19th International Conference on Parallel Architectures and Compilation Techniques, PACT ’10, page 295–306, New York, NY, USA, 2010. Association for Computing Machinery.
  * [25] E.M. Clarke, O. Grumberg, and D. Peled.  Model Checking.  MIT Press, Dec. 1999.
  * [26] J.G. Kemeny, J.L. Snell, and A.W. Knapp.  Denumerable Markov Chains.  D Van Nostad Co., 1966.
  * [27] M.Y. Vardi.  Automatic verification of probabilistic concurrent finite-state programs.  In FOCS85, pages 327–338, 1985.
  * [28] Scott Owens, Susmit Sarkar, and Peter Sewell.  A better x86 memory model: x86-tso.  In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Science, pages 391–407. Springer, 2009.
  * [29] Christel Baier, Nathalie Bertrand, and Philippe Schnoebelen.  A note on the attractor-property of infinite-state markov chain.  Inf. Process. Lett., 97(2):58–63, January 2006.
  * [30] Chao Wang, Gustavo Petri, Yi Lv, Teng Long, and Zhiming Liu.  Decidability of liveness on the TSO memory model.  CoRR, abs/2107.09930, 2021.
  * [31] Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, and Viktor Vafeiadis.  Making weak memory models fair.  ArXiv, abs/2012.01067, 2020.
  * [32] Marta Z. Kwiatkowska, Gethin Norman, and David Parker.  PRISM 4.0: Verification of probabilistic real-time systems.  In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 585–591. Springer, 2011.
  * [33] Kousha Etessami and Mihalis Yannakakis.  Recursive markov decision processes and recursive stochastic games.  J. ACM, 62(2):11:1–11:69, 2015.
  * [34] Tomás Brázdil, Stefan Kiefer, Antonín Kucera, and Ivana Hutarová Vareková.  Runtime analysis of probabilistic programs with unbounded recursion.  J. Comput. Syst. Sci., 81(1):288–310, 2015.
  * [35] Javier Esparza, Antonín Kucera, and Richard Mayr.  Model checking probabilistic pushdown automata.  In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings, pages 12–21. IEEE Computer Society, 2004.
  * [36] Tomás Brázdil, Krishnendu Chatterjee, Antonín Kucera, Petr Novotný, and Dominik Velan.  Deciding fast termination for probabilistic VASS with nondeterminism.  In Yu-Fang Chen, Chih-Hong Cheng, and Javier Esparza, editors, Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, volume 11781 of Lecture Notes in Computer Science, pages 462–478. Springer, 2019.
  * [37] Tomás Brázdil, Stefan Kiefer, Antonín Kucera, Petr Novotný, and Joost-Pieter Katoen.  Zero-reachability in probabilistic multi-counter automata.  In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14 - 18, 2014, pages 22:1–22:10. ACM, 2014.
  * [38] Tomás Brázdil, Stefan Kiefer, and Antonín Kucera.  Efficient analysis of probabilistic programs with an unbounded counter.  J. ACM, 61(6):41:1–41:35, 2014.
  * [39] Parosh Aziz Abdulla, Christel Baier, S. Purushothaman Iyer, and Bengt Jonsson.  Simulating perfect channels with probabilistic lossy channels.  Inf. Comput., 197(1-2):22–40, 2005.
  * [40] Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, and Pierre Carlier.  Analysing decisive stochastic processes.  In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55 of LIPIcs, pages 101:1–101:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.
  * [41] Parosh Aziz Abdulla, Noomene Ben Henda, Luca de Alfaro, Richard Mayr, and Sven Sandberg.  Stochastic games with lossy channels.  In Roberto M. Amadio, editor, Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29 - April 6, 2008. Proceedings, volume 4962 of Lecture Notes in Computer Science, pages 35–49. Springer, 2008.

Open Access This chapter is licensed under the terms of the Creative
CommonsAttribution 4.0 International License
(http://creativecommons.org/licenses/by/4.0/), which permits use, sharing,
adaptation, distribution and reproduction in any medium or format, as long as
you give appropriate credit to the original author(s) and the source, provide
a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in
thechapter’s Creative Commons license, unless indicated otherwise in a credit
line to thematerial. If material is not included in the chapter’s Creative
Commons license andyour intended use is not permitted by statutory regulation
or exceeds the permitteduse, you will need to obtain permission directly from
the copyright holder.

##  Appendix 0.A Glossary of Notation

In this section we provide a glossary of notation.

Notation | Meaning | Reference
---|---|---
Transition Systems
$\gamma$ and $\Gamma$ | One and a set of configuration(s) | §2
$\stackrel{{\scriptstyle}}{{\rightarrow}},\stackrel{{\scriptstyle*}}{{\rightarrow}}$, $\stackrel{{\scriptstyle k}}{{\rightarrow}}$ | Single, multi and $k$-step reachability | §2
Temporal Logic
$\rho\models_{{\mathcal{T}}}\Diamond^{\\!\\!k}G$ |  $\rho$ reaches $G$ first at the $k^{th}$ step | §2
$\rho\models_{{\mathcal{T}}}\bigcirc^{\\!k}G$ |  $\rho$ reaches $G$ at the $k^{th}$ step (possibly before) | §2
$\stackrel{{\scriptstyle}}{{\rightarrow}}$, $\stackrel{{\scriptstyle k}}{{\rightarrow}}$ | Simple and $k$-step reachability | §2
Concurrent Programs
${\mathcal{P}}$ | A program | §3
$p$, ${\sf Procs}$ | A process, set of processes | §3
${\sf Regs}_{p}$, ${\sf Regs}_{{\mathcal{P}}}$ | Registers of a process, registers of a program | §3
$\mathsf{Lbl}_{p}$, $\mathsf{Lbl}_{{\mathcal{P}}}$ | Labels of a process, registers of a program | §3
Operational Semantics
$\gamma=\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle$ | Labelling, Register, Buffer, Memory | §4.1
components of $\gamma$
$\left|{\gamma}\right|$ | Size of (buffers of) a configuration | §4.1
$\Gamma_{{\mathcal{P}}}$ | All configurations of ${\mathcal{P}}$ | §4.1
$\Gamma^{\tt plain}_{{\mathcal{P}}}$ | Plain (empty buffer) configurations of ${\mathcal{P}}$ | §4.1
$\llbracket{{\mathcal{P}}}\rrbracket^{\tt TS}$ | Transition system of ${\mathcal{P}}$ | §4.2
$\llbracket{{\mathcal{P}}}\rrbracket^{\tt MC}$ | Markov chain for ${\mathcal{P}}$ | §4.3
$\xrightarrow{p}_{{\tt proc}},\xrightarrow{}_{{\tt update}},\xrightarrow{}_{{\mathcal{P}}}$ | Process, Update, Program transitions | §4.2
${\tt Sched}\left(p\right),{\tt Rweight}\left(\gamma\right)\left(p\right)$ | Weight and relative weight for scheduling | §4.3
PTSO
$\Gamma^{\tt small}_{{\mathcal{P}}}$ | Small ($\left|{\gamma}\right|\leq 4$) configurations of ${\mathcal{P}}$ | §5.1
$\Gamma^{\tt large}_{{\mathcal{P}}}$ | Large ($\left|{\gamma}\right|>4$) configuration of ${\mathcal{P}}$ | §5.1
Costs
${\tt Cost}\left(\mathsf{l}\right)$ | Cost of instruction at $\mathsf{l}$ | §8
${\tt Cost}\left(\gamma,\gamma^{\prime}\right)$ | Single step cost | §8
${\tt Cost}\left(\rho\right)\left(\mathsf{l}\right)$ | Cost of run $\rho$ | §8
$X_{\gamma,\mathsf{l},{\tt Cost}}\left(\rho\right)$ | Random variable for cost over runs | §8
${\mathcal{E}}_{{\mathcal{P}}}$ | Eagerness parameter for ${\mathcal{P}}$ | §8.2.4
$\eta_{{\mathcal{P}}}$ | Eagerness bound for ${\mathcal{P}}$ | §8.2.4
${\mathcal{G}}_{{\mathcal{P}}}$ | Gravity parameter for ${\mathcal{P}}$ | §8.2.1

We now prove Lemma 1. See 1

###### Proof

From any configuration $\gamma$, each transition consists of 2 parts : a
process transition $\gamma\xrightarrow{p}_{{\tt proc}}\gamma_{p}$ followed by
an update transition $\gamma_{p}\xrightarrow{}_{{\tt update}}\gamma^{\prime}$.
Assuming that the configuration $\gamma$ is enabled, the process transition
can be done by any enabled process. This is followed by considering all
possible update transitions. Consider an enabled process $p$. Then
$\gamma\xrightarrow{p}_{{\tt proc}}\gamma_{p}$ happens with probability ${\tt
Rweight}\left(\gamma\right)\left(p\right)$. From $\gamma_{p}$, we consider all
sequences of processes which can result in an update. Let
$S_{\gamma_{p},\gamma^{\prime}}=\\{w\mid\gamma_{p}\xrightarrow{w}_{{\tt
update}}\gamma^{\prime}\\}$ be the set of sequences resulting in a fixed
configuration $\gamma^{\prime}$ and let
$S_{\gamma_{p}}=\\{w\mid\exists\gamma^{\prime}~{}\gamma_{p}\xrightarrow{w}_{{\tt
update}}\gamma^{\prime}\\}$ be all possible sequences labelling an update from
$\gamma_{p}$. Then the probability of reaching configuration $\gamma^{\prime}$
from $\gamma_{p}$ after an update is
$\frac{|S_{\gamma_{p},\gamma^{\prime}}|}{|S_{\gamma_{p}}|}$. Thus, the
probability to reach some configuration from $\gamma_{p}$ after an update is
$\sum_{\gamma^{\prime}}\frac{|S{\gamma_{p},\gamma^{\prime}}|}{|S_{\gamma_{p}}|}=1$,
since $\uplus_{\gamma^{\prime}}S_{\gamma_{p},\gamma^{\prime}}=S_{\gamma_{p}}$.

  1. 1.

For an enabled configuration $\gamma$, $\sum_{p\in{\sf
enab}\left(\gamma\right)}\sum_{\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}}{\tt
M}_{\tt proc}\left(\gamma,\gamma_{p}\right)\cdot{\tt M}_{\tt
update}\left(\gamma_{p},\gamma^{\prime}\right)$, where $\gamma_{p}$ is the
configuration such that $\gamma\xrightarrow{p}_{{\tt
proc}}\gamma_{p}\xrightarrow{}_{{\tt update}}\gamma^{\prime}$ can be written
as

$\sum\limits_{p\in{\sf enab}\left(\gamma\right)}{\tt
Rweight}\left(\gamma\right)\left(p\right)\sum\limits_{\gamma^{\prime}}\frac{|S_{\gamma_{p},\gamma^{\prime}}|}{|S_{\gamma_{p}}|}=\sum_{p\in{\sf
enab}\left(\gamma\right)}\frac{{\tt
Sched}\left(p\right)}{\sum_{p^{\prime}\in{\sf enab}\left(\gamma\right)}{\tt
Sched}\left(p^{\prime}\right)}=1$

  2. 2.

For the case when $\gamma$ is disabled, by definition, we have ${\tt M}_{\tt
proc}\left(\gamma,\gamma\right):=1$ and ${\tt M}_{\tt
proc}\left(\gamma,\gamma_{p}\right):=0$ for $\gamma_{p}\neq\gamma$. Further,
from $\gamma$, we can consider all possible update transitions resulting in a
configuration $\gamma^{\prime}$. This gives us
$\sum_{\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}}{\tt M}_{\tt
proc}\left(\gamma,\gamma\right)\cdot{\tt M}_{\tt
update}\left(\gamma,\gamma^{\prime}\right)$ which can be seen to be

$1.\sum\limits_{\gamma^{\prime}}\frac{|S_{\gamma,\gamma^{\prime}}|}{|S_{\gamma}|}=1$

Thus, in all cases, we have shown that ${\tt M}_{{\mathcal{P}}}$ is a
probability distribution, and the induced transition system is a Markov Chain.

Recall that in section 4.2, we introduced the notion of a transition system
$\llbracket{{\mathcal{P}}}\rrbracket^{\tt
TS}=\left\langle\Gamma_{{\mathcal{P}}},\xrightarrow{}_{{\mathcal{P}}}\right\rangle$
given a program ${\mathcal{P}}$. The Markov chain associated to the program
${\mathcal{P}}$ has been introduced in Section 4.3 as
$\llbracket{{\mathcal{P}}}\rrbracket^{\tt
MC}=\left\langle\Gamma_{{\mathcal{P}}},{\texttt{M}}_{{\mathcal{P}}}\right\rangle$.
Now, we formally show that $\llbracket{{\mathcal{P}}}\rrbracket^{\tt TS}$ is
the same as the transition system
${\left(\llbracket{{\mathcal{P}}}\rrbracket^{\tt MC}\right)}^{\downarrow}$
induced by $\llbracket{{\mathcal{P}}}\rrbracket^{\tt MC}$.

We begin with the proof for Lemma 2, which says that the transition system
induced by the Markov chain is the same as the transition system induced by
the program. See 2

###### Proof

First we show that if
$\left\langle\gamma,\gamma^{\prime}\right\rangle\in\stackrel{{\scriptstyle}}{{\rightarrow}}_{{\left(\llbracket{{\mathcal{P}}}\rrbracket^{\tt
MC}\right)}^{\downarrow}}$ then
$\left\langle\gamma,\gamma^{\prime}\right\rangle\in\stackrel{{\scriptstyle}}{{\rightarrow}}_{\llbracket{{\mathcal{P}}}\rrbracket^{\tt
TS}}$. Whenever
$\left\langle\gamma,\gamma^{\prime}\right\rangle\in\stackrel{{\scriptstyle}}{{\rightarrow}}_{{\left(\llbracket{{\mathcal{P}}}\rrbracket^{\tt
MC}\right)}^{\downarrow}}$, we have ${\tt
M}_{{\mathcal{P}}}{(\gamma,\gamma^{\prime})}>0$.

  1. 1.

Consider the case when $\gamma$ is enabled. Then there exists some
$\gamma^{\prime\prime}$ such that ${\tt M}_{\tt
proc}\left(\gamma,\gamma^{\prime\prime}\right)>0$ and ${\tt M}_{\tt
update}\left(\gamma^{\prime\prime},\gamma^{\prime}\right)>0$. Since ${\tt
M}_{\tt proc}\left(\gamma,\gamma^{\prime\prime}\right)>0$, we have ${\tt
Rweight}\left(\gamma\right)\left(p\right)>0$ for some $p$ which resulted in
obtaining $\gamma^{\prime\prime}$ from $\gamma$. Hence, for process $p$ we
have $\gamma\xrightarrow{p}_{{\tt proc}}\gamma^{\prime\prime}$. Similarly,
there is a sequence $w$ such that $\gamma^{\prime\prime}\xrightarrow{w}_{{\tt
update}}\gamma^{\prime}$, i.e. $\gamma^{\prime\prime}\xrightarrow{}_{{\tt
update}}\gamma^{\prime}$. Composing the two, we obtain
$\gamma\stackrel{{\scriptstyle}}{{\rightarrow}}_{\llbracket{{\mathcal{P}}}\rrbracket^{\tt
TS}}\gamma^{\prime}$.

  2. 2.

The second case is when $\gamma$ is not enabled. Then ${\tt M}_{\tt
proc}\left(\gamma,\gamma\right)=1$, by definition. An update transition can
still be done from $\gamma$ (empty update if all buffers are empty). In any
case, the resultant configuration $\gamma^{\prime}$ after an update is such
that ${\tt M}_{\tt update}\left(\gamma,\gamma^{\prime}\right)>0$. Thus, as
above, composing the two, we obtain
$\gamma\stackrel{{\scriptstyle}}{{\rightarrow}}_{\llbracket{{\mathcal{P}}}\rrbracket^{\tt
TS}}\gamma^{\prime}$ in ${\llbracket{{\mathcal{P}}}\rrbracket^{\tt TS}}$.

Next, we show that if
$\left\langle\gamma,\gamma^{\prime}\right\rangle\in\stackrel{{\scriptstyle}}{{\rightarrow}}_{\llbracket{{\mathcal{P}}}\rrbracket^{\tt
TS}}$, then ${\tt M}_{{\mathcal{P}}}{(\gamma,\gamma^{\prime})}>0$. As above,
there are two cases depending on whether $\gamma$ is enabled or not.

  1. 1.

Assume $\gamma$ is enabled. Then
$\stackrel{{\scriptstyle}}{{\rightarrow}}_{\llbracket{{\mathcal{P}}}\rrbracket^{\tt
TS}}$ is a composition of $\xrightarrow{}_{{\tt proc}}$ and
$\xrightarrow{}_{{\tt update}}$. There exists some process $p$ and a sequence
$w$ such that $\gamma\xrightarrow{p}_{{\tt
proc}}\gamma^{\prime\prime}\xrightarrow{w}_{{\tt update}}\gamma^{\prime}$.
Hence ${\tt M}_{\tt proc}\left(\gamma,\gamma^{\prime\prime}\right)={\tt
Rweight}\left(\gamma\right)\left(p\right)>0$ and ${\tt M}_{\tt
update}\left(\gamma^{\prime\prime},\gamma^{\prime}\right)>0$ since
$\left|{\left\\{w~{}|~{}\;{\gamma^{\prime\prime}\xrightarrow{w}_{{\tt
update}}\gamma^{\prime}}\right\\}}\right|>0$. Hence ${\tt
M}_{{\mathcal{P}}}{(\gamma,\gamma^{\prime})}>0$.

  2. 2.

If $\gamma$ is not enabled, then all processes are disabled in $\gamma$. In
this case, the only transition in ${\llbracket{{\mathcal{P}}}\rrbracket^{\tt
TS}}$ is $\gamma\xrightarrow{}_{{\tt proc}}\gamma$, followed by an update
transition leading to some $\gamma^{\prime}$. Hence, ${\tt
M}_{{\mathcal{P}}}{(\gamma,\gamma^{\prime})}>0$.

Thus we have shown that there is a transition between a pair of configurations
in ${\llbracket{{\mathcal{P}}}\rrbracket^{\tt TS}}$ iff there exists a
transition between them in
$\stackrel{{\scriptstyle}}{{\rightarrow}}_{{\left(\llbracket{{\mathcal{P}}}\rrbracket^{\tt
MC}\right)}^{\downarrow}}$.

Thanks to Lemma 2, whenever ${\left(\llbracket{{\mathcal{P}}}\rrbracket^{\tt
MC}\right)}^{\downarrow}$ has a transition with non zero probability,
$\llbracket{{\mathcal{P}}}\rrbracket^{\tt TS}$ has the same transition. Thus,
it suffices to check reachability in $\llbracket{{\mathcal{P}}}\rrbracket^{\tt
TS}$.

The reachability between plain configurations (those which have all buffers
empty) follows from [12]. We prove Lemma 3 by reducing reachability from a
given configuration to a plain configuration to the reachability problem
between two plain configurations. Likewise, label reachability is known to be
decidable when starting from a plain configuration in classical TSO semantics
[13]. We can prove Lemma 4 in a similar manner (as in Lemma 3) by reducing the
label reachability from a given configuration to label reachability from a
plain configuration, and then invoking [13].

See 3

###### Proof

Given a program ${\mathcal{P}}$, and a configuration
$\gamma=\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle$,
and a plain configuration
$\gamma^{\prime}=\left\langle\lambda^{\prime},{\mathcal{R}}^{\prime},{\mathcal{B}}^{\prime},{\mathcal{M}}^{\prime}\right\rangle$,
can we reach $\gamma^{\prime}$ from $\gamma$? Assume that there are $n$
processes $p_{1},\dots,p_{n}$, with shared variables $x_{1},\dots,x_{m}$. The
bufferstate ${\mathcal{B}}$ consists of words $w_{1},w_{2},\dots,w_{n}$ where
$w_{i}$ is the buffer content of process $i$ in ${\mathcal{B}}$. Note that
each $w_{i}$ is a finite length word. Assume that $|w_{i}|=k_{i}$, and $w_{i}$
has the form $(x_{i1},v_{i1})\dots(x_{ik_{i}},v_{ik_{i}})$.

We modify ${\mathcal{P}}$ to a program ${\mathcal{P}}^{\prime}$ by (i)
modifying the code of $p_{1},\dots,p_{n}$ and by adding a new process
$p_{n+1}$, (ii) we introduce two new local registers $r,r^{\prime}$ in
$p_{1}$, a new shared variable $flag$, initializing all of them to 0. We
reduce the reachability of $\gamma$ to $\gamma^{\prime}$ in ${\mathcal{P}}$ to
the reachability between two plain configurations in ${\mathcal{P}}^{\prime}$.

  1. 1.

Assume that ${\mathcal{M}}$ is given by $x_{i}\mapsto u_{i}$, for all $1\leq
i\leq m$. We alter $p_{1}$ by adding some instructions before all the existing
instructions in $p_{1}$.

The new instructions added to $p_{1}$ are the following. We begin with a while
loop which checks $flag$ is 0. Inside the loop, we have the following. For
$1\leq i\leq m$, we add the instructions
$r^{\prime}=u_{i};CAS(x_{i},r,r^{\prime})$. When we finish executing all $m$
of these instructions, this results in the memory state as given by
${\mathcal{M}}$. This is followed by writing $v_{11}$ to $x_{11}$,
$\dots,v_{1k_{1}}$ to $x_{1k_{1}}$, obtaining the buffer content of $p_{1}$ in
${\mathcal{B}}$ and also writing the appropriate values to all registers of
$p_{1}$ as in ${\mathcal{R}}$. This is followed by setting $flag$ to 1. The
while loop is broken at this point. The next instruction checks if $flag$ is
$n+1$, and if so, goes to the label $\ell_{1}$ (the control location of
$p_{1}$ in $\lambda$).

  2. 2.

Processes $p_{i}$ for $2\leq i\leq n$ are modified as follows. Add a new
register $r_{i}$

  3. 3.

for each $p_{i}$, and initialize to 0. We begin with a while loop which checks
$flag$ is $i-1$. Inside the loop, we have the following. Using $r_{i}$, we
write $v_{i1}$ to $x_{i1}$, and so on until we write $v_{ik_{i}}$ to
$x_{ik_{i}}$, obtaining the buffer content of $p_{i}$ in ${\mathcal{B}}$. Then
we write the appropriate values to all registers of $p_{i}$ as in
${\mathcal{R}}$. This is followed by setting $flag$ to $i$. The while loop is
broken at this point. The next instruction checks if $flag$ is $n+1$, and if
so, goes to the label $\ell_{i}$ (the control location of $p_{i}$ in
$\lambda$).

  4. 4.

For $p_{n+1}$, we begin with a while loop which checks if $flag$ is $n$.
Inside the loop, it reads the memory and checks that it agrees with
${\mathcal{M}}$. This is possible as the buffer of $p_{n+1}$ is empty. After
the check, it changes the $flag$ to $n+1$, breaking the while loop and
reaching the terminal instruction of $p_{n+1}$.

The modified program ${\mathcal{P}}^{\prime}$ has polynomially many extra
instructions at the beginning of each process. Starting from the initial
configuration $\gamma_{\it init}$ consisting of all initial labels of
instructions in all processes $p_{1},\dots,p_{n+1}$, with all variables and
registers having value 0, and all empty buffers, ${\mathcal{P}}^{\prime}$
first executes these extra instructions in all processes. The new shared
variable $flag$ moves the processes 1 to $n+1$ in order until we obtain (i)
the memory state as in ${\mathcal{M}}$, (ii) buffer contents of all processes
$p_{1},\dots,p_{n}$ as in ${\mathcal{B}}$, (iii) local registers of all
processes $p_{1},\dots,p_{n}$ as in ${\mathcal{R}}$. When $flag$ becomes
$n+1$, all processes $p_{1},\dots,p_{n}$ move to the control locations given
by $\lambda$ in $\gamma$. Ignoring $flag$ as well as the two new local
registers added to $p_{1}$, and $p_{n+1}$, the configuration of
${\mathcal{P}}^{\prime}$ at this point is
$\gamma=\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle$,
the configuration given to us.

Define a configuration
$\gamma^{\prime\prime}=\left\langle\lambda^{\prime\prime},{\mathcal{R}}^{\prime\prime},{\mathcal{B}}^{\prime\prime},{\mathcal{M}}^{\prime\prime}\right\rangle$
as follows.

  1. 1.

The labeling $\lambda^{\prime\prime}$ agrees with $\lambda^{\prime}$ for
processes $p_{1},\dots,p_{n}$,

  2. 2.

${\mathcal{B}}^{\prime\prime}$ agrees with ${\mathcal{B}}^{\prime}$ in terms
of buffer states of $p_{1},\dots,p_{n}$,

  3. 3.

${\mathcal{M}}^{\prime\prime}$ agrees with ${\mathcal{M}}^{\prime}$, the
memory state wrt $x_{1},\dots,x_{m}$

  4. 4.

${\mathcal{R}}^{\prime\prime}$ agrees with ${\mathcal{R}}^{\prime}$, the
register state wrt the registers in ${\mathcal{P}}$. In addition,

  5. 5.

the buffer of $p_{n+1}$ is empty in ${\mathcal{B}}^{\prime\prime}$,

  6. 6.

The new shared variable $flag\mapsto n+1$ in the memorystate
${\mathcal{M}}^{\prime\prime}$,

  7. 7.

The new registers $r,r^{\prime}$ of $p_{1}$ are such that $r$ has value 0 and
$r^{\prime}$ has value $u_{m}$ in ${\mathcal{R}}^{\prime\prime}$,

  8. 8.

The new register $r_{i}$ of $p_{i}$ for $2\leq i\leq m$ has value $v_{ik_{i}}$
in ${\mathcal{R}}^{\prime\prime}$.

  9. 9.

The label of $p_{n+1}$ in $\lambda^{\prime\prime}$ is the term instruction in
$p_{n+1}$.

We now ask the reachability query from $\gamma_{\it init}$ to
$\gamma^{\prime\prime}$ in ${\mathcal{P}}^{\prime}$ which is known to be
decidable [12], since both $\gamma_{\it init}$ and $\gamma^{\prime\prime}$ are
plain. Note that ${\mathcal{P}}^{\prime}$ starts simulating ${\mathcal{P}}$
only when it reaches a configuration whose projection to the processes
$p_{1},\dots,p_{n}$, modulo the new registers and $flag$ is $\gamma$. Indeed,
if $\gamma^{\prime\prime}$ is reachable in ${\mathcal{P}}^{\prime}$ from
$\gamma_{\it init}$, then it must be that (i) Ignoring values of new registers
and $flag$, $\gamma$ is reachable from $\gamma_{\it init}$ in
${\mathcal{P}}^{\prime}$ (this follows by construction), and (ii)
$\gamma^{\prime\prime}$ is reachable in ${\mathcal{P}}^{\prime}$ from
$\gamma$. Indeed since $\gamma^{\prime\prime}$ when projected to the old
registers and shared variables and $p_{1},\dots,p_{n}$ is $\gamma^{\prime}$,
we obtain the reachability of $\gamma^{\prime}$ from $\gamma$ in
${\mathcal{P}}$.

Finally we prove Lemma 5.

See 5

###### Proof

We will show that $\Gamma^{\tt plain}_{{\mathcal{P}}}$ is a finite attractor
in the sense of [16]. An attractor [16], is a set of configurations which is
eventually reached with probability 1 from every configuration in the Markov
Chain $\llbracket{{\mathcal{P}}}\rrbracket^{\tt MC}$.

$\Gamma^{\tt plain}_{{\mathcal{P}}}$ contains configurations with empty
buffers. We intuitively want to show that the system behaviours tend to
concentrate towards these. We make this notion precise through the concept of
configuration size, $|\gamma|$. It is sufficient to show that the expected
value of $|\gamma|$ at each step decreases (when transitioning from
configurations with sufficiently large buffers). The expectation is over the
possible transitions from $\gamma$.

We show this in two steps. We first show that

${\it Prob}_{{\mathcal{P}}}\left(\gamma\models\Box\Diamond\Gamma^{\leq
k}_{{\mathcal{P}}}\right)=1$

for constant $k=4$ for all programs ${\mathcal{P}}$ and configurations
$\gamma\in\Gamma_{{\mathcal{P}}}$. Recall that $\Gamma^{\leq
k}_{{\mathcal{P}}}$ is the set of configurations with size (sum of buffer
lengths) at most $k=4$. Then we use this to prove the statement of the lemma.
First to show that $\Gamma^{\leq 4}_{{\mathcal{P}}}$ is an attractor, we use
the following result from [29].

##### Left-oriented Markov chains ([29])

Baier et al. consider (infinite) Markov chains where the state space $S$ is
partitioned into non-negative integer labelled levels
$\cup_{i\in\mathbb{N}}S_{i}$. For $s\in S$, the level of $s$, $level(s)$ is
$i$ if $s\in S_{i}$. Then $\mathbb{E}(s)=\sum_{j=0}^{\infty}{\it
Prob}\left(s,S_{j}\right)\cdot j$ defines the expected next level for state
$s$. The Markov chain is called left oriented iff there is a positive constant
$\Delta$ such that $\mathbb{E}(s)\leq level(s)-\Delta$ for all states $s\notin
S_{0}$, that is, for all states $s$ at level 1 or more. Theorem 2.1 from [29]
shows that for any left oriented Markov chain, the leftmost level $S_{0}$ is
an attractor.

We leverage Theorem 2.1 from [29] in our proof. To do this, we show that our
Markov Chain $\llbracket{{\mathcal{P}}}\rrbracket^{\tt MC}$ is left oriented.
The “levels” in $\llbracket{{\mathcal{P}}}\rrbracket^{\tt MC}$ are the
configuration sizes, except for the set $\Gamma^{\leq 4}_{{\mathcal{P}}}$. We
formalize this as an abstraction function $level$ from the configuration set
$\Gamma_{{\mathcal{P}}}$ to (non-negative) integers.

$\displaystyle level(\gamma)=0$ $\displaystyle\qquad\text{ if
}\gamma\in\Gamma^{\leq 4}_{{\mathcal{P}}}$ $\displaystyle
level(\gamma)=|\gamma|$ otherwise

For a configuration $\gamma$ in $\\{\gamma~{}|~{}level(\gamma)>0\\}$, let
$X_{\gamma}$ be the random variable representing the next configuration
obtained after a single transition from $\gamma$. We then show that for all
configurations in $\\{\gamma~{}|~{}level(\gamma)>0\\}$, the single step
expected change in the $level$ is negative. That is forall
$\gamma\in\Gamma^{\geq 5}_{{\mathcal{P}}}$,
$\mathbb{E}(level(X_{\gamma}))\leq|\gamma|-\Delta$ where $\Delta$ is a
positive constant where,

$\mathbb{E}(level(X_{\gamma}))=\sum_{\gamma^{\prime}}level(\gamma^{\prime})\cdot{\texttt{M}}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)$

We show that
$\sum_{\gamma^{\prime}}|\gamma^{\prime}|\cdot{\texttt{M}}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)\leq|\gamma|-\Delta$,
(we replace $level(\gamma^{\prime})$ by $|\gamma^{\prime}|$ since
$level(\gamma^{\prime})\leq|\gamma^{\prime}|$). Additionally, $|\gamma|$ can
be written as
$|\gamma|\cdot\sum_{\gamma^{\prime}}{\texttt{M}}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)$,
and hence we want to show:

$\displaystyle\sum_{\gamma^{\prime}}(|\gamma^{\prime}|-|\gamma|)\cdot{\texttt{M}}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)<-\Delta$

Showing this helps us to conclude that
$\llbracket{{\mathcal{P}}}\rrbracket^{\tt MC}$ is left oriented. Now, we focus
on showing this.

#####  $\llbracket{{\mathcal{P}}}\rrbracket^{\tt MC}$ is left-oriented

Consider a transition from the configuration $\gamma^{t}$ (with
$|\gamma^{t}|\geq 5$), to the configuration $\gamma^{t+1}$ as a result of the
process ($\xrightarrow{}_{{\tt proc}}$) and update ($\xrightarrow{}_{{\tt
update}}$) sub-transitions. For a particular $\gamma^{t+1}$, let
$\gamma^{\prime}$ be the intermediate configuration satisfying
$\gamma^{t}\xrightarrow{}_{{\tt proc}}\gamma^{\prime}\xrightarrow{}_{{\tt
update}}\gamma^{t+1}$. We can write the single step change in expectation when
going from $\gamma^{t}$ to $\gamma^{t+1}$ as follows.

$\displaystyle\sum_{\gamma^{t+1}}(|\gamma^{t+1}|-|\gamma^{t}|)\cdot{\texttt{M}}_{{\mathcal{P}}}\left(\gamma^{t},\gamma^{t+1}\right)$
$\displaystyle=\sum_{\gamma^{\prime}}{\tt M}_{\tt
proc}\left(\gamma^{t},\gamma^{\prime}\right)\cdot\left(\underbrace{|\gamma^{\prime}|-|\gamma^{t}|}_{\xrightarrow{}_{{\tt
proc}}}+\sum_{\gamma^{t+1}}{\tt M}_{\tt
update}\left(\gamma^{\prime},\gamma^{t+1}\right)\cdot(\underbrace{|\gamma^{t+1}|-|\gamma^{\prime}|}_{\xrightarrow{}_{{\tt
update}}})\right)$

The first term $|\gamma^{\prime}|-|\gamma^{t}|$ is the number of elements
added to the buffer in $\gamma^{t}\xrightarrow{}_{{\tt proc}}\gamma^{\prime}$
and the expectation is over the $\xrightarrow{}_{{\tt proc}}$ probabilities
while the second term $|\gamma^{t+1}|-|\gamma^{\prime}|$ is the number of
elements removed from the buffer in $\gamma^{\prime}\xrightarrow{}_{{\tt
update}}\gamma^{t+1}$ and the expectation is over the $\xrightarrow{}_{{\tt
update}}$ probabilities.

Now we see that (by Figure 2) in any $\xrightarrow{}_{{\tt proc}}$ step either
one element is added to the buffer (in case of a write transition) or the
buffer remains the same (for all other transitions). In particular, even when
the disabled rule is taken, the configuration remains the same. We have the
following.

$\displaystyle\forall\gamma^{\prime}\qquad\gamma^{t}\xrightarrow{}_{{\tt
proc}}\gamma^{\prime}$ $\displaystyle\implies
0\leq|\gamma^{\prime}|-|\gamma^{t}|\leqslant 1$

Since this holds for all $\gamma,\gamma^{\prime}$ pairs, it certainly holds
for expected values, and we can substitute in the above equation:

$\displaystyle\sum_{\gamma^{t+1}}(|\gamma^{t+1}|-|\gamma^{t}|)\cdot{\texttt{M}}_{{\mathcal{P}}}\left(\gamma^{t},\gamma^{t+1}\right)$
$\displaystyle\leq\qquad\sum_{\gamma^{\prime}}{\tt M}_{\tt
proc}\left(\gamma^{t},\gamma^{\prime}\right)\cdot\left(1+\sum_{\gamma^{t+1}}{\tt
M}_{\tt
update}\left(\gamma^{\prime},\gamma^{t+1}\right)\cdot(|\gamma^{t+1}|-|\gamma^{\prime}|)\right)$

As for the update part of the transition, we consider a uniform distribution
over all possible update sequences from the state $\gamma^{\prime}$. Due to
the combinatorial term involved, the probability of an update that propagates
more writes to the memory is strictly greater than that of an update which
propagates shorter lengths. Even this conservative reasoning implies that the
update rule leads to a configuration with at most half the size with at least
probability of $\frac{1}{2}$, giving us the following bound. Below, ${\it
Prob}_{\xrightarrow{}_{{\tt update}}}\left(x\right)$ denotes the probability
of an update where $x$ specifies how many elements from the buffer are pushed.

$\displaystyle\sum_{\gamma^{t+1}}{\tt M}_{\tt
update}\left(\gamma^{\prime},\gamma^{t+1}\right)\cdot(|\gamma^{t+1}|-|\gamma^{\prime}|)$
$\displaystyle=-\sum_{i=0}^{|\gamma^{\prime}|}i\cdot{\it
Prob}_{\xrightarrow{}_{{\tt update}}}\left(i\text{ elements of the buffer are
updated}\right)$ $\displaystyle\leq-\frac{|\gamma^{\prime}|}{2}\cdot{\it
Prob}_{\xrightarrow{}_{{\tt update}}}\left(\text{at
least}\frac{|\gamma^{\prime}|}{2}\text{ elements are
updated}\right)\leq-\frac{|\gamma^{\prime}|}{4}$

Here the first inequality follows from the fact that we are discounting for
cases where less than $|\gamma^{\prime}|/2$ elements are updated. The second
inequality follows from the fact that the probability of updating at least
$|\gamma^{\prime}|/2$ elements is greater than $\frac{1}{2}$. We note that
this holds for each configuration $\gamma^{\prime}$, and hence substituting
this bound in the earlier expression, we get (noting that
$|\gamma^{\prime}|\geq|\gamma^{t}|\geq 5$),

$\displaystyle\sum_{\gamma^{t+1}}(|\gamma^{t+1}|-|\gamma^{t}|)\cdot{\texttt{M}}_{{\mathcal{P}}}\left(\gamma^{t},\gamma^{t+1}\right)$
$\displaystyle\leq\sum_{\gamma^{\prime}}{\tt M}_{\tt
proc}\left(\gamma^{t},\gamma^{\prime}\right)\cdot\left(1-\frac{|\gamma^{\prime}|}{4}\right)$
$\displaystyle\leq\sum_{\gamma^{\prime}}{\tt M}_{\tt
proc}\left(\gamma^{t},\gamma^{\prime}\right)\cdot\left(1-\frac{5}{4}\right)$
$\displaystyle\leq\left(1-\frac{5}{4}\right)\cdot\sum_{\gamma^{\prime}}{\tt
M}_{\tt proc}\left(\gamma^{t},\gamma^{\prime}\right)\leq-\frac{1}{4}$

This proves that $\llbracket{{\mathcal{P}}}\rrbracket^{\tt MC}$ is left-
oriented (for $\Delta=\frac{1}{4}$). Hence by invoking Theorem 2.1 from [29]
we get that, the level 0 set is an attractor. That is ${\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{T}}}\Box\Diamond\Gamma^{\leq
4}_{{\mathcal{P}}}\right)=1$.

Now we want to show that ${\it
Prob}_{{\mathcal{P}}}\left(\gamma\models\Box\Diamond\Gamma^{\tt
plain}_{{\mathcal{P}}}\right)=1$. But this follows directly from the notion of
probabilistic fairness (for details see Theorem 10.25 of [20]). We have (even
for infinite Markov chains $\mathcal{M}$) and (finite) sets of configurations
$T,T^{\prime}$,

${\it Prob}_{\mathcal{M}}\left(s\models\Box\Diamond T\right)={\it
Prob}_{\mathcal{M}}\left(s\models\bigwedge_{T^{\prime}\subseteq
Post^{*}(T)}\Box\Diamond T^{\prime}\right)$

We note that the sets $\Gamma^{\tt plain}_{{\mathcal{P}}}$ and $\Gamma^{\leq
4}_{{\mathcal{P}}}$ are indeed finite (since the buffer sizes are bounded) and
$\Gamma^{\tt plain}_{{\mathcal{P}}}$ is reachable from $\Gamma^{\leq
4}_{{\mathcal{P}}}$, since the update rule can simply empty all buffers with
non-zero probability. Hence instantiating $s=\gamma$, $T=\Gamma^{\leq
4}_{{\mathcal{P}}}$, $T^{\prime}=\Gamma^{\tt plain}_{{\mathcal{P}}}$ we have
that ${\it Prob}_{{\mathcal{P}}}\left(\gamma\models\Box\Diamond\Gamma^{\tt
plain}_{{\mathcal{P}}}\right)=1$ as desired.

##  Appendix 0.B Qualitative Reachability: Supplementary material for Sec. 6

In this section, we discuss the results for qualitative reachability and
repeated reachability, filling in the details ommitted in the main paper. In
particular, we provide algorithms for the almost-sure repeated reachability
and almost-never repeated reachability.

Then, we go on to prove Theorems 1 and 2.

###  0.B.1 Almost-Sure Repeated Reachability

The qualitative repeated reachability problem, differs from reachability in
that now we are interested in the property $\Box\Diamond\mathsf{l}$ i.e.,
whether $\mathsf{l}$ will be reached infinitely often. In a similar manner to
the case of reachability, the algorithm of Fig. 7 analyzes the transition
system $\llbracket{{\mathcal{P}}}\rrbracket^{\tt TS}$.

The difference between the two algorithms is that we do not need to transform
the program by removing the label $\mathsf{l}$ here, since reaching
$\mathsf{l}$ a finite number of times does not affect repeated reachability.
Therefore, we perform analysis directly on the input program ${\mathcal{P}}$.
As before, the loop on line 1 generates all the plain configurations one by
one, and performs the same tests as in the qualitative reachability algorithm
of Fig. 3. More precisely, the algorithm terminates and returns a negative
answer if it finds a plain configuration that is reachable from $\gamma_{\it
init}$ but that cannot reach $\mathsf{l}$. Otherwise, it returns a positive
answer.

Input: ${\mathcal{P}}$: program; $\gamma_{\it init}\in\Gamma_{{\mathcal{P}}}$:
configuration; $\mathsf{l}\in\mathsf{Lbl}_{\mathcal{P}}$: label.

1 for  _each $\gamma\in\Gamma^{\tt plain}_{{\mathcal{P}}}$_ do

2 if  _$\gamma_{\it init}\xrightarrow{*}_{{\mathcal{P}}}\gamma$ and
$\neg\left(\gamma\xrightarrow{*}_{{\mathcal{P}}}\mathsf{l}\right)$_ then
return _${\tt false}$_

3

return _${\tt true}$_

Algorithm 4 Qual_Rep_Reach

Figure 7: Almost-sure repeated reachability.

To see the correctness of the algorithm, we observe that it answers negatively
only if it finds a path with a positive probability from $\gamma_{\it init}$
to a plain configuration from which $\mathsf{l}$ is not reachable. Using a
similar reasoning to the case of reachability, this implies that the measure
of runs from $\gamma_{\it init}$ that reach $\mathsf{l}$ is smaller than one.
Therefore, the measure of runs from $\gamma_{\it init}$ that repeatedly reach
$\mathsf{l}$ is also smaller than one. In the other direction, if the
algorithm answers positively then there is no plain configuration that is
reachable from $\gamma_{\it init}$ but that cannot reach $\mathsf{l}$. Using
Lemma 5, as in Sec. 6.1, we conclude that any run $\rho$ from $\gamma_{\it
init}$ will almost surely repeatedly visit some plain configuration $\gamma$
from which $\mathsf{l}$ is reachable. Consequently, $\rho$ almost surely
visits $\mathsf{l}$ infinitely often.

###  0.B.2 Almost-Never (Repeated) Reachability

The almost-never variants of the (repeated) reachability problems,
Never_Qual_Reach resp. Never_Qual_Rep_Reach, ask whether the probabilities
equal to $0$ rather than $1$. The solution to Never_Qual_Reach is
straightforward, since ${\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Diamond\mathsf{l}\right)=0$ iff $\neg(\gamma_{\it
init}\xrightarrow{*}_{{\mathcal{P}}}\mathsf{l})$ the latter is decidable by
Lemma 4.

Input: ${\mathcal{P}}$: program; $\gamma_{\it init}\in\Gamma_{{\mathcal{P}}}$:
configuration; $\mathsf{l}\in\mathsf{Lbl}_{\mathcal{P}}$: label.

1 for  _each $\gamma\in\Gamma^{\tt plain}_{{\mathcal{P}}}$_ do

2 if  _$\gamma_{\it init}\xrightarrow{*}_{{\mathcal{P}}}\gamma$_ then

3 flag:=true

4 for  _each $\gamma^{\prime}\in\Gamma^{\tt plain}_{{\mathcal{P}}}$_ do

5 if  _$\gamma\xrightarrow{*}_{{\mathcal{P}}}\gamma^{\prime}$ and
$\neg\left(\gamma^{\prime}\xrightarrow{*}_{{\mathcal{P}}}\gamma\right)$_ then
flag:=false

6

7 if
_${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
flag}={\tt true}$ and $\gamma\xrightarrow{*}_{{\mathcal{P}}}\mathsf{l}$_ then
return _${\tt false}$_

8

return _${\tt true}$_

Algorithm 5 Never_Qual_Rep_Reach

Figure 8: Almost-never repeated reachability algorithm.

We give the algorithm for solving the almost-never repeated reachability
problem in Fig. 8. The algorithm searches for B-plain configurations that are
reachable from $\gamma_{\it init}$ and from which $\mathsf{l}$ is reachable.
If it detects such a configuration, it returns a negative answer. Otherwise,
it returns a positive answer. The outer loop cycles through all plain
configurations. For each such configuration $\gamma$ that is reachable from
$\gamma_{\it init}$, the inner loop checks whether $\gamma$ is a B-plain
configuration (by trying to search for a plain configuration which is
reachable but without a path back to $\gamma$).

We intuitively explain the algorithm as follows. Suppose there is a
$\gamma\in\Gamma^{\tt Bplain}_{{\mathcal{P}}}$ such that $\gamma_{\it
init}\xrightarrow{*}_{{\mathcal{P}}}\gamma\xrightarrow{*}_{{\mathcal{P}}}\mathsf{l}$.
By Lemma 5 and the fact that $\gamma$ is a B-plain configuration, any run from
$\gamma$ will almost surely visit $\gamma$ infinitely often. Hence by the
fairness property for Markov chains it follows that the run almost surely
visits $\mathsf{l}$ infinitely often and we return false. Conversely, assume
there is no B-plain configuration satisfying $\gamma_{\it
init}\xrightarrow{*}_{{\mathcal{P}}}\gamma\xrightarrow{*}_{{\mathcal{P}}}\mathsf{l}$.
By Lemma 6, we know that any run $\rho$ from $\gamma_{\it init}$ will visits
some B-plain configuration $\gamma$ infinitely often. Since $\mathsf{l}$ is
not reachable from $\gamma$ it follows that $\rho$ will almost never visit
$\mathsf{l}$.

###  0.B.3 Proofs for Sec. 6

See 1

##### Reachability

###### Proof

Decidability follows by proving that the algorithm given in Figure 3 gives the
correct answer and terminates, which we now do.

##### Correctness

(Algorithm returns false) When the algorithm returns false, we know that there
exists a plain configuration $\gamma$ and a finite length path $\gamma_{\it
init}\xrightarrow{*}_{{\mathcal{P}}^{\prime}}\gamma$, such that
$\neg(\gamma\xrightarrow{*}_{{\mathcal{P}}^{\prime}}\mathsf{l})$. Since it is
a finite path, it is taken with a non-zero probability, say p. Then we know
that ${\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Diamond\mathsf{l}\right)\leq 1-\texttt{p}<1$ and we are done.

(Algorithm returns true) Let the set of plain configurations (in the original
program ${\mathcal{P}}$) reachable from $\gamma_{\it init}$ be
$\Gamma^{\texttt{r-plain}}_{\mathcal{P}}$. Given that there are finitely many
plain configurations, $|\Gamma^{\texttt{r-plain}}_{\mathcal{P}}|$ is also
finite. Since the algorithm returned true we know that $\mathsf{l}$ is
reachable from each configuration in
$\Gamma^{\texttt{r-plain}}_{\mathcal{P}}$, with a finite length path and hence
some non-zero probability. Let p denote the minimum of these reachability
probabilities over the (finite) set $\Gamma^{\texttt{r-plain}}_{\mathcal{P}}$.
We must have $\texttt{p}>0$, since
$\Gamma^{\texttt{r-plain}}_{\mathcal{P}}\neq\phi$. Hence starting from any
configuration in $\Gamma^{\texttt{r-plain}}_{\mathcal{P}}$, the probability of
reaching $\mathsf{l}$ is at least $\texttt{p}>0$. Now, Lemma 5 implies that
the set $\Gamma^{\texttt{r-plain}}_{\mathcal{P}}$ is reached infinitely often,
${\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Box\Diamond\Gamma^{\texttt{r-plain}}_{\mathcal{P}}\right)=1$.

Then the result follows from the fairness theorem for Markov chains which
says,

${\it Prob}_{{\mathcal{P}}}\left(\gamma\models\Box\Diamond\Gamma\right)={\it
Prob}_{{\mathcal{P}}}\left(\gamma\models\bigwedge_{\gamma^{\prime}\in
Post^{*}(\Gamma)}\Box\Diamond\gamma^{\prime}\right).$

As a corollary, we get,

${\it
Prob}_{{\mathcal{P}}}\left(\gamma\models\Box\Diamond\Gamma\right)\leq{\it
Prob}_{{\mathcal{P}}}\left(\gamma\models\Box\Diamond\Gamma^{\prime}\right)\quad\quad\text{
for }\Gamma^{\prime}\subseteq~{}Post^{*}(\Gamma).$

In particular, instantiating $\gamma=\gamma_{\it
init},\Gamma=\Gamma^{\texttt{r-plain}}_{\mathcal{P}},\Gamma^{\prime}=\\{\gamma^{\prime}~{}|~{}\mathsf{l}\in\gamma^{\prime}\\}$,
we get

$\displaystyle{\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Box\Diamond\Gamma^{\texttt{r-plain}}_{\mathcal{P}}\right)=1$
$\displaystyle\leq{\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Box\Diamond\mathsf{l}\right)$ $\displaystyle\leq{\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it init}\models\Diamond\mathsf{l}\right).$

Both the inequalities must be equalities which completes the proof for
correctness.

##### Termination

The set of plain configurations is finite, and hence the loop performs finite
iterations. At each iteration, both of the queries are decidable as discussed
in Lemma 4 and Lemma 3. This shows termination and proves the theorem.

##### Repeated Reachability

###### Proof

This proof is similar to its reachability counterpart. The algorithm returns
true only when all plain configurations
$\gamma\in\Gamma^{\texttt{r-plain}}_{\mathcal{P}}$ reachable from $\gamma_{\it
init}$, are such that $\mathsf{l}$ is also reachable from $\gamma$. By Lemma 5
we know that any run from $\gamma_{\it init}$ visits almost surely, some plain
configuration infinitely often. In our case, any run from $\gamma_{\it init}$
visits some configuration from
$\gamma\in\Gamma^{\texttt{r-plain}}_{\mathcal{P}}$ infinitely often; since
$\mathsf{l}$ is reachable from $\gamma$, the run from $\gamma_{\it init}$
which reaches $\mathsf{l}$ will visit almost surely, $\gamma$ again and again,
and hence $\mathsf{l}$ also, infinitely often, almost surely. In particular,
we show correctness and termination for the algorithm in Figure 7.

##### Correctness

Proof of correctness is identical to the earlier. In particular, at the last
step we also showed

${\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Box\Diamond\Gamma^{\texttt{r-plain}}_{\mathcal{P}}\right)=1\leq{\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Box\Diamond\mathsf{l}\right)$

where the inequality must be an equality, owing to the probability values.

##### Termination

The set of plain configurations is finite, and hence the loop performs finite
iterations. At each iteration, both of the queries are decidable as discussed
in Lemma 4 and Lemma 3. This shows termination and proves the theorem.

##### Almost-Never Repeated Reachability

###### Proof

_Correctness_. (Algorithm returns false) When the algorithm returns false, we
know that there exists a B-plain configuration $\gamma$ reachable from
$\gamma_{\it init}$ and a finite length path
$\gamma\xrightarrow{*}_{{\mathcal{P}}}\mathsf{l}$. Since it is a finite path,
it is taken with a non-zero probability, say p. By Lemma 5 and the fact that
$\gamma$ can reach back to itself, we know that any run from $\gamma$ visits
$\gamma$ infinitely often. Since $\mathsf{l}$ is reachable from $\gamma$ with
probability $\texttt{p}>0$, we can reach $\mathsf{l}$ infinitely often with
probability $>0$. Thus, ${\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Box\Diamond\mathsf{l}\right)>0$ and we are done.

(Algorithm returns true) Assume that all B-plain configurations $\gamma$
reachable from $\gamma_{\it init}$ are such that
$\neg(\gamma\xrightarrow{*}_{{\mathcal{P}}}\mathsf{l})$. Then we know by Lemma
5, $\gamma$ is visited infinitely often on any run from $\gamma_{\it init}$;
since $\mathsf{l}$ is not reachable from $\gamma$, it is not repeatedly
reachable along any run from $\gamma_{\it init}$ ( if $\mathsf{l}$ were
repeatedly reachable on some run from $\gamma_{\it init}$, then since some
B-plain configuration $\gamma$ is also visited infinitely often along that
run, it would result in reaching $\mathsf{l}$ from $\gamma$, contradicting the
non reachability of $\mathsf{l}$ from $\gamma$). Thus, the probability of
repeatedly reaching $\mathsf{l}$ from $\gamma_{\it init}$ is 0 : ${\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Box\Diamond\mathsf{l}\right)=0$.

##### Termination

The set of plain configurations is finite, and hence the loop performs finite
iterations. At each iteration, both of the queries (checking if a plain
configuration $\gamma$ is B-plain : that is, it is reachable from itself, as
well as whether $\mathsf{l}$ is reachable from $\gamma$) are decidable as
discussed in Lemma 4 and Lemma 3. This shows termination and proves the
theorem.

See 2

##### Reachability

######  Proof (Proof)

The proof follows from a reduction from the (non-probabilistic) control-state
reachability problem for TSO, which is known to be non-primitive recursive
[12].

Concretely, consider an instance program ${\mathcal{P}}$ of the (non-
probabilistic) reachability problem for TSO. We ask whether $\gamma_{\it
init}\xrightarrow{*}_{{\mathcal{P}}}\mathsf{l}^{*}$ for some label
$\mathsf{l}^{*}\in\mathsf{Lbl}_{p_{r}}$ (we ask for reachability of process
$p_{r}$, and other processes can be in arbitrary labels).

##### Reduction construction

For the reduction, we construct a program ${\mathcal{P}}^{\prime}$ obtained
from ${\mathcal{P}}$ by modifying process $p_{r}$, and adding a new process
$p_{new}$. All other processes of ${\mathcal{P}}$ remain unchanged.
${\mathcal{P}}^{\prime}$ has all the shared variables and local registers as
${\mathcal{P}}$, and a new shared variable $x$, as well as a new local
register $a$. As always, all shared variables and local registers are
initialized to 0. Assume the finite data domain of ${\mathcal{P}}$ (and
${\mathcal{P}}^{\prime}$) consists of values $\\{v_{0},v_{1},\dots,v_{n}\\}$,
where $v_{0}=0$.

  1. 1.

$p_{new}$ consists of a sequence of instructions which starts by checking if
$a$ is $v_{0}$, and if so, goes to the next two instructions which are
$a:=v_{1};x:=a$. This is followed by an instruction which checks if $a$ is
$v_{1}$, and if so, goes to the next two instructions which are
$a:=v_{2};x:=a$. This is continued till we reach the instruction which checks
if $a$ is $v_{n}$ and if so, goes to the first instruction. Thus, $p_{new}$ is
a loop which repeatedly writes values $v_{0},\dots,v_{n}$ to $x$.

  2. 2.

Now we discuss the modifications in $p_{r}$.

     * •

We add two fresh instruction labels $\mathsf{l}_{win}$ and $\mathsf{l}_{lose}$
to $p_{r}$ such that

$\mathsf{l}_{win}:{\tt{if}}~{}(a\geq
0)~{}{\tt{then}}~{}~{}\mathsf{l}_{win},~{}~{}\mathsf{l}_{lose}:{\tt{if}}~{}(a\geq
0)~{}{\tt{then}}~{}~{}\mathsf{l}_{lose}$

     * •

Immediately before each instruction label $\mathsf{l}\neq\mathsf{l}^{*}$ in
$p_{r}$, we add two fresh instructions labeled $\mathsf{l}_{pre1}$ and
$\mathsf{l}_{pre2}$ as follows.

$\mathsf{l}_{pre1}:a:=x,~{}~{}~{}~{}\mathsf{l}_{pre2}:{\tt{if}}(a=v_{i})~{}{\tt{then}}~{}~{}\mathsf{l}_{win}$

Thus, if the value of $a$ is not $v_{i}$, control moves to $\mathsf{l}$;
otherwise to $\mathsf{l}_{win}$.

     * •

Immediately before $\mathsf{l}^{*}$, we add two fresh instructions labeled
$\mathsf{l}^{*}_{pre1}$ and $\mathsf{l}^{*}_{pre2}$ as follows.

$\mathsf{l}^{*}_{pre1}:a:=x,~{}~{}~{}~{}\mathsf{l}^{*}_{pre2}:{\tt{if}}(a=v_{i})~{}{\tt{then}}~{}~{}\mathsf{l}_{lose}$

Thus, if the value of $a$ is not $v_{i}$, control moves to $\mathsf{l}^{*}$;
otherwise to $\mathsf{l}_{lose}$.

We see that
$\neg(\mathsf{l}_{win}\xrightarrow{*}_{{\mathcal{P}}^{\prime}}\mathsf{l}_{lose})$
and
$\neg(\mathsf{l}_{lose}\xrightarrow{*}_{{\mathcal{P}}^{\prime}}\mathsf{l}_{win})$.

##### Equivalence

For this program ${\mathcal{P}}^{\prime}$, we ask the probabilistic
qualitative reachability problem: ${\it
Prob}_{{\mathcal{P}}^{\prime}}\left(\gamma_{\it
init}\models\Diamond\mathsf{l}_{win}\right)=1?$ We claim that an answer to
this question, allows us to decide reachability to $\mathsf{l}^{*}$ in
${\mathcal{P}}$.

($\Rightarrow$) If the answer to this is yes, we know that $\neg(\gamma_{\it
init}\xrightarrow{*}_{{\mathcal{P}}}\mathsf{l}^{*})$, since a (finite-length)
path to $\mathsf{l}^{*}$, implies a finite length path to
$\mathsf{l}^{*}_{pre1},\mathsf{l}^{*}_{pre2}$. This implies a finite and hence
non-zero probability path to reach $\mathsf{l}_{lose}$, from which there is no
path to $\mathsf{l}_{win}$.

($\Leftarrow$) On the other hand, if $\mathsf{l}^{*}$ is not reachable in
${\mathcal{P}}$, we have $\gamma_{\it
init}\models\Box(\mathsf{Lbl}_{p_{r}}\setminus\\{\mathsf{l}^{*}\\})$ and hence
$\gamma_{\it
init}\models\Box(\mathsf{Lbl}_{p^{\prime}_{r}}\setminus\\{\mathsf{l}_{lose},\mathsf{l}^{*},\mathsf{l}^{*}_{pre1},\mathsf{l}^{*}_{pre2}\\})$
in ${\mathcal{P}}^{\prime}$. In the extended program ${\mathcal{P}}^{\prime}$,
define $\Gamma^{win}_{{\mathcal{P}}^{\prime}}$ as the set of configurations
with $\lambda(p_{r}^{\prime})=\mathsf{l}_{win}$. Additionally, we have that
all reachable configurations
$\mathsf{Lbl}_{p^{\prime}_{r}}\setminus\\{\mathsf{l}_{lose},\mathsf{l}^{*},\mathsf{l}^{*}_{pre1},\mathsf{l}^{*}_{pre2}\\}$
can reach $\Gamma^{win}_{{\mathcal{P}}^{\prime}}$ in a single step (with a
non-zero probability). Thus, $\mathsf{l}_{win}$ is reachable in a single step
with non zero probability from all configurations which are reachable from
$\gamma_{\it init}$. This implies that the probability to reach
$\Gamma^{win}_{{\mathcal{P}}^{\prime}}$ from $\gamma_{\it init}$ is 1, which
proves the lemma.

##### Repeated Reachability

######  Proof (Proof)

This proof is identical to its reachability counterpart. In particular note
that $\mathsf{l}_{win},\mathsf{l}_{lose}$ are associated with self loop
transitions, so, reachability and repeated reachability for
$\mathsf{l}_{win},\mathsf{l}_{lose}$ are equivalent problems for program
${\mathcal{P}}^{\prime}$.

##### Never Reachability

######  Proof (Proof)

We can use the construction above, once again. Note that by construction,
reaching $\mathsf{l}_{win}$ is same as never reaching label
$\mathsf{l}_{lose}$. We have already established the reduction from
reachability to some $\mathsf{l}$ to the problem ${\it
Prob}_{{\mathcal{P}}^{\prime}}\left(\gamma_{\it
init}\models\Diamond\mathsf{l}_{win}\right)=1?$. Since ${\it
Prob}_{{\mathcal{P}}^{\prime}}\left(\gamma_{\it
init}\models\Diamond\mathsf{l}_{win}\right)=1?$ iff ${\it
Prob}_{{\mathcal{P}}^{\prime}}\left(\gamma_{\it
init}\models\Diamond\mathsf{l}_{lose}\right)=0?$, we now have the reduction
from reachability in classical TSO to the never reachability in probabilistic
TSO.

##### Never Repeated Reachability

######  Proof (Proof)

Once again, by construction, reaching $\mathsf{l}_{win}$ is same as never
repeatedly reaching label $\mathsf{l}_{lose}$. Thus, ${\it
Prob}_{{\mathcal{P}}^{\prime}}\left(\gamma_{\it
init}\models\Diamond\mathsf{l}_{win}\right)=1?$ iff ${\it
Prob}_{{\mathcal{P}}^{\prime}}\left(\gamma_{\it
init}\models\Box\Diamond\mathsf{l}_{lose}\right)=0?$, we now have the
reduction from reachability in classical TSO to the never repeated
reachability in probabilistic TSO.

##  Appendix 0.C Quantitative Reachability: Supplementary material for Sec. 7

In this section, we provide the algorithm for the approximate repeated
reachability problem and then provide proofs of correctness and termination.

###  0.C.1 Algorithmic details for Approximate Quantitative Repeated
Reachability

In the case of the approximate quantitative repeated reachability problem,
Quant_Rep_Reach, our task is to approximate the probability of visiting a
given label infinitely often. We provide an algorithm for approximate
quantitative reachability in Figure 9.

Input: ${\mathcal{P}}$: program; $\gamma_{\it init}\in\Gamma_{{\mathcal{P}}}$:
configuration; $\mathsf{l}\in\mathsf{Lbl}_{\mathcal{P}}$: label;
$\varepsilon\in\mathbb{R}^{>0}$: precision.

1 Var

2
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
flag},{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
posflag}\in\mathbb{B}$: Boolean flags

3
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
BPlain}\subseteq\Gamma^{\tt plain}_{{\mathcal{P}}}$: subset of the plain
configurations

4
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx},{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}\in\mathbb{R}$: under-approximations

5
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}\in{(\Gamma_{{\mathcal{P}}}\times\mathbb{R})}^{*}$: queue

6

7${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}:=0$;
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}:=0$

8
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
BPlain}:=\emptyset$;
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}:=\left\langle\gamma_{\it init},1\right\rangle$

9 for  _each $\gamma\in\Gamma^{\tt plain}_{{\mathcal{P}}}$_ do

10 flag:=true

11 for  _each $\gamma^{\prime}\in\Gamma^{\tt plain}_{{\mathcal{P}}}$_ do

12 if  _$(\gamma\xrightarrow{*}_{{\mathcal{P}}}\gamma^{\prime})$ and
$\neg(\gamma^{\prime}\xrightarrow{*}_{{\mathcal{P}}}\gamma)$_ then

13 flag:=false

14 if
_${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
flag}={\tt true}$_ then

15
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
BPlain}:={\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
BPlain}\cup\left\\{\gamma\right\\}$

16while
_${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}+{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx} <1-\varepsilon$_ do

17 $\left\langle\gamma,\phi\right\rangle:={\tt
head}\left({{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}}\right)$;
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}:={\tt
tail}\left({{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}}\right)$

18
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
posflag}:={\tt true}$

19 for  _each
$\gamma^{\prime}\in{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
BPlain}$_ do

20 if
_$(\gamma\stackrel{{\scriptstyle*}}{{\rightarrow}}_{\mbox{\tiny${{\mathcal{P}}}$}}\gamma^{\prime})\land\neg(\gamma^{\prime}\stackrel{{\scriptstyle*}}{{\rightarrow}}_{\mbox{\tiny${{\mathcal{P}}}$}}\mathsf{l})$_
then
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
posflag}:={\tt false}$

21

22 if
_${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
posflag}={\tt true}$_ then
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}:={\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}+\phi$

23 else if
_$\neg(\gamma\stackrel{{\scriptstyle*}}{{\rightarrow}}_{\mbox{\tiny${{\mathcal{P}}}$}}\mathsf{l})$_
then
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}:={\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}+\phi$

24 else

25 for  _each $\gamma^{\prime}$ with
$\gamma\rightarrow_{\mbox{\tiny${{\mathcal{P}}}$}}\gamma^{\prime}$_ do
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}:={\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}\boldsymbol{\cdot}\left\langle\gamma^{\prime},\phi\cdot{\texttt{M}}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)\right\rangle$

26

return
_${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}$_

Algorithm 6 Quant_Rep_Reach

Figure 9: Quantitative repeated reachability algorithm.

The algorithm for repeated reachability is very similar to the one for
reachability. The main difference compared to algorithm of Fig. 4 is the
condition of the if-statement (line 19). Instead of checking whether we have
reached label $\mathsf{l}$, we now increase the value of
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}$ if there is no $\gamma$-path to a configuration from which
$\mathsf{l}$ is not reachable. To check this condition, we first compute set
of B-plain configurations and store them in
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
BPlain}$. We go through the B-plain configurations that are reachable from the
current configuration $\gamma$ one by one. We increase the value of
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}$ if $\mathsf{l}$ is reachable from all such configurations.

Again, we let
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}$ and
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}^{(i)}}$ represent the value of
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}$ resp.
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}$ prior to performing the $i^{\it th}$ iteration. The partial
correctness of the algorithm, follows from the following properties of the
algorithm: (i) The value of
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}$ increases only by weights of $\gamma_{\it init}$-paths that visit
configuration $\gamma$ from which all reachable B-plain configurations can in
turn reach $\mathsf{l}$. We argue that any $\gamma$-run will almost surely
repeatedly reach $\mathsf{l}$. To see that, we know by Lemma 6 that $\rho$
will almost surely visit the set of B-plain configurations. By finiteness of
the set, $\rho$ will almost surely visit a particular B-plain configuration
$\gamma^{\prime}\in\Gamma^{\tt Bplain}_{{\mathcal{P}}}$ infinitely often.
Since $\gamma^{\prime}\models\Diamond\mathsf{l}$ it follows that $\rho$ will
almost surely visit $\mathsf{l}$ infinitely often. It follows that
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}\leq{\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Box\Diamond\mathsf{l}\right)$. (ii) We increase the value of
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}$ only by weights of $\gamma_{\it init}$-paths that end up at a
configuration $\gamma$ from which $\mathsf{l}$ is not reachable. Since
$(\gamma\models\Diamond\mathsf{l})=\emptyset$, and hence also
$(\gamma\models\Box\Diamond\mathsf{l})=\emptyset$. Therefore,
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}^{(i)}}\leq{\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\neg\Box\Diamond\mathsf{l}\right)$. (iii) If the algorithm
terminates after the $i^{\it th}$ iteration, the condition of the while-loop
implies that
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}+{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}^{(i)}}>1-\varepsilon$. From (i), (ii), and (iii), it follow that if
the termination point is $i$ then:

${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}\leq{\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Box\Diamond\mathsf{l}\right)\leq
1-{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}^{(i)}}<{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}+\varepsilon$

Therefore, on termination,
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}$ is within $\varepsilon$-precision of $\theta$.

###  0.C.2 Proofs of correctness for Sec. 7

See 3

###### Proof

Decidability follows by proving that the algorithm given in Figure 4 gives the
correct answer and terminates, which we now do.

##### Correctness

We have that
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}$ is monotone in $i$ and that

${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}\leq{\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Diamond\mathsf{l}\right)$

since we only accumulate probabilities of distinct paths reaching $\mathsf{l}$
in
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}$. On the other hand, for
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}^{(i)}}$ we have the following inequality,

${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}^{(i)}}\leq{\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\neg\Diamond\mathsf{l}\right)=1-{\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it init}\models\Diamond\mathsf{l}\right).$

This in turn follows from the fact that
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}^{(i)}}$ accumulates probabilities of distinct (infinite) paths which
never will reach $\mathsf{l}$. Hence,
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}^{(i)}}+{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}\geq 1-\varepsilon$ implies that

${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}\leq{\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Diamond\mathsf{l}\right)\leq
1-{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}^{(i)}}\leq{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}+\varepsilon$

showing that
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}$ approximates ${\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Diamond\mathsf{l}\right)$ to $\varepsilon$ precision and proving
correctness of the algorithm.

##### Termination

This proof crucially uses the existence of a finite set $\Gamma^{\tt
plain}_{{\mathcal{P}}}$ which is reached repeatedly with probability one and
the fairness theorem on Markov chains. The fairness theorem says that for a
Markov chain with (set of) states $S_{1}$ and $S_{2}$, if there is a non-zero
probability path from $S_{1}$ to $S_{2}$, then the probability of taking a
path which reaches $S_{1}$ infinitely often but which never reaches $S_{2}$ is
zero.

As introduced earlier in the main text, we denote by
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}},{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}^{(i)}}$ the iterates at the $i$ iteration of the while-loop and
additionally we define

$\texttt{UndetApprx}^{(i)}=1-{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}-{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}^{(i)}}$

If we can show that $\lim_{i\rightarrow\infty}\texttt{UndetApprx}^{(i)}=0$ we
are done since we have that

${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}\leq{\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Diamond\mathsf{l}\right)\leq{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}+\texttt{UndetApprx}^{(i)}.$

We now work towards this goal. First we observe that the algorithm performs a
breadth-first traversal of the space of configurations. Hence at each loop
iteration, the configuration which is dequeued from the
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}$-queue is associated with a certain depth of search. We denote this
depth by $\mathsf{depth}(i)$ for iteration $i$. Conversely, for each depth
$d$, there exists a maximal loop-iteration $i$ that considers a configuration
at that depth, denoted by
$\mathsf{maxiter}(d)=\max_{i}\\{\mathsf{depth}(i)=d\\}$. At each depth, there
are only finitely many configurations which are considered, and hence, $\max$
is over a finite set, and is well defined. The finiteness of the number of
configurations at each depth follows from the observation that the $Post$ set
of each configuration $\gamma$ is finite (concretely it can be represented as
a polynomial in the size of the configuration, $|\gamma|$). This implies that
$\lim_{i\rightarrow\infty}\mathsf{depth}(i)=\infty$. Hence, the limits,
whether taken over the loop iteration count $i$ or over the depth of search
$\mathsf{depth}(i)$ directly are equal. Hence we switch to the limits over the
depth of search that is more convenient to reason about.

$\lim_{i\rightarrow\infty}\texttt{UndetApprx}^{(i)}=\lim_{d\rightarrow\infty}\texttt{UndetApprx}^{(\mathsf{maxiter}(d))}$

Now for a depth $d$, consider the set of all paths of length $d$: $\gamma_{\it
init}\boldsymbol{\cdot}\Gamma^{d}$. A path $\rho\in\gamma_{\it
init}\boldsymbol{\cdot}\Gamma^{d}$ can be one of three types: (1) which have
reached $\mathsf{l}$, i.e $\exists i,\pi[i]=\mathsf{l}$ (2) which cannot reach
$\mathsf{l}$: $\neg(\pi[d]\xrightarrow{}_{{\mathcal{P}}}\mathsf{l})$ and (3)
undetermined (where none of (1,2) hold). The paths from (1) and (2) have
probabilities corresponding to
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(\mathsf{maxiter}(d))}}$ and
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}^{(\mathsf{maxiter}(d))}}$. The probability that a path belongs to
(3) on the other hand is given by
$\texttt{UndetApprx}^{(\mathsf{maxiter}(d))}$.

For a given $d$, denote the set of these undetermined paths from (3) as
$\mathsf{Undet}(d)$. Let $U=\\{\pi~{}|~{}\forall
d,\pi[0]\cdots\pi[d]\in\mathsf{Undet}(d)\\}\subseteq\gamma_{\it
init}\boldsymbol{\cdot}{\Gamma}^{\omega}$. These are the set of infinite paths
from $\gamma_{\it init}$, for which all finite prefixes are undetermined w.r.t
reachability to $\mathsf{l}$. Now we know that ${\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it init}\models\Box\Diamond\Gamma^{\tt
plain}_{{\mathcal{P}}}\right)=1$. Partition $\Gamma^{\tt
plain}_{{\mathcal{P}}}=\Gamma_{\mathcal{P}}^{\texttt{pos-
plain}}\uplus\Gamma_{\mathcal{P}}^{\texttt{neg-plain}}$ into two: (1)
$\Gamma_{\mathcal{P}}^{\texttt{pos-
plain}}=\\{\gamma~{}|~{}\gamma\xrightarrow{}_{{\mathcal{P}}}\mathsf{l}\\}$ and
(2) $\Gamma_{\mathcal{P}}^{\texttt{neg-
plain}}=\\{\gamma~{}|~{}\neg(\gamma\xrightarrow{}_{{\mathcal{P}}}\mathsf{l})\\}$.
We have the following since $\Gamma^{\tt plain}_{{\mathcal{P}}}$ is reached
repeatedly with probability one.

${\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it init}\models U\right)={\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models(U\land\Box\Diamond\Gamma^{\tt plain}_{{\mathcal{P}}})\right)$

However, any path satisfying
$\pi\models\Diamond\Gamma_{\mathcal{P}}^{\texttt{neg-plain}}$ cannot belong to
$U$ (if it belongs to $U$, each finite prefix is undetermined wrt
$\mathsf{l}$, contradicting $\Diamond\Gamma_{\mathcal{P}}^{\texttt{neg-
plain}}$ which is determined to not reach $\mathsf{l}$), we must have the
following.

${\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it init}\models U\right)={\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models(U\land\Box\Diamond\Gamma_{\mathcal{P}}^{\texttt{pos-
plain}})\right)$

Since $\Gamma^{\tt plain}_{{\mathcal{P}}}$ is finite so it
$\Gamma_{\mathcal{P}}^{\texttt{pos-plain}}$ and we have

${\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it init}\models
U\right)\leq\sum_{\gamma\in\Gamma_{\mathcal{P}}^{\texttt{pos-plain}}}{\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models(U\land\Box\Diamond\gamma)\right)$

where the sum is over a finite set. Now $U$ consists of paths which never
reach $\mathsf{l}$. However these paths reach
$\Gamma_{\mathcal{P}}^{\texttt{pos-plain}}$ infinitely often. Consequently,
since each $\gamma\in\Gamma_{\mathcal{P}}^{\texttt{pos-plain}}$ has a finite
path (with non-zero probability) to $\mathsf{l}$, and by the fairness theorem
on Markov chains we must have, for all
$\gamma\in\Gamma_{\mathcal{P}}^{\texttt{pos-plain}}$,

${\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models(U\land\Box\Diamond\gamma)\right)=0,$

and hence,

${\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it init}\models U\right)\leq 0$

To finish the proof note that the approximation margin term
$\texttt{UndetApprx}^{(d)}$ approaches ${\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it init}\models U\right)$ as $d$
approaches infinity (since at a given value of $d$ it expresses the
probability of taking paths which are undetermined for $d$ steps). Hence we
have

$\lim_{d\rightarrow\infty}\texttt{UndetApprx}^{(\mathsf{maxiter}(d))}={\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it init}\models U\right)=0.$

Proving the requisite claim and hence the thorem.

See 4

###### Proof

Decidability follows by proving that the algorithm given in Figure 9 gives the
correct answer and terminates, which we now do.

##### Correctness

The proof of correctness is similar to that for Theorem 3. In particular, the
only difference is that
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}$ and
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}^{(i)}}$ now estimate (from below) the probabilities ${\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Box\Diamond\mathsf{l}\right)$ and ${\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\neg\Box\Diamond\mathsf{l}\right)$. The remaining analysis follows
replacing reachability by repeated reachability.

##### Termination

The proof is similar to the termination argument for Theorem 3. There are two
main differences. First the definition of the undetermined set of infinite
paths ($U$ in Theorem 3) changes: we call this set $V$ here. Secondly we must
use a stronger variant of the fairness theorem on Markov chains, which says
that for two (sets of) states $S_{1},S_{2}$ if we have a non-zero probability
path from $S_{1}$ to $S_{2}$ then the probability of taking infinite paths
which reach $S_{1}$ infinitely often, but reach $S_{2}$ only finitely often is
zero.

To begin, we once again define
$\texttt{UndetApprx}^{(i)}=1-{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}-{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}^{(i)}}$ and invoke the finite branching of the transition system to
go from limit over the iteration count to limit over the depth of search. The
following two relations hold.

$\displaystyle{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}$ $\displaystyle\leq{\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Diamond\mathsf{l}\right)\leq{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}+\texttt{UndetApprx}^{(i)}$
$\displaystyle\lim_{i\rightarrow\infty}\texttt{UndetApprx}^{(i)}$
$\displaystyle=\lim_{d\rightarrow\infty}\texttt{UndetApprx}^{(\mathsf{maxiter}(d))}$

Then once again it remains to prove:
$\lim_{d\rightarrow\infty}\texttt{UndetApprx}^{(\mathsf{maxiter}(d))}=0$.

Each path $\rho\in\gamma_{\it init}\boldsymbol{\cdot}\Gamma^{d}$ (from the
ones considered upto depth $d$) fall into three (disjoint) sets: (1) which
henceforth will reach $\mathsf{l}$ infinitely often, i.e $\exists i\in[0\cdots
d],\pi[i]\models\forall\Box\exists\lozenge\mathsf{l}$ (2) which cannot reach
$\mathsf{l}$: $\neg(\pi[d]\xrightarrow{}_{{\mathcal{P}}}\mathsf{l})$ and (3)
undetermined (in none of the sets (1,2)). The probability that a path belongs
to (3) is given by $\texttt{UndetApprx}^{(\mathsf{maxiter}(d))}$.

For a given $d$, denote the set of these undetermined paths from (3) as
$\mathsf{RepUndet}(d)$. Let $V=\\{\pi~{}|~{}\forall
d,\pi[0]\cdots\pi[d]\in\mathsf{RepUndet}(d)\\}\subseteq\gamma_{\it
init}\boldsymbol{\cdot}{\Gamma}^{\omega}$. These are infinite paths from
$\gamma_{\it init}$, for which all finite prefixes are undetermined w.r.t
repeated reachability to $\mathsf{l}$. Invoking ${\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it init}\models\Box\Diamond\Gamma^{\tt
plain}_{{\mathcal{P}}}\right)=1$ we partition $\Gamma^{\tt
plain}_{{\mathcal{P}}}=\Gamma_{\mathcal{P}}^{\texttt{pos-
plain}}\uplus\Gamma_{\mathcal{P}}^{\texttt{neg-plain}}$: (1)
$\Gamma_{\mathcal{P}}^{\texttt{pos-
plain}}=\\{\gamma~{}|~{}\gamma\xrightarrow{\mathsf{l}}_{{\mathcal{P}}}\\}$ and
(2) $\Gamma_{\mathcal{P}}^{\texttt{neg-
plain}}=\\{\gamma~{}|~{}\neg(\gamma\xrightarrow{}_{{\mathcal{P}}}\mathsf{l})\\}$.
We have the following since $\Gamma^{\tt plain}_{{\mathcal{P}}}$ is reached
repeatedly with probability one.

${\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it init}\models V\right)={\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models(V\land\Box\Diamond\Gamma^{\tt plain}_{{\mathcal{P}}})\right)$

However, any path satisfying
$\pi\models\Diamond\Gamma_{\mathcal{P}}^{\texttt{neg-plain}}$ cannot belong to
$V$ (as it is determined to not reach $\mathsf{l}$, it cannot be in $V$), we
must have the following.

${\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it init}\models V\right)={\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models(V\land\Box\Diamond\Gamma_{\mathcal{P}}^{\texttt{pos-
plain}})\right)$

Since $\Gamma^{\tt plain}_{{\mathcal{P}}}$ is finite so it
$\Gamma_{\mathcal{P}}^{\texttt{pos-plain}}$ and we have

${\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it init}\models
V\right)\leq\sum_{\gamma\in\Gamma_{\mathcal{P}}^{\texttt{pos-plain}}}{\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models(V\land\Box\Diamond\gamma)\right)$

where the sum is over a finite set. Now $V$ consists of paths which never
reach $\mathsf{l}$. However these paths reach
$\Gamma_{\mathcal{P}}^{\texttt{pos-plain}}$ infinitely often. Consequently,
since each $\gamma\in\Gamma_{\mathcal{P}}^{\texttt{pos-plain}}$ has a finite
path (with non-zero probability) to $\mathsf{l}$, and by the (extended)
fairness theorem on Markov chains we must have the probability of repeatedly
reaching $\gamma\in\Gamma_{\mathcal{P}}^{\texttt{pos-plain}}$ yet reaching
$\mathsf{l}$ only finitely many times is zero:

${\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models(V\land\Box\Diamond\gamma)\right)=0,$

and hence,

${\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it init}\models V\right)\leq 0$

Again note that the approximation margin term $\texttt{UndetApprx}^{(d)}$
approaches ${\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it init}\models V\right)$
as $d$ approaches infinity (since at a given value of $d$ it expresses the
probability of taking paths which are undetermined for $d$ steps). Hence we
have

$\lim_{d\rightarrow\infty}\texttt{UndetApprx}^{(\mathsf{maxiter}(d))}={\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it init}\models V\right)=0.$

##  Appendix 0.D Gravitation to small configurations: Proofs for Sec.8

We give the full details of the proof of Lemma 7. First, we recall the
classical Gambler’s ruin problem. We show Lemma 8 by comparing the probability
measures of runs in the gambler’s ruin problem with probability measures of
runs from small configurations.

###  0.D.1 The Gambler’s Ruin Problem

We consider the family of Gambler’s Ruin Markov chains
${\mathcal{C}}_{p,q}^{G}=\left\langle\mathbb{N},{\texttt{M}}^{G}_{p,q}\right\rangle$.
The family is parameterized by two positive real numbers
$p,q\in\mathbb{R}^{>0}$ such $p+q=1$. For each instantiation of the
parameters, we get a concrete Markov chain. The set of configurations is the
set of natural numbers, and the probability matrix is parameterized by $p$ and
$q$. More precisely, we have ${\texttt{M}}^{G}_{p,q}(i,i+1)=p$ for $i>0$,
${\texttt{M}}^{G}_{p,q}(i,i-1)=q$ for $i>0$, and ${\texttt{M}}^{G}(0,0)=1$. In
other words, the left-most configuration $0$ is a sink (a configuration which
we cannot leave). In configurations different from $0$, we move right with
probability $p$ and move left with probability $q$. If $q\geq p$ we say that
the Markov chain is “left-oriented”; otherwise we say it “right-oriented”. The
following lemma is classical.

###### Lemma 0.D.1

If $p\leq q$ then ${\it Prob}_{{\mathcal{C}}_{p,q}^{G}}\left(k\models\Diamond
0\right)=1$ for all $k\in\mathbb{N}$.

Lemma 0.D.1 tells us that if the Markov is left-oriented then, from any
configuration, we will almost surely reach the sink state.

The following lemma states that if the Markov chain is left-oriented then the
probability of reaching a left segment of the chain, within a given number of
steps, is higher if we are closer to the left.

###### Lemma 0.D.2

If $p\leq q$ then ${\it
Prob}_{{\mathcal{C}}_{p,q}^{G}}\left(k\models\Diamond^{\\!\\!\geq
n}0\right)\leq{\it
Prob}_{{\mathcal{C}}_{p,q}^{G}}\left(k+1\models\Diamond^{\\!\\!\geq
n}0\right)$ for all $k,n\in\mathbb{N}$.

###### Proof

We use induction on $n$. For the base case, with $n=0$, we know that ${\it
Prob}_{{\mathcal{C}}_{p,q}^{G}}\left(k+1\models\Diamond^{\\!\\!\geq
0}0\right)={\it Prob}_{{\mathcal{C}}_{p,q}^{G}}\left(k+1\models\Diamond
0\right)$. Hence, Lemma 0.D.1 immediately implies the result. For the
induction step, we consider two sub-cases. If $k=0$ then ${\it
Prob}_{{\mathcal{C}}_{p,q}^{G}}\left(k\models\Diamond^{\\!\\!\geq
n}0\right)=0$, and the result holds trivially. In the second case, we assume
that $k>0$.

$\begin{array}[]{lll}&{\it
Prob}_{{\mathcal{C}}_{p,q}^{G}}\left(k\models\Diamond^{\\!\\!\geq
n+1}0\right)&\\\ &=q\cdot{\it
Prob}_{{\mathcal{C}}_{p,q}^{G}}\left(k-1\models\Diamond^{\\!\\!\geq
n}0\right)+p\cdot{\it
Prob}_{{\mathcal{C}}_{p,q}^{G}}\left(k+1\models\Diamond^{\\!\\!\geq
n}0\right)&\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Definition
of ${\mathcal{C}}^{G}$}\right\\}}\\\ &\leq q\cdot{\it
Prob}_{{\mathcal{C}}_{p,q}^{G}}\left(k\models\Diamond^{\\!\\!\geq
n}0\right)+p\cdot{\it
Prob}_{{\mathcal{C}}_{p,q}^{G}}\left(k+2\models\Diamond^{\\!\\!\geq
n}0\right)&\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Induction
Hypothesis}\right\\}}\\\ &={\it
Prob}_{{\mathcal{C}}_{p,q}^{G}}\left(k+1\models\Diamond^{\\!\\!\geq
n+1}0\right)&\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Definition
of ${\mathcal{C}}^{G}$}\right\\}}\end{array}$

###### Corollary 1

$p\leq q$ and $k_{1}\leq k_{2}$ imply ${\it
Prob}_{{\mathcal{C}}_{p,q}^{G}}\left(k_{1}\models\Diamond^{\\!\\!\geq
n}0\right)\leq{\it
Prob}_{{\mathcal{C}}_{p,q}^{G}}\left(k_{2}\models\Diamond^{\\!\\!\geq
n}0\right)$.

The following lemma is an instantiation of equation (4.14), page 352, in [14].
It gives an upper bound on the probability of avoiding the sink in the $n^{\it
th}$ step, starting from position $1$.

###### Lemma 0.D.3

${\it
Prob}_{{\mathcal{C}}_{p,q}^{G}}\left(1\models\Diamond^{\\!\\!=n}0\right)=\frac{1}{n}\cdot\left(\begin{array}[]{c}n\\\
\frac{n+1}{2}\end{array}\right)\cdot p^{\frac{n-1}{2}}\cdot
q^{\frac{n+1}{2}}$, if $n$ is odd, and ${\it
Prob}_{{\mathcal{C}}^{G}}\left(1\models\Diamond^{\\!\\!=n}\right)=0$, if $n$
is even.

We use Lemma 0.D.3 to give an upper bound on the probability of avoiding the
sink in the next $n$ steps, starting from position $1$.

###### Lemma 0.D.4

${\it Prob}_{{\mathcal{C}}_{p,q}^{G}}\left(1\models\Diamond^{\\!\\!\geq
n}0\right)\leq\frac{3\cdot q}{\sqrt{\pi}}\cdot(4\cdot p\cdot
q)^{\left\lfloor\frac{n}{2}\right\rfloor}$, for all $n\geq 2$, $p$, and $q$.

###### Proof

$\begin{array}[]{l}{\it
Prob}_{{\mathcal{C}}_{p,q}^{G}}\left(1\models\Diamond^{\\!\\!\geq
n}0\right)\\\ =\frac{1}{n}\cdot\left(\begin{array}[]{c}n\\\
\frac{n+1}{2}\end{array}\right)\cdot p^{\frac{n-1}{2}}\cdot
q^{\frac{n+1}{2}}\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Lemma~{}\ref{Fuller:lemma}}\right\\}}\\\
=\sum_{m=\left\lfloor\frac{n}{2}\right\rfloor}^{\infty}\frac{1}{2\cdot
m+1}\cdot\left(\begin{array}[]{c}2\cdot m+1\\\ m+1\end{array}\right)\cdot
p^{m}\cdot
q^{m+1}\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{$n\geq
2$}\right\\}}\\\
=\sum_{m=\left\lfloor\frac{n}{2}\right\rfloor}^{\infty}\frac{1}{m+1}\cdot\left(\begin{array}[]{c}2\cdot
m\\\ m\end{array}\right)\cdot p^{m}\cdot
q^{m+1}\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Algebra}\right\\}}\\\
\leq\sum_{m=\left\lfloor\frac{n}{2}\right\rfloor}^{\infty}\frac{1}{m+1}\cdot\frac{1}{\sqrt{\pi\cdot
m}}\cdot 2^{2\cdot m}\cdot p^{m}\cdot
q^{m+1}\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{\cite[cite]{[\@@bibref{}{Binomial:2001}{}{}]}}\right\\}}\\\
\leq\frac{q}{\sqrt{\pi}}\cdot\sum_{m=\left\lfloor\frac{n}{2}\right\rfloor}^{\infty}\frac{1}{m\cdot\sqrt{m}}\cdot(4\cdot
p\cdot
q)^{m}\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Algebra}\right\\}}\\\
\leq\frac{q}{\sqrt{\pi}}\cdot\left(\frac{1}{\left\lfloor\frac{n}{2}\right\rfloor\cdot\sqrt{\left\lfloor\frac{n}{2}\right\rfloor}}\cdot(4pq)^{\left\lfloor\frac{n}{2}\right\rfloor}+\int_{\left\lfloor\frac{n}{2}\right\rfloor}^{\infty}\frac{1}{m\cdot\sqrt{m}}\cdot(4pq)^{m}\,dm\right)\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Approximating
$\sum$ by $\int$}\right\\}}\\\
\leq\frac{q}{\sqrt{\pi}}\cdot\left(\frac{1}{\left\lfloor\frac{n}{2}\right\rfloor\cdot\sqrt{\left\lfloor\frac{n}{2}\right\rfloor}}\cdot(4pq)^{\left\lfloor\frac{n}{2}\right\rfloor}+2\cdot\left\lfloor\frac{n}{2}\right\rfloor^{-\frac{1}{2}}\cdot(4pq)^{\left\lfloor\frac{n}{2}\right\rfloor}\right)\\\
\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Overapprox,
since
$\int\frac{e^{-x}}{x\sqrt{x}}dx=-2\frac{e^{-x}}{x\sqrt{x}}-2\int\frac{e^{-x}}{\sqrt{x}}dx$}\right\\}}\\\
\leq\frac{3\cdot q}{\sqrt{\pi}}\cdot(4\cdot p\cdot
q)^{\left\lfloor\frac{n}{2}\right\rfloor}\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{$n\geq
2$}\right\\}}\end{array}$

###  0.D.2 Gravity

In this sub-section, we give the details of Lemma 8.

We define

$q_{\mathcal{P}}\,:=\,\min_{\gamma\in\Gamma_{{\mathcal{P}}}^{=5}}\sum_{\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}^{\leq
4}}{\tt M}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)$

In other words, it is the smallest probability by which a configuration of
size $5$ will decrease its buffer size in the next transition step, and thus
moves to a small configurations.

In Lemma 0.D.5, we first show that $q_{\mathcal{P}}$ is always (independent of
the program ${\mathcal{P}}$) bounded from below $\hat{q}=2/3$. We will then
use this bound $\hat{q}$ in our further development.

###### Lemma 0.D.5

For all programs ${\mathcal{P}}$, $q_{\mathcal{P}}\geq\hat{q}$.

###### Proof

The transition from $\gamma\in\Gamma_{{\mathcal{P}}}^{=5}$ is composed of two
parts, the $\xrightarrow{}_{{\tt proc}}$ and $\xrightarrow{}_{{\tt update}}$
transitions. The $\xrightarrow{}_{{\tt proc}}$ transition can lead to a
configuration $\gamma^{\prime}$ of size either 5 (when the process does not
take a write transition) or 6 (when the process does take a write transition).
Then $\xrightarrow{}_{{\tt update}}$ transition essentially pushes writes from
the buffer such that all possible update words are given equal weight. We
treat the cases with configuration size 5, 6 separately.

##### $|\gamma^{\prime}|=5$

We consider all possible distributions of buffer sizes across the processes.
Depending upon the number of processes, ($|{\sf Procs}|$), we have different
cases. We only need to consider atmost 5 processes since beyind this, the
remaining proceses must have empty buffers. The possible distributions are as
follows (since order is immaterial, we represent distribution as a set):
$\\{1,1,1,1,1\\},\\{2,1,1,1,0\\},\\{2,2,1,0,0\\},\\{3,1,1,0,0\\},\\{3,2,0,0,0\\},\\{4,1,0,0,0\\},\\{5,0,0,0,0\\}$.

For each of these distributions, the number of non-empty update words is
clearly greater than the number of empty update words (a singleton set,
$\epsilon$), i.e. 1. Since we choose uniformly across all update words, we
choose the non-empty word with probability greater than 0.5 and hence reach a
configuration in $\Gamma_{{\mathcal{P}}}^{\leq 4}$ w.p. greater than 0.5.

##### $|\gamma^{\prime}|=6$

Now it suffices to consider 6 processes. The possible distributions of the
buffer sizes across these are as follows (since order is immaterial, we
represent distribution as a set):
$\\{1,1,1,1,1,1\\},\\{2,1,1,1,1,0\\},\\{2,2,1,1,0,0\\},\\{2,2,2,0,0,0\\},\\{3,1,1,1,0,0\\},\\{3,2,1,0,0,0\\}$,
$\\{3,3,0,0,0,0\\},\\{4,1,1,0,0,0\\},\\{4,2,0,0,0,0\\},\\{5,1,0,0,0,0\\},\\{6,0,0,0,0,0\\}$.

Once again the number of update words of length less or equal to 1 for each of
these distributions are 7, 6, 5, 4, 5, 4, 3, 4, 3, 3, 2 respectively. This is
clearly less than half the total number of update words of each configuration.
On choosing an update word of length greater than one, we reach a
configuration in $\Gamma_{{\mathcal{P}}}^{\leq 4}$. Since we choose uniformly
amongst these words, and since words longer than 1 outnumber those less or
equal to 1, we reach a configuration in $\Gamma_{{\mathcal{P}}}^{\leq 4}$ w.p.
greater than 0.5.

Since we show this without making any assumption on the intermediate
configuration $\gamma^{\prime}$ (except for the size), we can conclude that
$q_{\mathcal{P}}>0.5$. On enumerating the exact update word counts for each of
the above cases, we verify that $\hat{q}=\frac{2}{3}$ satisfies the needed
constraints.

Henceforth, we will continue to use the symbol $\hat{q}$, instead of the
concrete value, to make the terms in the presentation clearer to understand.
However, we highlight that we the concrete value of $\frac{2}{3}$ that can be
substituted in place of $\hat{q}$. The next lemma states that probability of
decreasing the size of the buffer is at least $\hat{q}$ for all configuration
of size at least $4$.

###### Lemma 0.D.6

For any $\gamma\in\Gamma_{{\mathcal{P}}}^{\geq 5}$, we have
$\sum_{\gamma^{\prime}\in\Gamma^{<|\gamma|}}{\tt
M}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)\geq\hat{q}$.

###### Proof

By a similar reasoning as the earlier, we see that starting from the
configuration $\gamma$, following the $\xrightarrow{}_{{\tt proc}}$
transition, the intermediate configuration $\gamma^{\prime}$ has size
$\gamma^{\prime}\in\\{|\gamma|,|\gamma|+1\\}$. We can consider the update
words for both possibilities.

##### $|\gamma^{\prime}|=|\gamma|$

For this the only the empty update word leads to a configuration in
$\Gamma_{{\mathcal{P}}}^{=|\gamma|}$. On the other hand, the total number of
update words is atleast greater than the configuration size (atleast one
possible update word for each number of single updates). Hence we have that
the probability to reach $\Gamma_{{\mathcal{P}}}^{<|\gamma|}$ from
$\gamma^{\prime}$ is $>\frac{|\gamma|}{|\gamma|+1}\geq\frac{5}{6}$ (since
$|\gamma|\geq 5$). This gives us the following for all
$\gamma\in\Gamma_{{\mathcal{P}}}^{\geq 5}$.

$\sum_{\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}^{<|\gamma|}}{\tt M}_{\tt
update}\left(\gamma,\gamma^{\prime}\right)>\underbrace{2/3}_{\hat{q}}$

##### $|\gamma^{\prime}|=|\gamma|+1$

Let the distribution of buffer contents across processes be
$\\{b_{0},b_{1},\cdots\\}$. Then the number of update words of length
$|\gamma^{\prime}|=\sum b_{i}$ is given by the multinomial coefficient
${|\gamma^{\prime}|\choose{b_{0},b_{1},\cdots}}$. For this case update words
of length 0 or 1 lead to a configuration not in
$\Gamma_{{\mathcal{P}}}^{<|\gamma|}$. The number of these words is
$1+\sum_{i}\textbf{1}_{b_{i}\neq 0}$, where 1 is the indicator function. It is
clear that the multinomial coefficient is greater than the this expression by
atleast a factor of 2 for $|\gamma^{\prime}|\geq 5$. This follows from the
fact that under the constraints $\sum_{i}b_{i}=|\gamma^{\prime}|$ and
$\sum_{i}\textbf{1}_{b_{i}\neq 0}=c$ for some fixed $c$, the largest value of
$\prod_{i}b_{i}!$ (and hence the smallest value of the multinomial
coefficient) is given by the distribution
$\\{b_{i}\\}=\\{|\gamma^{\prime}|-c+1,\underbrace{1,\cdots,1}_{c-1\text{
times}},0,0,\cdots\\}$

Hence the probability that the length of the update word is atmost 1 is less
than $\frac{1}{3}$, and we have the following.

$\displaystyle\sum_{\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}^{<|\gamma|-1}}{\tt
M}_{\tt update}\left(\gamma,\gamma^{\prime}\right)>\underbrace{2/3}_{\hat{q}}$

Since we showed the above two inequalities for all configurations, this holds
for any possible $\xrightarrow{}_{{\tt proc}}$ transition and hence we have
the result as desired.

We define specific Gambler’s Ruin’s Markov chain, induced by the program
${\mathcal{P}}$, namely
${\mathcal{C}}_{{\mathcal{P}}}^{G}:={\mathcal{C}}_{\hat{p},\hat{q}}^{G}$. From
Lemma 0.D.1 and Lemma 0.D.5 we get the following lemma.

###### Lemma 0.D.7

${\it Prob}_{{\mathcal{C}}_{{\mathcal{P}}}^{G}}\left(k\models\Diamond
0\right)=1$, for all $k\in\mathbb{N}$ and $\ell\geq 5$.

We consider the probability of reaching the set $\Gamma^{\tt
small}_{{\mathcal{P}}}$ of small configurations. To that end, we define the
function

${y}\\!:{\mathbb{N}\times\mathbb{N}}\rightarrow{\mathbb{R}}\;\;\mbox{where}\;\;y\left(k,n\right)\,:=\,\max_{\gamma\in\Gamma_{{\mathcal{P}}}^{=k}}{\it
Prob}_{{\mathcal{P}}}\left(\gamma\models\Diamond^{\\!\\!\geq n}{\Gamma^{\tt
small}_{{\mathcal{P}}}}\right)$

In other words, it is the maximum of the probability measures by which runs
from configurations of size $k$ can avoid small configurations in the next $n$
steps. The following lemma relates this probability with the corresponding
probability in the Gambler Ruin’s problem. Essentially, the lemma abstracts
the set of configurations of $\llbracket{{\mathcal{P}}}\rrbracket^{\tt MC}$ to
the configurations in ${\mathcal{C}}_{{\mathcal{P}}}^{G}$ as given by the
following $level$ function, which was first introduced in 0.A:
$level(\gamma)=0\quad\text{ if }\quad\gamma\in\Gamma^{\leq
4}_{{\mathcal{P}}}$, and $level(\gamma)=|\gamma|$ otherwise.

The following lemma follows directly from the fact that the size of the
configuration will never increase by more than one in PTSO (which is the case
when a write $\xrightarrow{}_{{\tt proc}}$ transition is taken, and no element
of any buffer is pushed to the memory).

###### Lemma 0.D.8

$\sum_{\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}^{\leq
n+1}}{\texttt{M}}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)=1$, for
all $\gamma\in\Gamma_{{\mathcal{P}}}^{n}$ for all $n$.

###### Lemma 0.D.9

$y\left(k+4,n\right)\leq{\it
Prob}_{{\mathcal{C}}_{{\mathcal{P}}}^{G}}\left(k\models\Diamond^{\\!\\!\geq
n}0\right)$, for all $k,n\in\mathbb{N}$.

###### Proof

We use induction on $n$. In the base case, we have $n=0$. By Lemma 0.D.1 and
Lemma 0.D.5 it follows that ${\it
Prob}_{{\mathcal{C}}_{{\mathcal{P}}}^{G}}\left(k\models\Diamond^{\\!\\!\geq
n}0\right)=1$, and the result follows immediately.

For the induction step we consider two cases, namely when $k=1$ and when
$k\geq 1$. If $k=1$ then $y\left(k+4,n+1\right)=0$ and the results follows
immediately. If $k\geq 2$, we fix $\gamma\in\Gamma_{{\mathcal{P}}}^{=k+4}$,
where $k\geq 1$, such that $y\left(k+3,n+1\right)={\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}\Diamond^{\\!\\!\geq
n+1}\Gamma^{\tt small}_{{\mathcal{P}}}\right)$. Such a configuration exists by
the definition of $y$.

$\begin{array}[]{ll}y\left(k+4,n+1\right)&\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{=}\;\left\\{\mbox{Definition
of $\gamma$}\right\\}}\\\ &{\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}\Diamond^{\\!\\!\geq
n+1}\Gamma^{\tt small}_{{\mathcal{P}}}\right)\\\
&\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{=}\;\left\\{\mbox{Lemma~{}\ref{fattractor:prob:one:ptso:lemma}}\right\\}}\\\
&\sum_{j=0}^{k+3}\sum_{\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}^{=j}}{\tt
M}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)\cdot{\it
Prob}_{{\mathcal{P}}}\left(\gamma^{\prime}\models_{{\mathcal{P}}}\Diamond^{\\!\\!\geq
n}\Gamma^{\tt small}_{{\mathcal{P}}}\right)\\\
&\quad+\sum_{\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}^{=k+4}}{\tt
M}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)\cdot{\it
Prob}_{{\mathcal{P}}}\left(\gamma^{\prime}\models_{{\mathcal{P}}}\Diamond^{\\!\\!\geq
n}\Gamma^{\tt small}_{{\mathcal{P}}}\right)\\\
&\quad+\sum_{\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}^{=k+5}}{\tt
M}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)\cdot{\it
Prob}_{{\mathcal{P}}}\left(\gamma^{\prime}\models_{{\mathcal{P}}}\Diamond^{\\!\\!\geq
n}\Gamma^{\tt small}_{{\mathcal{P}}}\right)\\\
&\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{\leq}\;\left\\{\mbox{Definition
of $y$}\right\\}}\\\
&\sum_{j=0}^{k+3}\sum_{\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}^{=j}}{\tt
M}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)\cdot
y\left(j,n\right)\\\
&\quad+\sum_{\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}^{=k+4}}{\tt
M}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)\cdot
y\left(k+4,n\right)\\\
&\quad+\sum_{\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}^{=k+5}}{\tt
M}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)\cdot
y\left(k+5,n\right)\\\
&\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{=}\;\left\\{\mbox{Algebra}\right\\}}\\\
&\sum_{j=0}^{k+3}y\left(j,n\right)\cdot\left(\sum_{\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}^{=j}}{\tt
M}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)\right)\\\
&\quad+y\left(k+4,n\right)\cdot\left(\sum_{\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}^{=k+4}}{\tt
M}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)\right)\\\
&\quad+y\left(k+5,n\right)\cdot\left(\sum_{\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}^{=k+5}}{\tt
M}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)\right)\\\
&\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{\leq}\;\left\\{\mbox{Induction
Hypothesis}\right\\}}\\\ &\sum_{j=0}^{k+3}{\it
Prob}_{{\mathcal{C}}_{{\mathcal{P}}}^{G}}\left(j-4\models\Diamond^{\\!\\!\geq
n}0\right)\cdot\left(\sum_{\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}^{=j}}{\tt
M}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)\right)\\\ &\quad+{\it
Prob}_{{\mathcal{C}}_{{\mathcal{P}}}^{G}}\left(k\models\Diamond^{\\!\\!\geq
n}0\right)\cdot\left(\sum_{\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}^{=k+4}}{\tt
M}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)\right)\\\ &\quad+{\it
Prob}_{{\mathcal{C}}_{{\mathcal{P}}}^{G}}\left({k+1}\models\Diamond^{\\!\\!\geq
n}0\right)\cdot\left(\sum_{\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}^{=k+5}}{\tt
M}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)\right)\\\
&\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{\leq}\;\left\\{\mbox{Corollary~{}\ref{gambler:ruin:close:corollary}}\right\\}}\\\
&{\it
Prob}_{{\mathcal{C}}_{{\mathcal{P}}}^{G}}\left(k-1\models\Diamond^{\\!\\!\geq
n}0\right)\cdot\left(\sum_{j=0}^{k+3}\sum_{\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}^{=j}}{\tt
M}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)\right)\\\ &\quad+{\it
Prob}_{{\mathcal{C}}_{{\mathcal{P}}}^{G}}\left(k+1\models\Diamond^{\\!\\!\geq
n}0\right)\cdot\left(\sum_{\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}^{=k+4}}{\tt
M}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)\right)\\\ &\quad+{\it
Prob}_{{\mathcal{C}}_{{\mathcal{P}}}^{G}}\left({k+1}\models\Diamond^{\\!\\!\geq
n}0\right)\cdot\left(\sum_{\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}^{=k+5}}{\tt
M}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)\right)\\\
&\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{=}\;\left\\{\mbox{Lemma~{}\ref{fattractor:prob:one:ptso:lemma}}\right\\}}\\\
&{\it
Prob}_{{\mathcal{C}}_{{\mathcal{P}}}^{G}}\left(k-1\models\Diamond^{\\!\\!\geq
n}0\right)\cdot\left(\sum_{\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}^{\leq
k+3}}{\tt M}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)\right)\\\
&\quad+{\it
Prob}_{{\mathcal{C}}_{{\mathcal{P}}}^{G}}\left(k+1\models\Diamond^{\\!\\!\geq
n}0\right)\cdot\left(1-\sum_{\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}^{\leq
k+3}}{\tt M}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)\right)\\\
&\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{\leq}\;\left\\{\mbox{
Lemma~{}\ref{threshold:prob:ptso:lemma} and
Lemma~{}\ref{larger:than:threshold:prob:ptso:lemma}}\right\\}}\\\
&\hat{q}\cdot{\it
Prob}_{{\mathcal{C}}_{{\mathcal{P}}}^{G}}\left(k-1\models\Diamond^{\\!\\!\geq
n}0\right)+\hat{p}\cdot{\it
Prob}_{{\mathcal{C}}_{{\mathcal{P}}}^{G}}\left(k+1\models\Diamond^{\\!\\!\geq
n}0\right)\\\
&\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{=}\;\left\\{\mbox{Definition
of ${\mathcal{C}}_{{\mathcal{P}}}^{G}$}\right\\}}\\\ &{\it
Prob}_{{\mathcal{C}}_{{\mathcal{P}}}^{G}}\left(k\models\Diamond^{\\!\\!\geq
n+1}0\right)\end{array}$

From Lemma 0.D.9 and Lemma 0.D.4 we get the following lemma.

###### Lemma 0.D.10

$y\left(k+4,n\right)\leq\frac{3\cdot\hat{q}}{\sqrt{\pi}}\cdot(4\cdot\hat{p}\cdot\hat{q})^{\left\lfloor\frac{n}{2}\right\rfloor}$,
for all $n\geq 2$.

Now we have the ingredients to formally prove Lemma 8. See 8

###### Proof

If $n=0$ then ${\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}\bigcirc\Diamond^{\\!\\!\geq
0}\Gamma^{\tt small}_{{\mathcal{P}}}\right)\leq
1\leq\left({\mathcal{G}}_{{\mathcal{P}}}\right)^{0}$

If $n=1$ then, by Lemma 0.D.10, we have

$\begin{array}[]{ll}{\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}\bigcirc\Diamond^{\\!\\!\geq
0}\Gamma^{\tt small}_{{\mathcal{P}}}\right)&\\\
\leq\hat{p}&\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Definition
of $\hat{p}$}\right\\}}\\\
\leq\sqrt{4\cdot\hat{p}\cdot\hat{q}}&\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Since
$\hat{q}>\hat{p}$}\right\\}}\\\ \leq{\mathcal{G}}_{{\mathcal{P}}}&\end{array}$

If $n\geq 2$.

$\begin{array}[]{ll}{\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}\bigcirc\Diamond^{\\!\\!\geq
n}\Gamma^{\tt small}_{{\mathcal{P}}}\right)&\\\ \leq\hat{p}\cdot
y\left(4,n+1\right)&\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Definition
of $y$ and $\hat{p}$}\right\\}}\\\ \leq\hat{p}\cdot{\it
Prob}_{{\mathcal{C}}_{{\mathcal{P}}}^{G}}\left(1\models\Diamond^{\\!\\!\geq
n+1}0\right)&\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Algebra
and $4\cdot\hat{p}\cdot\hat{q}<1$}\right\\}}\\\
\leq\frac{3\cdot\hat{q}\cdot\hat{p}}{\sqrt{\pi}}\cdot(4\cdot\hat{p}\cdot\hat{q})^{\frac{n}{2}}&\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Lemma~{}\ref{ptso:gambler:ruin:lemma}}\right\\}}\\\
\leq(4\cdot\hat{p}\cdot\hat{q})^{\frac{n}{2}}&\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{$3<\pi$
and $\hat{p}\cdot\hat{q}<1$}\right\\}}\\\
\leq({\mathcal{G}}_{{\mathcal{P}}})^{n}&\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Definition
of ${\mathcal{G}}_{{\mathcal{P}}}$}\right\\}}\end{array}$

###  0.D.3 S-Runs and F-Runs

We first define the predicate ${\tt Visit}$ formally. For a natural number
$1\leq m\leq n$, let $n\oplus m\subseteq{\left(\mathbb{N}^{>0}\right)}^{m}$ be
the set of words $w=i_{1},\ldots,i_{m}$ of length $m$, over the set of
positive natural numbers, such that $i_{1}+\cdots+i_{m}=n$. Notice that

$\left|{n\oplus m}\right|=\left(\begin{array}[]{c}n-1\\\
m-1\end{array}\right)$

We define $n^{\oplus}:=\cup_{1\leq m\leq n}n\oplus m$. For $w\in n^{\oplus}$,
we define ${\tt Visit}_{{\mathcal{P}}}\left(n,w\right)$ to be the set of runs
of the form
$\gamma_{0}\boldsymbol{\cdot}\pi_{0}\boldsymbol{\cdot}\gamma_{1}\boldsymbol{\cdot}\cdots\boldsymbol{\cdot}\gamma_{m}\boldsymbol{\cdot}\pi_{m}\boldsymbol{\cdot}\rho^{\prime}$,
such that the following conditions are satisfied

  * $\triangleright$

$m=\left|{w}\right|$.

  * $\triangleright$

$\forall i:0\leq i\leq m:w[i]=\left|{\pi_{i}}\right|+1$.

  * $\triangleright$

$\forall i:0\leq i\leq m:\gamma_{i}\in\Gamma^{\tt small}_{{\mathcal{P}}}$.

  * $\triangleright$

$\forall i:0\leq i\leq m:\forall j:1\leq
j\leq\left|{\pi_{i}}\right|:\pi_{i}[j]\not\in\Gamma^{\tt
small}_{{\mathcal{P}}}$.

We define ${\tt Visit}_{{\mathcal{P}}}\left(n,m\right):=\cup_{w\in(n\oplus
m)}{\tt Visit}_{{\mathcal{P}}}\left(n,w\right)$. Intuitively, ${\tt
Visit}_{{\mathcal{P}}}\left(n,m\right)$ is the set of runs whose prefixes of
length $n$ visit the set of small configurations exactly $m$ times.

###### Lemma 0.D.11

For every $m,n:1\leq m\leq n$, $w\in\left(n\oplus m\right)$, and
$\gamma\in\Gamma^{\tt small}_{{\mathcal{P}}}$, we have ${\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}{\tt
Visit}_{{\mathcal{P}}}\left(n,w\right)\right)\leq\left({\mathcal{G}}_{{\mathcal{P}}}\right)^{n-m}$

###### Proof

We use induction on $m$.

The base case corresponds to $m=1$, i.e. $w\in(n\oplus 1)$.

$\begin{array}[]{rl}{\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}{\tt
Visit}_{{\mathcal{P}}}\left(n,w\right)\right)&={\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}\bigcirc\Diamond^{\\!\\!\geq
n-1}\Gamma^{\tt
small}_{{\mathcal{P}}}\right)\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Definition
of ${\tt Visit}$}\right\\}}\\\
&\leq\left({\mathcal{G}}_{{\mathcal{P}}}\right)^{n-1}\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Lemma~{}\ref{gravity:lemma}}\right\\}}\end{array}$

Let
$w=\gamma_{0}\boldsymbol{\cdot}\pi_{0}\boldsymbol{\cdot}\gamma_{1}\boldsymbol{\cdot}\cdots\boldsymbol{\cdot}\gamma_{m}\boldsymbol{\cdot}\pi_{m}\boldsymbol{\cdot}\rho^{\prime}$.
Define
$v:=\gamma_{1}\boldsymbol{\cdot}\cdots\boldsymbol{\cdot}\gamma_{m}\boldsymbol{\cdot}\pi_{m}\boldsymbol{\cdot}\rho^{\prime}$.
We know that

$\begin{array}[]{l}{\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}{\tt
Visit}_{{\mathcal{P}}}\left(n,w\right)\right)\\\
=\sum_{\gamma^{\prime}\in\Gamma^{\tt small}_{{\mathcal{P}}}}{\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}\bigcirc\left(\Diamond^{\\!\\!=\left|{\pi_{0}}\right|}\gamma^{\prime}\right)\right)\cdot{\it
Prob}_{{\mathcal{P}}}\left(\gamma^{\prime}\models_{{\mathcal{P}}}{\tt
Visit}_{{\mathcal{P}}}\left(n-\left|{\pi_{0}}\right|-1,v\right)\right)\\\
\qquad\qquad\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Definition
of ${\tt Visit}$}\right\\}}\\\ \leq\sum_{\gamma^{\prime}\in\Gamma^{\tt
small}_{{\mathcal{P}}}}{\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}\bigcirc\left(\Diamond^{\\!\\!=\left|{\pi_{0}}\right|}\gamma^{\prime}\right)\right)\cdot\left({\mathcal{G}}_{{\mathcal{P}}}\right)^{n-\left|{\pi_{0}}\right|-1-(m-1)}\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Induction
Hypothesis}\right\\}}\\\
\leq\left({\mathcal{G}}_{{\mathcal{P}}}\right)^{n-\left|{\pi_{0}}\right|-m}\cdot\sum_{\gamma^{\prime}\in\Gamma^{\tt
small}_{{\mathcal{P}}}}{\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}\bigcirc\left(\Diamond^{\\!\\!=\left|{\pi_{0}}\right|}\gamma^{\prime}\right)\right)\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Algebra}\right\\}}\\\
\leq\left({\mathcal{G}}_{{\mathcal{P}}}\right)^{n-\left|{\pi_{0}}\right|-m}\cdot{\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}\bigcirc\left(\Diamond^{\\!\\!=\left|{\pi_{0}}\right|}\Gamma^{\tt
small}_{{\mathcal{P}}}\right)\right)\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Definition
of ${\it Prob}_{{\mathcal{P}}}$}\right\\}}\\\
\leq\left({\mathcal{G}}_{{\mathcal{P}}}\right)^{n-\left|{\pi_{0}}\right|-m}\cdot\left({\mathcal{G}}_{{\mathcal{P}}}\right)^{\left|{\pi_{0}}\right|}\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Lemma~{}\ref{gravity:lemma}}\right\\}}\\\
\leq\left({\mathcal{G}}_{{\mathcal{P}}}\right)^{n-m}\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Algebra}\right\\}}\end{array}$

We now recall and give the proof of Lemma 9. See 9

###### Proof

$\begin{array}[]{l}{\it Prob}_{{\mathcal{P}}}\left({\tt
SRuns}\left(\gamma\right)\left(n\right)\right)\par\\\
=\sum_{m=1}^{\lfloor\frac{n}{\nu}\rfloor}{\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}\Diamond^{\\!\\!=n}\mathsf{l}\land{\tt
Visit}_{{\mathcal{P}}}\left(n,m\right)\right)\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Definition
of s-runs}\right\\}}\\\ \leq\sum_{m=1}^{\lfloor\frac{n}{\nu}\rfloor}{\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}{\tt
Visit}_{{\mathcal{P}}}\left(n,m\right)\right)\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Definition
of ${\it Prob}_{{\mathcal{P}}}$}\right\\}}\\\
=\sum_{m=1}^{\lfloor\frac{n}{\nu}\rfloor}\sum_{w\in n\oplus m}{\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}{\tt
Visit}_{{\mathcal{P}}}\left(n,m\right)\right)\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Definition
of $\oplus$}\right\\}}\\\ =\sum_{m=1}^{\lfloor\frac{n}{\nu}\rfloor}\sum_{w\in
n\oplus
m}{\mathcal{G}}_{{\mathcal{P}}}^{n-m}\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Lemma~{}\ref{visit:measure:lemma}}\right\\}}\\\
\leq\sum_{m=1}^{\lfloor\frac{n}{\nu}\rfloor}\left(\begin{array}[]{c}n-1\\\
m-1\end{array}\right)\cdot{\mathcal{G}}_{{\mathcal{P}}}^{n-m}\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Algebra}\right\\}}\\\
={\mathcal{G}}_{{\mathcal{P}}}^{n}\cdot\left(\sum_{m=1}^{\lfloor\frac{n}{\nu}\rfloor}\left(\begin{array}[]{c}n-1\\\
m-1\end{array}\right)\cdot{\mathcal{G}}_{{\mathcal{P}}}^{-m}\right)\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Algebra}\right\\}}\\\
\leq{\mathcal{G}}_{{\mathcal{P}}}^{n}\cdot\left(\sum_{m=1}^{\lfloor\frac{n}{\nu}\rfloor}\left(\begin{array}[]{c}n\\\
m\end{array}\right)\cdot{\mathcal{G}}_{{\mathcal{P}}}^{-m}\right)\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Algebra}\right\\}}\\\
\leq{\mathcal{G}}_{{\mathcal{P}}}^{n}\cdot\left(\sum_{m=1}^{\lfloor\frac{n}{\nu}\rfloor}\left(\begin{array}[]{c}n\\\
\lfloor\frac{n}{\nu}\rfloor\end{array}\right)\cdot\left(\begin{array}[]{c}\lfloor\frac{n}{\nu}\rfloor\\\
m\end{array}\right)\cdot\frac{\left(n-\left\lfloor\frac{n}{\nu}\right\rfloor\right)!\cdot\left(\left\lfloor\frac{n}{\nu}\right\rfloor-m\right)!}{\left(n-m\right)!}\cdot{\mathcal{G}}_{{\mathcal{P}}}^{-m}\right)\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Algebra}\right\\}}\\\
\leq{\mathcal{G}}_{{\mathcal{P}}}^{n}\cdot\left(\begin{array}[]{c}n\\\
\lfloor\frac{n}{\nu}\rfloor\end{array}\right)\cdot\left(\sum_{m=1}^{\lfloor\frac{n}{\nu}\rfloor}\left(\begin{array}[]{c}\lfloor\frac{n}{\nu}\rfloor\\\
m\end{array}\right)\cdot\frac{\left(n-\left\lfloor\frac{n}{\nu}\right\rfloor\right)!\cdot\left(\left\lfloor\frac{n}{\nu}\right\rfloor-m\right)!}{\left(n-m\right)!}\cdot{\mathcal{G}}_{{\mathcal{P}}}^{-m}\right)\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Algebra}\right\\}}\\\
\leq{\mathcal{G}}_{{\mathcal{P}}}^{n}\cdot\left(\begin{array}[]{c}n\\\
\lfloor\frac{n}{\nu}\rfloor\end{array}\right)\cdot\left(\sum_{m=1}^{\lfloor\frac{n}{\nu}\rfloor}\left(\begin{array}[]{c}\lfloor\frac{n}{\nu}\rfloor\\\
m\end{array}\right)\cdot\left(\prod_{i=1}^{\left\lfloor\frac{n}{\nu}\right\rfloor}\frac{i}{n-\frac{n}{\nu}+i}\right)\cdot{\mathcal{G}}_{{\mathcal{P}}}^{-m}\right)\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Algebra}\right\\}}\\\
\leq{\mathcal{G}}_{{\mathcal{P}}}^{n}\cdot\left(\begin{array}[]{c}n\\\
\lfloor\frac{n}{\nu}\rfloor\end{array}\right)\cdot\left(\sum_{m=1}^{\lfloor\frac{n}{\nu}\rfloor}\left(\begin{array}[]{c}\lfloor\frac{n}{\nu}\rfloor\\\
m\end{array}\right)\cdot\left(\frac{1}{\nu}\right)^{\left\lfloor\frac{n}{\nu}\right\rfloor-m}\cdot{\mathcal{G}}_{{\mathcal{P}}}^{-m}\right)\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Algebra}\right\\}}\\\
\leq{\mathcal{G}}_{{\mathcal{P}}}^{n}\cdot\left(\begin{array}[]{c}n\\\
\lfloor\frac{n}{\nu}\rfloor\end{array}\right)\cdot\left(\frac{1}{\nu}\right)^{\left\lfloor\frac{n}{\nu}\right\rfloor}\cdot\left(\sum_{m=1}^{\lfloor\frac{n}{\nu}\rfloor}\left(\begin{array}[]{c}\lfloor\frac{n}{\nu}\rfloor\\\
m\end{array}\right)\cdot\left(\frac{\nu}{{\mathcal{G}}_{{\mathcal{P}}}}\right)^{m}\right)\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Algebra}\right\\}}\\\
\leq{\mathcal{G}}_{{\mathcal{P}}}^{n}\cdot\left(\begin{array}[]{c}n\\\
\lfloor\frac{n}{\nu}\rfloor\end{array}\right)\cdot\left(\frac{1}{\nu}\right)^{\left\lfloor\frac{n}{\nu}\right\rfloor}\cdot\left(1+\left(\frac{\nu}{{\mathcal{G}}_{{\mathcal{P}}}}\right)^{\lfloor\frac{n}{\nu}\rfloor}\right)\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Algebra:
$\sum_{b=0}^{\infty}\left(\begin{array}[]{c}{\mathcal{G}}\\\
b\end{array}\right)\cdot x^{b}=(1+x)^{\mathcal{G}}$}\right\\}\par}\\\
\leq{\mathcal{G}}_{{\mathcal{P}}}^{n}\cdot\frac{1}{\sqrt{2\cdot\pi}}\cdot\frac{n^{\frac{n+1}{2}}}{\left(n-\lfloor\frac{n}{\nu}\rfloor\right)^{n-\lfloor\frac{n}{\nu}\rfloor+\frac{1}{2}}\cdot\left(\lfloor\frac{n}{\nu}\rfloor\right)^{\lfloor\frac{n}{\nu}\rfloor+\frac{1}{2}}}\cdot\left(1+\left(\frac{\nu}{{\mathcal{G}}_{{\mathcal{P}}}}\right)^{\lfloor\frac{n}{\nu}\rfloor}\right)\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{\cite[cite]{[\@@bibref{}{Binomial:2001}{}{}]}}\right\\}}\\\
\leq{\mathcal{G}}_{{\mathcal{P}}}^{n}\cdot\left(\frac{n}{n-\left\lfloor\frac{n}{\nu}\right\rfloor}\right)^{n}\cdot\left(\frac{n-\left\lfloor\frac{n}{\nu}\right\rfloor}{\left\lfloor\frac{n}{\nu}\right\rfloor}\right)^{\left\lfloor\frac{n}{\nu}\right\rfloor}\cdot\sqrt{\frac{n}{2\cdot\pi\cdot\left(n-\left\lfloor\frac{n}{\nu}\right\rfloor\right)\cdot\left\lfloor\frac{n}{\nu}\right\rfloor}}\cdot\left(\frac{1}{\nu}+\frac{1}{{\mathcal{G}}_{{\mathcal{P}}}}\right)^{\lfloor\frac{n}{\nu}\rfloor}\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Algebra}\right\\}}\\\
\leq{\mathcal{G}}_{{\mathcal{P}}}^{n}\cdot\left(\frac{n}{n-\frac{n}{\nu}}\right)^{n}\cdot\left(\frac{n-\left\lfloor\frac{n}{\nu}\right\rfloor}{\left\lfloor\frac{n}{\nu}\right\rfloor}\right)^{\left\lfloor\frac{n}{\nu}\right\rfloor}\cdot\sqrt{\frac{n}{2\cdot\pi\cdot\left(n-\frac{n}{\nu}\right)\cdot\frac{n}{\nu}}}\cdot\left(\frac{1}{\nu}+\frac{1}{{\mathcal{G}}_{{\mathcal{P}}}}\right)^{\lfloor\frac{n}{\nu}\rfloor}\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Algebra}\right\\}}\\\
\leq{\mathcal{G}}_{{\mathcal{P}}}^{n}\cdot\left(\frac{\nu}{\nu-1}\right)^{n}\cdot\left(\frac{n-\left\lfloor\frac{n}{\nu}\right\rfloor}{\left\lfloor\frac{n}{\nu}\right\rfloor}\right)^{\left\lfloor\frac{n}{\nu}\right\rfloor}\cdot\sqrt{\frac{\nu}{2\cdot\pi\cdot\left(n-\frac{n}{\nu}\right)}}\cdot\left(\frac{1}{\nu}+\frac{1}{{\mathcal{G}}_{{\mathcal{P}}}}\right)^{\lfloor\frac{n}{\nu}\rfloor}\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Algebra}\right\\}}\\\
={\mathcal{G}}_{{\mathcal{P}}}^{n}\cdot\left(\frac{\nu}{\nu-1}\right)^{n}\cdot(2\cdot\nu)^{\lfloor\frac{n}{\nu}\rfloor}\cdot\left(\frac{1}{\nu}+\frac{1}{{\mathcal{G}}_{{\mathcal{P}}}}\right)^{\lfloor\frac{n}{\nu}\rfloor}\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{$4\leq
2\cdot\nu\leq n$}\right\\}}\\\
\leq{\mathcal{G}}_{{\mathcal{P}}}^{n}\cdot\left(\left(\frac{\nu}{\nu-1}\right)(2\cdot\nu)^{\frac{1}{\nu}}\right)^{n}\cdot\left(\frac{1}{\nu}+\frac{1}{{\mathcal{G}}_{{\mathcal{P}}}}\right)^{\lfloor\frac{n}{\nu}\rfloor}\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Algebra}\right\\}}\\\
\leq\left(\left(\frac{\nu}{\nu-1}\right)(2\cdot\nu)^{\frac{1}{\nu}}\cdot\left(\frac{1}{\nu}+\frac{1}{{\mathcal{G}}_{{\mathcal{P}}}}\right)^{\lfloor\frac{1}{\nu}\rfloor}\cdot{\mathcal{G}}_{{\mathcal{P}}}\right)^{n}\;{\color[rgb]{0.6640625,0.359375,0.40625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.359375,0.40625}{}\;\left\\{\mbox{Algebra}\right\\}}\\\
\leq\left({\mathcal{E}}^{\tt