Fair Termination for Parameterized Probabilistic
Concurrent Systems
Ondřej Lengál1 , Anthony W. Lin2 , Rupak Majumdar3 , and Philipp Rümmer4
2

1
FIT, Brno University of Technology, Czech Republic
Department of Computer Science, University of Oxford, UK
3
MPI-SWS Kaiserslautern, Germany
4
Uppsala University, Sweden

Abstract. We consider the problem of automatically verifying that a parameterized family of probabilistic concurrent systems terminates with probability one
for all instances against adversarial schedulers. A parameterized family defines
an infinite-state system: for each number n, the family consists of an instancewith n finite-state processes. In contrast to safety, the parameterized verificationof liveness is currently still considered extremely challenging especially in thepresence of probabilities in the model. One major challenge is to provide a sufficiently powerful symbolic framework. One well-known symbolic framework forthe parameterized verification of non-probabilistic concurrent systems is regularmodel checking. Although the framework was recently extended to probabilistic
systems, incorporating fairness in the framework — often crucial for verifying
termination — has been especially difficult due to the presence of an infinite
number of fairness constraints (one for each process). Our main contribution isa systematic, regularity-preserving, encoding of finitary fairness (a realistic notion of fairness proposed by Alur & Henzinger) in the framework of regular model
checking for probabilistic parameterized systems. Our encoding reduces termination with finitary fairness to verifying parameterized termination without fairness
over probabilistic systems in regular model checking (for which a verification
framework already exists). We show that our algorithm could verify termination
for many interesting examples from distributed algorithms (Herman’s protocol)and evolutionary biology (Moran process, cell cycle switch), which do not holdunder the standard notion of fairness. To the best of our knowledge, our algorithm
is the first fully-automatic method that can prove termination for these examples.

1

Introduction

In parameterized probabilistic concurrent systems, a population of agents, each typically modeled as a finite-state probabilistic program, run concurrently in discrete timeand update their states based on probabilistic transition rules. The interaction is governed by an underlying topology, which determines which agents can interact in one
step, and a scheduler, which picks the specific agents involved in the interaction. Concurrent probabilistic systems arise as models of distributed algorithms [38,29,31,34,25],
where each agent is a processor, the interaction between processors is determined by
a communication topology, and the processor can update its internal state based on
the communication as well as randomization. In each step, the scheduler adversariallychooses a processor to run. Concurrent probabilistic populations also arise in agentbased population models in biology [35], wherein an agent can represent an allele, acell, or a species, and the interaction between agents describes how these entities evolve
over time. For a population of a fixed size, there is a rich theory of probabilistic verification [20,7,1,48] based on finite-state Markov decision processes (MDPs). Verificationquestions for population models, however, ask if a property holds for populations of all
sizes: even if each agent is finite-state, the family of all processes (for each populationsize) is an infinite-state MDP. Indeed, for many simple population models, one can showthat the verification question is undecidable, even for reachability or safety properties in
the non-probabilistic setting [6,11,22]. Consequently, the verification question for populations requires techniques beyond finite-state probabilistic verification, and requires
symbolic techniques to represent potentially infinite sets of states.
One well-known symbolic framework for verifying parameterized non-probabilistic
concurrent systems is regular model checking [3,42,4,13,41,47], where states of a population are modeled using words over a suitable alphabet, sets of states are represented
as regular languages, and the transition relation is defined as a regular transducer. Fromparameterized verification of non-probabilistic processes, it is known that regular languages provide a robust symbolic representation of infinite sets, and automata-theoretic
algorithms provide the basis of checking safety or termination properties.
In this paper, we consider the problem of verifying that a given parameterized family of probabilistic concurrent systems almost surely terminates, i.e., reaches certain
final states with probability 1 from each initial state regardless of the behaviour of theschedulers. Termination is a fundamental property when verifying parameterized probabilistic systems. Since termination typically, however, fails without imposing certain
fairness conditions on the scheduler, it is crucial to be able to incorporate fairness assumptions into a termination analysis. Therefore, although the framework of regularmodel checking has recently been extended for proving termination (without fairness)over parameterized probabilistic concurrent systems [36], it still cannot be used to prove
termination for many interesting parameterized probabilistic concurrent systems.
What notion of fairness should we consider for proving termination for parameterized probabilistic concurrent systems? To answer this question, one would naturally
start by looking at standard notions of fairness in probabilistic model checking [7],which asserts that every process must be chosen infinitely often. However, this notion
seems to be too weak to prove termination for many of our examples, notably Herman’s self-stabilizing protocol [29] in an asynchronous setting, and population models
from biology (e.g. Moran’s process [35]). The standard notion of fairness gives rise toa rather unintuitive and unrealistic strategy for the scheduler, which could delay an enabled process for as long as it desires while still being fair (see [15, Example 8] andthe Herman’s protocol example in Section 3). For this reason, we propose to consider
Alur & Henzinger’s [5] finitary fairness — a stronger notion of fairness that allows thescheduler to delaying executing an enabled process in an infinite run for at most k steps,
for some unknown but fixed bound k ∈ N. Alur & Henzinger argued that this fairness
notion is more realistic in practice, but it is not as restrictive as the notion of k-fairness,
which fixes the bound k a priori. In addition, it should be noted that finitary fairness isstrictly weaker than probabilistic fairness (scheduler chooses processes randomly) for
almost-sure termination over finite MDPs and parameterized probabilistic systems (aninfinite family of finite MDPs). We will show in this paper that there are many interest2

ing examples of parameterized probabilistic concurrent systems for which termination
is satisfied under finitary fairness, but not under the most general notion of fairness.
Contributions. Our main contribution is a systematic, regularity-preserving, encodingof finitary fairness in the framework of regular model checking for parameterized probabilistic concurrent systems. More precisely, our encoding reduces the problem of verifying almost sure termination under finitary fairness to almost sure termination without
fairness in regular model checking, for which a verification framework exists [36].
In general, the difficulty with finding an encoding of fairness is how to deal withan infinite number of fairness requirements (one for each process) in a systematic andregularity-preserving manner. There are known encodings of general notions of fairness
in regular model checking, e.g., by using a token that is passed to the next process (withrespect to some ordering of the processes) when the current process is executed, andensuring that the first process holds the token and passes it to the right infinitely manytimes (e.g. see [4,42]). However, these encodings do not work in in our case for several
reasons. Firstly, they do not take into account the unknown upper bound (from finitaryfairness) within which time a process has to be executed. Adapting these encodings tofinitary fairness would require the use of unbounded counters, which do not preserve
regularity. Secondly, such encodings would yield the problem of verifying an almostsure Rabin property (of the form 23A∧3B in LTL notation, where A and B are regularsets). Although we could reduce this to an almost-sure termination property by meansof product automata construction (i.e. by first converting the formula to deterministic
Rabin automaton), the target set B in the resulting termination property 3B (consistingof configurations in strongly connected components satisfying some properties) is notnecessarily regular.
Instead, we revisit the well-known abstract program transformation in the setting of
non-probabilistic concurrent systems [26] encoding fairness into the program by associating to each process an unbounded counter that acts as an “alarm clock”, which will“set off” if an enabled process has not been chosen by the scheduler for “too long.” This
abstract program transformation has been adapted by Alur & Henzinger [5] in the caseof finitary fairness by additionally incorporating an extra counter n that stores the unknown upper bound and resetting the value of a counter belonging to a chosen process
to the “default value” n. Our contributions are as follows:
1. We show how Alur & Henzinger’s program transformation could be adapted to thesetting of probabilistic parameterized concurrent systems (infinite family of finite
MDPs). This involves constructing a new parameterization of the system (using
the idea of weakly finite systems) and a proof that the transformation preserves
reachability probabilities.
2. We show how the resulting abstract program transformation could be made concretein the setting of regular model checking without using automata models beyond
regular automata.
3. We have implemented this transformation in FAIRY TAIL. Combined with the existing algorithm [36] for verifying almost sure termination (without fairness) inregular model checking, we have successfully verified a number of models obtained from distributed algorithms and biological systems including Herman’s protocol [29], Moran processes in a linear array [40,35], and the cell cycle switch3

model [17] on ring and line topologies. To the best of our knowledge, our algorithm
is the first fully-automatic method that can prove termination for these examples.
Related work. There are few techniques for automatic verification of liveness properties of parameterized probabilistic programs. Almost sure verification of probabilistic
finite-state programs goes back to Pnueli and co-workers [28,45]. Esparza et al. [23]generalize the reasoning to weakly finite programs, and describe a heuristic to guessa terminating pattern by constructing a nondeterministic program from a given probabilistic program and a terminating pattern candidate. This allows them to exploit model
checkers and termination provers for nondeterministic programs. More recently, Lin
and Rümmer [36] consider unconditional termination for parameterized probabilistic
programs. While our work builds on these techniques, our main contribution is the incorporation of fairness in regular model checking of probabilistic programs, which was
not considered before.
Fairness for concurrent probabilistic systems was considered by Vardi [48] and byHart, Sharir, and Pnueli [28], and generalized later [45,21,8]. The focus was, however,on a fixed number of processes. The notion of fairness through explicit scheduling wasdeveloped by Olderog and Apt [43]. More recently, notions of fairness for infinitarycontrol (i.e., where an infinite number of processes can be created) was considered by
Hoenicke, Olderog, and Podelski [44,30].
Martingale techniques have been used to prove termination of sequential, infinitestate, probabilistic programs [18,39,24,19,32]. These results are not comparable to our
results, as they do not consider unbounded families of fairness constraints nor communication topologies.

2

Preliminaries

General notations: For any two given real numbers i ≤ j, we use a standard notation(with an extra subscript) to denote real intervals, e.g., [i, j]R = {k ∈ R : i ≤ k ≤ j} and(i, j]R = {k ∈ R : i < k ≤ j}. We will denote intervals over integers by removing thesubscript, i.e., [i, j] = [i, j]R ∩ Z. Given a set S, we use S ∗ to denote the set of all finite
sequences of elements from S. The set S ∗ always includes the empty sequence, which
we denote by . We use S + to denote the set S ∗ \{}. Given two sets of words S1 , S2 , weuse S1 · S2 to denote the set {v · w : v ∈ S1 , w ∈ S2 } of words formed by concatenatingwords from S1 with words from S2 . Given two relations R1 , R2 ⊆ S × S, we define
their composition as R1 ◦ R2 = {(s1 , s3 ) : ∃s2 ((s1 , s2 ) ∈ R1 ∧ (s2 , s3 ) ∈ R2 )}.
Transition systems: We fix the (countably infinite) set AP of atomic propositions. Let
ACT be a finite set of action symbols. A transition system over ACT is a tuple S =hS; {→a }a∈ACT , `i, where S is a set of configurations, →a ⊆ S × S is a binary relation
over S, and ` : AP → 2S maps atomic propositions to sets
(we omit `S of configurations
if it is not important). We use → to denote the relation a∈ACT →a . The notation →+(resp. →∗ ) is used to denote the transitive (resp. transitive-reflexive) closure of →. We
say that a sequence s1 → · · · → sn is a path (or run) in S (or in →). Given two paths
π1 : s1 →∗ s2 and π2 : s2 →∗ s3 in →, we may concatenate them to obtain π1 π2(by gluing together s2 ). We call π1 a prefix of π1 π2 . For each S 0 ⊆ S, we use the4notations pre → (S 0 ) and post → (S 0 ) to denote the pre/post image of S 0 under →. That is,
pre → (S 0 ) = {p ∈ S : ∃q ∈ S 0 (p → q)} and post → (S 0 ) = {q ∈ S : ∃p ∈ S 0 (p → q)}.
Words and automata: We assume basic familiarity with finite word automata. Fix a finite alphabet Σ. For each finite word w = w1 . . . wn ∈ Σ ∗ , we write w[i, j], where 1 ≤i ≤ j ≤ n, to denote the segment wi . . . wj . Given an automaton A = (Σ, Q, δ, q0 , F ),a run of A on w is a function ρ : {0, . . . , n} → Q with ρ(0) = q0 that obeys thetransition relation δ. We may also denote the run ρ by the word ρ(0) · · · ρ(n) over thealphabet Q. The run ρ is said to be accepting if ρ(n) ∈ F , in which case we say that w
is accepted by A. The language L(A) of A is the set of words in Σ ∗ accepted by A.
Reachability games: We recall some basic concepts on 2-player reachability games(see e.g. [27, Chapter 2] on games with 1-accepting conditions). An arena is a transition
system S = hS = V1 ∪ V2 ; →1 , →2 i, where S (i.e. the set of “game configurations”)
is partitioned into two disjoint sets V1 and V2 such that pre→i (S) ⊆ Vi for each i ∈{1, 2}. The transition relation →i denotes the actions of Player i. Similarly, for eachi ∈ {1, 2}, the configurations Vi are controlled by Player i. In the following, Player 1
will also be called “Scheduler,” and Player 2 “Process”. Given a set I0 ⊆ S of initialconfigurations and a set F ⊆ S of final (a.k.a. target) configurations, the goal of Player 2
is to reach F from I0 , while the goal of Player 1 is to avoid it. More formally, a strategy
for Player i is a partial function f : S ∗ Vi → S such that, for each v ∈ S ∗ and p ∈ Vi ,if vp is a path in S and p is not a dead end (i.e., p →i q for some q), then f (vp) is
defined in such a way that p →i f (vp). Given a strategy fi for Player i ∈ {1, 2} andan initial configuration s0 ∈ S, we can define a unique (finite or infinite) path in S
such that π : s0 →j1 s1 →j2 · · · where sjk+1 = fi (s0 s1 . . . sjk ) for i ∈ {1, 2} is the(unique) configuration s.t. sjk ∈ Vi . Player 2 wins iff some configuration in F appears
in π, or if the path is finite and the last configuration belongs to Player 1. Player 1 wins
iff Player 2 does not win; we say Player 2 loses. A strategy f for Player i is winningfrom I0 if for each strategy g of Player 3 − i, the unique path in S from each s0 ∈ I0
witnesses a win for Player i. Such games (a.k.a. reachability games) are determined(see e.g. [27, Proposition 2.21]): either Player 1 has a winning strategy or Player 2 hasa winning strategy.
Convention. For notational simplicity, w.l.o.g., we make the following assumptions on
our reachability games. They suffice for the purpose of proving liveness for parameterised systems.
(A0) Arenas are strictly alternating, i.e., a move made by a player does not take thegame back to her configuration (post →i (S) ∩ Vi = ∅, for each i ∈ {1, 2}).
(A1) Initial and final configurations belong to Player 1, i.e., I0 , F ⊆ V1
(A2) Non-final configurations are not dead ends: ∀x ∈ S \ F, ∃y : x →1 y ∨ x →2 y.
Markov chains: A (discrete-time) Markov chain (a.k.a. DTMC) is a structure of theform S = hS; δ, `i where S is a set of configurations, δ is a function that associates
a configuration s ∈ S with a probability distribution over a sample space D ⊆ S (i.e.
the probability of going to a certain configuration from s), and ` : AP → 2S maps
atomic propositions to subsets of S. In what follows, we will assume that each δ(s) is
a discrete probability distribution with a finite sample space. This assumption allows us
5to simplify our notation: a DTMC hS; δ, `i can be seen as a transition system hS; →,`i with a transition probability
a transition t = (s, s0 ) ∈ → to a
Pfunction δ mapping0
value δ(t) ∈ (0, 1] such that s0 ∈post(s) δ((s, s )) = 1. That is, transitions with zerop

probabilities are removed from →. We will write s −→ s0 to denote s → s0 and that
δ((s, s0 )) = p. The underlying transition graph of a DTMC hS; δ, `i is the transition
system hS; →, `i with δ omitted. Given a finite path π = s0 → · · · → sn from theinitial configuration s0 ∈ S, let Runπ be the set of all finite/infinite paths with π asa prefix, i.e., of the form π π 0 for some finite/infinite path π 0 . Given a set F ⊆ S
of target configurations, the probability ProbS (s0 |= 3F ) (the subscript S may beomitted when understood) of reaching F from s0 in S can be defined using a standard
cylinder construction (see e.g [33]) as follows. For each finite path π = s0 → · · · → sn
in S from s0 , weQset Runπ to be a basic cylinder, to which we associate the probabilityn−1
Prob(Runπ ) = i=0 δ((si , si+1 )). This gives rise to a unique probability measure forthe σ-algebra over the set of all runs from s0 . The probability Prob(s0 |= 3F ) is thenthe probability of the event F containing all paths in S with some “accepting” finite
path as a prefix, i.e., a finite path from s0 ending in some configuration in F . In general,
given an LTL formula ϕ over AP, the event containing all paths from s0 in S satisfying
ϕ is measurable [48] and its probability value Prob(s0 |= ϕ) is well-defined.
Notation: Whenever understood, we will omit mention of ` from hS; δ, `i.

3Abstract Models of Probabilistic Concurrent Programs

In this section, we recall the notion of Markov Decision Processes (MDPs) and fair
MDPs [7]. These serve as our abstract models of probabilistic concurrent programs.
We then define the notion of finitary fairness [5] and discuss its basic properties in thesetting of MDPs.
3.1

Markov Decision Processes

A Markov decision process (MDP) is a strictly alternating arena S = hS = V1 ∪V2 ; →1 , →2 i such that hS; →2 i is a DTMC, i.e., →2 is associated with some transition
probability function, and that the atomic propositions are not important. Intuitively,
the transition relation →1 is nondeterministic (controlled by a “demonic” scheduler),
whereas the transition relation →2 is probabilistic. By definition of arenas, the configurations of the MDPs are partitioned into the set V1 of nondeterministic states (controlled by Scheduler) and the set V2 of probabilistic states. Formally, pre→1 (S) ∩pre→2 (S) = ∅. Each Scheduler’s strategy5 f : S ∗ V1 → S gives rise to an infinitestate DTMC with the underlying transition system Sf = hS 0 ; →3 , `i and the transition
probability function δ 0 defined as follows. Here, S 0 is the set of all finite/infinite paths πfrom s0 . For each state s0 ∈ S and each path π from s0 ending in some state s ∈ S, we
define π →3 πs0 iff: (1) if s ∈ V1 is a nondeterministic state, then f (π) = s0 , and (2) ifs ∈ V2 is a probabilistic state, then s →2 s0 . Intuitively, Sf is an unfolding of the gamearena S (i.e. a disjoint union of trees) where branching only occurs on probabilistic
states. Transitions π →3 πs0 satisfying Case (1) have the probability δ 0 ((π, πs0 )) = 1;
5

Also called “scheduler” or “adversary” for short.

6otherwise, its probability is δ 0 ((π, πs0 )) = δ((s, s0 )). We let ` be a function mapping
each subset X ⊆ S (used as an atomic proposition) to the set of all finite paths in Sf
from s0 to X. Since Sf is a DTMC, given an LTL formula ϕ over subsets of S as
atomic propositions, the probability ProbSf (s0 |= ϕ) of satisfying ϕ in S from s0 under the scheduler f is well-defined. In particular, ProbSf (s0 |= 3F ) is the probabilityof reaching F from s0 in S under the scheduler f . The probability ProbS,C (s0 |= ϕ)of satisfying ϕ from s0 in the MDP S under a class C of schedulers is defined to be theinfimum of the set of all probabilities ProbSf (s0 |= ϕ) over all f ∈ C. We will omit
mention of C when it denotes the class of all schedulers.
An MDP is weakly-finite [23] if from each configuration, the set of all configurations
that are reachable from it (in the underlying transition system of the MDP) is finite.
Note that the state space of weakly-finite MDPs can be infinite. The restriction of weakfiniteness is another way of defining the notion of parameterized systems, which are
an infinite family of finite-state systems. Weakly-finite MDPs capture many interesting
probabilistic concurrent systems in which each process is finite-state; this is the case formany probabilistic distributed protocols.
3.2

Fair Markov Decision Processes

A fair Markov decision process (FMDP) is a structure of the form S = hS = V1 ∪V2 ; →1 , →2 , C, Ji, where hS = V1 ∪ V2 ; →1 , →2 i is an MDP, J is a weak fairness(a.k.a. justice) requirement, and C is a strong fairness (a.k.a. compassion) requirement.
More precisely, a weak fairness requirement is a set (at most countably infinite) of
atomic weak fairness requirements of the form 32A ⇒ 23B, for some A, B ⊆ S.
Here, the 2 and 3 modalities are the standard “always” and “eventually” LTL operators.
The set A (resp. B) will be called the premise (resp. consequence). Intuitively, if A isinterpreted as “Process 1 is waiting to move” and B as “Process 1 is chosen”, then thisfairness requirement may be read as: at no point can Process 1 be continuously waiting
to move without being chosen. In addition, a strong fairness requirement is a set (again,at most countably infinite) of atomic strong fairness requirements of the form 23A ⇒23B, for some A, B ⊆ S. Using the above example, a strong fairness requirement
reads: if Process 1 is waiting to move infinitely often, then it is chosen infinitely often.
As before, the set A (resp. B) will be called the premise (resp. consequence). In thefollowing, when it is clear whether a fairness requirement is a justice or a compassion,
we will denote it by the pair (A, B) of premise and consequence.
Given an FMDP S = hS = V1 ∪ V2 ; →1 , →2 , C, Ji, a configuration s0 ∈ S, anda scheduler f , since each atomic fairness requirement is an LTL formula and there areat most countably many atomic fairness requirements, the set of paths from s0 in the
DTMC Sf induced by f satisfying C and J is measurable. We say that a scheduler f
is S-fair if ProbSf (s0 |= C ∧ J) = 1 for every initial configuration s0 . The fairness
conditions (C, J) are realizable in S if there exists at least one S-fair scheduler.
A natural fairness notion we consider in this paper is process fairness, which assertsthat each process is chosen infinitely often. For this notion of fairness, we can assume
that the consequence B of each atomic fairness requirement asserts that a particular process is chosen. We make one simplifying assumption: each process is always enabled(i.e., can always be chosen by the scheduler). This assumption is reasonable since we7can always introduce an idle transition for each process. Under this assumption, we
have that from each v1 ∈ V1 , there exists a transition v1 →1 v2 for some v2 ∈ B.
This implies that our fairness conditions are always realizable and that the probability
ProbS,C (E) of event E over the set of all S-fair schedulers is well-defined.
3.3

Finitary Fairness

Given an FMDP S = hS = V1 ∪ V2 ; →1 , →2 , C, Ji, a configuration s0 ∈ S, anda number k ∈ N, we say that a scheduler f is S-k-fair (or k-fair whenever S isunderstood) if for each atomic fairness requirement (A, B):
1. if (A, B) is justice, then (the underlying graph of) Sf contains no path π of lengthk satisfying the LTL formula 2(A ∧ ¬B).
2. if (A, B) is compassion, then Sf contains no path π satisfying the LTL formulaψk ∧ 2¬B, where ψ0 := true and ψi := 3(A ∧ ψi−1 ) for each i > 0.
In other words, a premise in a justice requirement cannot be satisfied for k consecutive
steps without satisfying a consequence, while a premise in a compassion requirement
cannot be satisfied for k (not necessarily consecutive) steps without satisfying a consequence. A scheduler is said to be finitary fair (fin-fair) if it is k-fair for some k. The
fairness conditions (C, J) are said to be finitary-realizable (fin-realizable) in S if there
exists at least one fin-fair scheduler. Under this assumption, the probability ProbS,C (E)of an event E over the set C of all fin-fair schedulers is well-defined. In what follows,
for an FMDP S, we will simply denote ProbS,C (E) as ProbS (E). In this paper, we
propose to study termination of probabilistic concurrent programs under finitary fairness, i.e., to determine whether ProbS,C (s0 |= 3F ) = 1, where C is the class of all
fin-fair schedulers.
The following proposition states one special property of weakly-finite MDPs.
Proposition 1. Let S and S0 be two weakly-finite fair MDPs with identical underlying
transition systems (but possibly different probability values). For each set F of final
states, and each initial configuration s0 , it is the case that ProbS (s0 |= 3F ) = 1 iff
ProbS0 (s0 |= 3F ) = 1.
By Proposition 1, when dealing with almost-sure finitary-fair termination of weaklyfinite MDPs, we only care whether a transition has a zero or a non-zero probability, i.e.,
if it is non-zero, then the exact value is irrelevant. Incidentally, the same also holds forother properties including almost-sure termination without fairness and qualitative temporal specifications [28,45,36]. For this reason, we may simply omit these probability
values from our symbolic representation of weakly-finite MDPs, which we will do fromthe next section onwards.
3.4

Herman’s Protocol

Herman’s protocol [29] is a distributed self-stabilization algorithm for a population ofprocesses organized in a ring. The correct configurations are those where exactly one
process holds a token. If, through some error, the ring enters an erroneous configuration8

(in which multiple processes hold tokens), Herman’s protocol ensures that the system
will self-stabilize: it will almost surely go back to a configuration with only one token.
Let us discuss how the protocol works in more detail. Fix N ≥ 3 processors organized in a ring. If a chosen process does not hold a token, then it can perform an idle
transition (i.e. do nothing). If a chosen process holds a token, then it can keep holding the token with probability 21 or pass it on to its clockwise neighbor (the process(i + 1) mod N , for processes numbered 0, . . . , N − 1) with probability 12 . If a process currently holds a token and receives another token from its (counter-clockwise)neighbor, then the two tokens are merged6 into one, leaving the process with one token.
Formally, Hermann’s protocol can be modeled as a weakly-finite Markov decision
process whose states are vectors in {⊥, >}∗ . For each N , the state of the protocol is
described by a bitvector of N bits, with the i-th bit being one iff the i-th process holds a
token. From a state v, the scheduler picks a process i ∈ {0, . . . , N −1}. Given a chosen
process i, the new state remains v if the chosen process i did not hold a token (v(i) =⊥). If v(i) = >, the new state is v with probability 21 and v ⊕ ei ⊕ e(i+1) mod N withprobability 12 . Here, ei denotes a vector with > in the i-th position and ⊥ everywhere
else, and ⊕ is the XOR operation. We want to ensure that, starting from an arbitrary
initial assignment of tokens, any population self-stabilizes with probability one.
Process fairness for Herman’s protocol is a set of N atomic fairness requirements,
each asserting that the process i is executed infinitely often, for each i ∈ {1, . . . , N }.
Unfortunately, Herman’s protocol does not terminate with probability one against somefair schedulers. To see this, consider the start state s0 = (>, ⊥, >). Let us call the token
held by Process 0 “the first token”, and the token held by Process 2 “the second token”.
Define a round as the following sequence of moves by the scheduler: keep choosing
the process that holds the first token until it passes the token to the right, and do thesame to the same to the second token. For example, the two configurations obtained
after completing the first and second rounds from s0 are, respectively, (>, >, ⊥) and(⊥, >, >). To see that the scheduler is fair, for each integer i > 0, the probability thatthe i-th round is not completed is 0 since the probability that one of the tokens will be
kept at the same process for an infinite amount of time is 0. Therefore, the probability
that some round is not completed is also 0. Completing two rounds ensure that all theprocesses are picked. Therefore, every process will be chosen with probability 1. On
the other hand, observe that correct configurations are not seen in the induced DTMC,
showing that self-stabilization holds with probability 0 under this scheduler.
Herman’s protocol can be shown to self-stabilize with probability one under all
fin-fair schedulers, which can be proved by our fully-automatic verification algorithm(presented later in the paper).

4

Regular Model Checking: A Symbolic Framework

In this section, we recall regular model checking (see e.g. [3,42,46]), a symbolic framework for specifying infinite-state systems based on finite automata and regular transducers and developing automatic verification (semi-)algorithms.
A transition system S = hS = V1 ∪ V2 ; →1 , →2 i is specified in the framework
as a regular language S (e.g. as a regular expression over some alphabet Σ), and two
6

Herman [29] describes a more general protocol in which tokens can be merged/destroyed withsome probability. We consider this restriction for simplicity of presentation.

9

“regular relations” →1 , →2 ⊆ Σ ∗ × Σ ∗ . For simplicity, in the following we will assume
that S = Σ ∗ . How do we specify regular relations? One standard way is to restrict tolength-preserving relations (i.e. the relation may only contain a pair of words of thesame length) and specify such relations as regular languages over the alphabet Σ × Σ.
There is, then, a simple one-to-one correspondence between the set of words over Σ×Σ
and the set of all pairs of words over Σ of the same length. This can be achieved by
mapping a pair (v, w) of words Σ with |v| = |w| = n to a word v ⊗ w, defined as(v1 , w1 )(v2 , w2 ) · · · (vn , wn ) whenever v = v1 · · · vn and w = w1 · · · wn .
Proving that a property ϕ holds over a transition system S is done “in a regularway,”, by finding a “regular proof” for the property. For example, if ϕ asserts that theset Bad of bad states can never be reached, then a regular proof amounts to finding an
inductive invariant Inv in the form of a regular language [3,42] that does not intersectwith Bad , i.e., Bad ∩ Inv = ∅, S0 ⊆ Inv (S0 is a regular set of initial states), andpost→ (Inv ) ⊆ Inv , where → = →1 ∪ →2 . Since regular languages are effectively
closed under boolean operations and taking pre/post images w.r.t. regular transducers,
an algorithm for verifying the correctness of a given regular proof can be obtained byusing language inclusion algorithms for regular automata, e.g., [14,2]. The frameworkof regular proofs is incomplete in general since it could happen that there is a proof,
but no regular proof. The pathological cases when only non-regular proofs exist do not,however, seem to frequently occur in practice, e.g., see [12,16,41,3,47,9,10,42,37].
The framework of regular proofs has been extended to deal with almost-sure termination for weakly-finite probabilistic concurrent programs in [36]. We briefly summarise the main idea, since we reduce the fair termination problem to their setting.
By Proposition 1, the actual probability values do not matter in proving almost-suretermination. For this reason, we may specify a weakly-finite MDP S = hS = V1 ∪V2 ; →1 , →2 i as a regular specification in the same way as we specify a non-probabilistictransition system in our regular specification language. Given an MDP S = hS =V1 ∪ V2 ; →1 , →2 i, a set I0 ⊆ V1 of initial configurations, and a set F ⊆ V1 of final configurations, a regular proof for Prob(s0 |= F ) = 1 for each s0 ∈ I0 is a pairhInv , ≺i consisting of a regular inductive invariant Inv ⊆ S and a regular relation≺ ⊆ S × S such that:
1. I0 ⊆ Inv and post → (Inv ) ⊆ Inv .
2. ≺ is a strict preorder on S, i.e., it is irreflexive (∀s ∈ S : s 6≺ s) and transitive(∀s, s0 , s00 ∈ S : s ≺ s0 ∧ s0 ≺ s00 → s ≺ s00 ).
3. irrespective of the nondeterministic transitions from any configuration in Inv , there
is a probabilistic transition to a configuration in Inv that decreases its rank withrespect to ≺:∀x ∈ Inv \ F, y ∈ S \ F :(x →1 y) ⇒ (∃z ∈ Inv : (y →2 z) ∧ x  z) .
An automata-theoretic algorithm can then be devised for checking the above verification
conditions with respect to a given regular proof [36].
Example 1. [Herman’s protocol, continued] We provide a regular encoding of Herman’s protocol. The configurations are words over the alphabet {>, ⊥, >, ⊥}, where >(resp. ⊥) signifies that a process holds (resp. does not hold) a token, while overlining
10the character signifies that the process is chosen by the scheduler. We set Σ = {>, ⊥}.
The set S0 of initial configurations is Σ ∗ >Σ ∗ , i.e., at least one process holds a token. The set of final configurations is ⊥∗ >⊥∗ , i.e., there is only a single token in thesystem. The actions of the scheduler is to choose a process; this can be expressed as
the regular expression I ∗ ((>, >) + (⊥, ⊥))I ∗ , where I denotes the regular language(>, >)+(⊥, ⊥). The probabilistic actions can be expressed as a union of the following
three regular expressions:I ∗ ((>, >) + (⊥, ⊥))I ∗(idle)

I ∗ (>, ⊥)((⊥, >)) + (>, >))I ∗ , ((⊥, >) + (>, >))I ∗ (>, ⊥)) (pass token right)

5

Handling Fairness Requirements

We now describe the main result of the paper: a general method for embedding finitaryfairness into regular model checking for probabilistic concurrent systems.
5.1

Regular Specifications of Fairness

When a complex system or a distributed protocol is being modelled in regular model
checking, it is often necessary to add an infinite number of fairness requirements. This isbecause such a system admits a finite but arbitrary number of agents or processes, eachwith its own fairness requirement (e.g. that the process should be executed infinitely
often). For this reason, it is not enough to simply express the fairness requirements asa finite set of pairs of regular languages (one for the premise, and one for the consequence). We describe a regular way of specifying infinitely many fairness constraints.
Our presentation is a generalisation of the regular specification of fairness from [4,42].
The general idea is to define a “regular function” T that maps a configurations = s1 · · · sn ∈ S to a word w = w1 · · · wn such that wi contains: (1) a bit bi indicating whether s is in the premise of the i-th fairness requirement, (2) a bit b0i indicating whether s is in the consequence of the i-th fairness requirement, and (3) a bit t
indicating whether the i-th fairness requirement is justice or compassion. Such a regular specification of fairness allows an infinite number of fairness constraints since S ispotentially infinite (i.e., containing words of unbounded lengths), though only the first|s| fairness requirements matter for a word s ∈ S. This is sufficient for weakly-finite
MDPs since the set of reachable configurations from any given configuration s is finite and so, among the infinite number of fairness constraints, only finitely many are
distinguishable. The regular function can be defined by a letter-to-letter tranducer with
input alphabet Σ and output alphabet Γ := {0, 1} × {0, 1} × {0, 1}. Without loss ofgenerality, we assume that the i-th letter in the output of every input word of T agree
on the third bit (i.e., whether the fairness requirement is justice or compassion is welldefined): for every s, s0 ∈ S and i ∈ N, if T (s)[i] = (a, b, c) and T (s0 )[i] = (a0 , b0 , c0 ),then c = c0 . Observe this condition on T can be algorithmically checked by using asimple automata-theoretic method: find two accepted words in which in some position
their third bits differ.
In this case, T gives rise to compassion requirements C and justice requirements J
by associating the i-th position in all output words by a unique fairness constraint.
11More precisely, let Ai = {s : T (s)[i] = (1, j, t), for some j, t ∈ {0, 1}} and Bi ={s : T (s)[i] = (j, 1, t), for some j, t ∈ {0, 1}}. Define: (i) J = {32Ai ⇒ 23Bi :T (s)[i] = (i, j, 0), for some s ∈ S, for some j ∈ {0, 1}}, (ii) C = {23Ai ⇒ 23Bi :T (s)[i] = (i, j, 1), for some s ∈ S, for some j ∈ {0, 1}}. Therefore, by Proposition
1, our regular fairness specification allows us to define weakly-finite fair MDPs hS =V1 ∪ V2 ; →1 , →2 , C, Ji. In the following, we shall call such fair MDPs regular.
Our main theorem is a regularity-preserving reduction from proving almost sure termination for regular FMDPs (under finitary fairness) to proving almost sure termination
for regular MDPs (without fairness).
Theorem 1. Let S = hS = V1 ∪ V2 ; →1 , →2 , C, Ji be a regular representation of
an FMDP, I0 ⊆ V1 be a regular set of initial configurations, and F ⊆ V1 be a regular
set of final configurations. Then one can compute a regular presentation of MDP S0 =hS = V10 ∪ V20 ; ;1 , ;2 i and two regular sets I00 , F 0 ⊆ V10 such that it holds that if C
and J are realizable, then ProbS0 (I00 |= 3F 0 ) = 1 iff ProbS (I0 |= 3F ) = 1.
5.2

Abstract Program Transformation

Before proving Theorem 1, let us first recall an abstract program transformation à la
Alur & Henzinger [5], which encodes finitary fairness into a program using integer
counter variables. Intuitively, we reserve one variable for each atomic fairness condition
as an “alarm clock” that will set off if its corresponding process has not been executedfor a long time, and one global variable n that acts as a default value to reset a clock to
as soon as the corresponding process is executed. Although Alur & Henzinger [5] did
not discuss about probabilistic programs, their transformation can be easily adapted tothe setting of MDPs, though correctness still has to be proven.
We now elaborate on the details of the transformation. Given an FMDP S = hS =V1 ∪V2 ; →1 , →2 , C, Ji with a probability distribution δ, the transformation will produce
an MDP S0 = hS = V10 ∪ V20 ; ;1 , ;2 i with a probability distribution δ 0 as follows.
Introduce a set V of “counter” variables that range over natural numbers: xj (for eachj ∈ J), yc (for each c ∈ C), and n. Let F be the set of all valuations f mapping eachvariable in V to a natural number such that f (xj ), f (yc ) ≤ f (n) for each j ∈ J andc ∈ C. We define V10 = V1 × F and V20 = V2 × F. We now define the transition relation;i such that (s, f ) ;i (s0 , f 0 ) if s →i s0 and– for each z ∈ V, f (z) > 0,
– f 0 (n) := f (n),– xj (for j = (A, B) ∈ J) and yc (for c = (A, B) ∈ C) change as follows:
if s ∈ A ∩ B
 f (n)f (xj ) − 1 if s ∈ A ∩ B
f 0 (yc ) = f (yc ) − 1 if s ∈ A ∩ B
f 0 (xj ) =f (n)if s ∈ A ∪ B
f (n)if s ∈ B(A denotes the set-complement of A). Finally, we define the probability distribution δ 0
underlying ;2 as δ 0 ((s, f ), (s0 , f 0 )) = δ(s, s0 ) whenever s ∈ V2 .
Lemma 1. If S is a weakly-finite FMDP, then S0 is weakly-finite.
12

Intuitively, the variables xj ’s and yc ’s keep track of how long the scheduler hasdelayed choosing an enabled process, while the variable n (unchanged once the initialconfiguration of the MDP is fixed) aims to ensure that the scheduler is n-fair. Since n
is a variable (not a constant), the resulting MDP S0 captures precisely the behaviour of
S under fin-fair schedulers.
We next state a correctness lemma for the transformation (proof in the full version).
To this end, given a set S0 ⊆ S of initial configurations in S, we define:– S00 := S0 × F= , where F= contains functions f ∈ F such that f (xj ) = f (yc ) =f (n) for each j ∈ J and c ∈ C.
– F 0 = (F × F>0 ) ∪ (S × F0 ), where F0 contains all f ∈ F such that f (xj ) = 0 forsome j ∈ J or f (yc ) = 0 for some c ∈ C (i.e. one of the alarms has been triggered),and F>0 := F \ F0 .
Lemma 2 (Correctness). For weakly-finite fair MDPs S, it is the case that
ProbS (S0 |= 3F ) = ProbS0 (S00 |= 3F 0 ).
These two lemmas immediately imply Theorem 1.
5.3

Finitary Fairness in Regular Model Checking

We now show how to implement the aforementioned abstract program transformationin our regular model checking framework. Fix a regular presentation of an FMDPS = hS = V1 ∪ V2 ; →1 , →2 , C, Ji, which includes two automata over the alphabet Σ × Σ representing →1 and →2 , and an automaton over the alphabet Σ × Γ
representing the regular specification of the fairness conditions C and J. [Recall that
Γ := {0, 1} × {0, 1} × {0, 1}.] We describe the construction of ;1 (the construction
for ;2 is similar). Let A = (Σ ×Σ, Q, ∆, q0 , F ) be an automaton representing →1 and
Af = (Σ × Γ, Qf , ∆f , q0f , F f ) be an automaton representing the regular specificationof fairness. The construction of the automaton for ;1 has two stages.
Stage 1: compute an intermediate automaton. The intermediate automaton B will havethe alphabet Σ 0 := (Σ × Σ) ∪ Γ and recognize a subset of ((Σ × Σ)Γ )∗ . Intuitively, on
input (a, b) ∈ Σ × Σ, the automaton B simultaneously runs both A and Af . Here, theautomaton Af will nondeterministically guess a letter c ∈ Γ and make a transition on
the letter (a, c). The automaton B, then, immediately consumes the letter c. This process
is repeated until both A and Af accept. More precisely, the automaton is defined as
B := (Σ 0 , QB , ∆B , q0B , F B ) where:– QB = Q × Qf × (Γ ∪ {?}), q0B = (q0 , q0f , ?), and F B = F × F f × {?}– ∆B has the following transitions:• ((p1 , q1f , ?), (a, b), (p2 , q2f , c)) if (p1 , (a, b), p2 ) ∈ ∆ and (q1f , (a, c), q2f ) ∈ ∆f .
• ((p, q f , c), c, (p, q f , ?)) for each c ∈ Γ .
Stage 2: regular substitution of letters in Γ . Define the following regular languages– (Identity) ID := (1, 1)+ (?, ?)∗ ,– (Decrement) DEC := (1, 1)∗ (1, ?)(?, ?)∗ , and– (Reset) RES := (1, 1)+ (?, 1)∗ .
13

Define the regular substitution σ mapping letters in Γ to regular languages:– if (x, y, z) is (i, 1, j) or (0, i, 0) (for i, j ∈ {0, 1}), then σ((x, y, z)) = RES.
– if (x, y, z) is of the form (1, 0, i) (for some i ∈ {0, 1}), then σ((x, y, z)) = DEC.
– define σ((0, 0, 1)) = ID.
We then apply the regular substitution σ to the letters Γ appearing in our intermediate
automaton B. The resulting automaton implements the desired automaton for ;1 .
Finishing off the rest of the construction. Computing S00 , F 0 is easy. Define S00 to be
the set of all words a1 w1 a2 w2 · · · am wm — where ai ∈ Σ and wi ∈ 1+ for each i ∈{1, . . . , m} — such that a1 · · · am ∈ S0 . Similarly, define F 0 to be the set of all words
a1 w1 a2 w2 · · · am wm — where ai ∈ Σ and wi ∈ 1+ ?∗ ∪ ?+ for each i ∈ {1, . . . , m}
— such that a1 · · · am ∈ F or wi ∈ ?+ for some i ∈ {1, . . . , m}. Regular automata forthese sets could be easily constructed given automata for S0 and F .
Example 2. [Herman’s protocol] We encode process fairness in the following way.
The counters use the unary encoding, their values represented as the lengths of sequences of 1’s padded on the right by the symbol ? (crucial to keep the transducers
length-preserving). For example, the number 3 is represented by any word of the form
111?∗ . Define X = 1∗ ?∗ , i.e., the set of all valid counters. The set of initial configurations can be expressed using the regular expression (Σ · X )∗ (> · X )(Σ · X )∗ , i.e.,counters for all processes are initialized to an arbitrary value. The set of final configurations is now (⊥ · X )∗ (> · X )(⊥ · X )∗ ∪ (Σ · X )∗ (Σ· ?∗ )(Σ · X )∗ , i.e., either thereis exactly one token in the system, or (at least) one counter has reached 0. Scheduler
now also performs operations on the counters for processes: for a chosen process, thecounter is reset, for other processes, the counter is decremented.
This can be expressed
as the language (I · DEC)∗ ((⊥, ⊥) + (>, >)) · RES (I · DEC)∗ . Actions of the protocol
are the same as in the original encoding and the values of counters are left unmodified:(I · ID)∗ ((⊥, ⊥) + (>, >)) · ID (I · ID)∗ (idle)(I · ID)∗ (>, ⊥) · ID ((⊥, >) + (>, >)) · ID (I · ID)∗ (pass token right1 )((⊥, >) + (>, >)) · ID (I · ID)∗ (>, ⊥) · ID
(pass token right2 )At this point, we can use existing tools for checking termination (without fairness constraints), e.g. [36]. Indeed, we can automatically check that the system after reduction
terminates with probability one, thus proving that Herman’s protocol fairly terminateswith probability one (under finitary process-fair schedulers).

6

Implementation and Experiments

The approach presented in this paper has been implemented in the tool FAIRY TAIL.7
For evaluation, we extracted models of a number of probabilistic parameterized systems. The tool receives a system with fairness conditions and transforms it into a system without fairness conditions, where fairness of the original system is encoded using
counters. For solving liveness in the output transformed system, we use S LRP [36] (inthe incremental liveness proofs setting) as the underlying liveness checker for parameterized systems.
7

https://github.com/uuverifiers/autosat/tree/master/Fairness

14

Table 6 shows the results of our exper- Table 1. Times of analyses of probabilistic
iments. The times given are the wall clock paremeterised systems. The timeout wastimes for the individual benchmarks on a PC set to 10 hours (timeout is denoted as T/O).
with 4 Quad-Core AMD Opteron 8389 pro- Case study
Time
cessors with Java heap memory limited to Herman’s protocol (merge, line)
3.64 s64 GiB. The time included translation of the Herman’s protocol (annih., line)
4.33 ssystem into a system without fairness (always Herman’s protocol (merge, ring)
4.31 sHerman’s protocol (annih., ring)
4.61 sless than 1s) and the runtime of S LRP.
2 m 48 s
We consider two versions of Herman’s Moran process (2 types, line)
56 m 14 s
protocol and two topologies. Moran process, Moran process (3 types, line)
43.94 sis a model of genetic drift [40] with individ- Cell cycle switch (1 types, line)
Cell
cycle
switch(2
types,line)
9h 46 muals of N ≥ 2 types. When an individual
Clustering(2
types,line)
10
m 30 sis chosen by the scheduler, it can either idle
Clustering (3 types, line)
T/O
or infect a neighbor. The model of cell cycle
Coin game (k = 3, clique)1m 0s
switch is a simplification of the model of [17].
Individuals can be committed to a decision from N ≥ 1 types. An individual neighboring another one not sharing the same decision can make him undecided, or persuade
an undecided individual to commit to his decision. Clustering considers a population
model of alleles of N ≥ 2 (resp. 3) types on a line, that can change position with theirneighbours of a different type. Coin game is a population protocol where every agent
has one of two types of coins. If an agent is chosen by the scheduler, it can change its
coin to the one held by the majority of k other randomly selected agents.
In our experiments, we verify that a given property holds under every finitary processfair scheduler with probability one. For clustering, the property is that the system eventually reaches a configuration with N clusters of the same type, while for the otherpopulation protocols, the property is that the system reaches a stable configuration.
The experiments show that our encoding of fairness into systems is viable and canbe used for verification of parameterized systems with fairness by their reduction to systems without fairness. On the other hand, when the size of the regular proof is large, we
observe that the problem for the underlying solver gets significantly more difficult (ascan be seen on the example of clustering for three types of alleles). We conjecture thatthe performance can be improved significantly by making the solver take into accountthe (not arbitrary) structure of the problem, which we leave for future work.
Future work. We leave the reader with several research challenges. A natural question is how to deal with non-finitary fairness for parameterized probabilistic concurrent
systems in general and in the framework of regular model checking. Secondly, since
there are numerous examples of population models over more complex topologies (e.g.
grids), how do you deal with termination and fair termination over such models in theparameterized setting?
Acknowledgement. We thank anonymous reviewers and Dave Parker for their helpful
feedback. This work was supported by the Czech Science Foundation (project 1624707Y), the BUT FIT project FIT-S-17-4014, the IT4IXS: IT4Innovations Excellencein Science project (LQ1602), Yale-NUS Starting Grant, the European Research Council
under ERC Grant Agreement no. 610150, and Swedish Research Council (2014-5484).

15

References
1. PRISM
website(referredinJuly2015).
http://http://www.
prismmodelchecker.org/.
2. P. A. Abdulla, Y.-F. Chen, L. Holı́k, R. Mayr, and T. Vojnar. When simulation meets antichains. In TACAS, pages 158–174, 2010.
3. Parosh Aziz Abdulla. Regular model checking. STTT, 14(2):109–118, 2012.
4. Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, Julien d’Orso, and Mayank Saksena.
Regular model checking for LTL(MSO). STTT, 14(2):223–241, 2012.
5. Rajeev Alur and Thomas A. Henzinger. Finitary fairness. ACM Trans. Program. Lang. Syst.,
20(6):1171–1194, 1998.
6. Krzysztof R. Apt and Dexter Kozen. Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett., 22(6):307–309, 1986.
7. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008.
8. Christel Baier and Marta Z. Kwiatkowska. On the verification of qualitative properties ofprobabilistic processes under fairness constraints. Inf. Process. Lett., 66(2):71–79, 1998.
9. S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. FAST: acceleration from theory to practice.
STTT, 10(5):401–424, 2008.
10. S. Bardin, A. Finkel, J. Leroux, and Ph. Schnoebelen. Flat acceleration in symbolic model
checking. In ATVA, pages 474–488, 2005.
11. Nathalie Bertrand and Paulin Fournier. Parameterized verification of many identical probabilistic timed processes. In FSTTCS’13, volume 24 of LIPIcs, pages 501–513. Schloss
Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013.
12. B. Boigelot and F. Herbreteau. The power of hybrid acceleration. In CAV, pages 438–451,
2006.
13. B. Boigelot, A. Legay, and P. Wolper. Iterating transducers in the large (extended abstract).
In CAV, pages 223–235, 2003.
14. Filippo Bonchi and Damien Pous. Checking NFA equivalence with bisimulations up tocongruence. In POPL’13, pages 457–468. ACM, 2013.
15. Rémi Bonnet, Stefan Kiefer, and Anthony Widjaja Lin. Analysis of probabilistic basic parallel processes. In FOSSACS, pages 43–57, 2014.
16. Ahmed Bouajjani, Peter Habermehl, Adam Rogalewicz, and Tomás Vojnar. Abstract regular(tree) model checking. STTT, 14(2):167–191, 2012.
17. Luca Cardelli and Attila Csikász-Nagy. The cell cycle switch computes approximate majority. Scientific Reports, 2(656), 2012.
18. Aleksandar Chakarov and Sriram Sankaranarayanan. Probabilistic program analysis withmartingales. In CAV, pages 511–526, 2013.
19. Aleksandar Chakarov, Yuen-Lam Voronin, and Sriram Sankaranarayanan. Deductive proofsof almost sure persistence and recurrence properties. In TACAS, pages 260–279, 2016.
20. C. Courcoubetis and M. Yannakakis. Minimum and maximum delay problems in real-timesystems. Formal Methods in System Design, 1(4):385–415, 1992.
21. Luca de Alfaro. Temporal logics for the specification of performance and reliability. In
STACS 97, Symposium on Theoretical Aspects of Computer Science, volume 1200 of Lecture
Notes in Computer Science, pages 165–176. Springer, 1997.
22. Javier Esparza. Parameterized verification of crowds of anonymous processes. Dependable
Software Systems Engineering, 45:59–71, 2016.
23. Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Proving termination of probabilistic programs using patterns. In CAV, pages 123–138, 2012.
24. Luis Marı́a Ferrer Fioriti and Holger Hermanns. Probabilistic termination: Soundness, completeness, and compositionality. In POPL’15, pages 489–501. ACM, 2015.

16

25. Wan Fokkink. Distributed Algorithms. MIT Press, 2013.
26. Nissim Francez. Fairness. Springer-Verlag New York, Inc., New York, NY, USA, 1986.
27. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite
Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001],
volume 2500 of Lecture Notes in Computer Science. Springer, 2002.
28. Sergiu Hart, Micha Sharir, and Amir Pnueli. Termination of probabilistic concurrent program. ACM Trans. Program. Lang. Syst., 5(3):356–380, 1983.
29. Ted Herman. Probabilistic self-stabilization. Inf. Process. Lett., 35(2):63–67, 1990.
30. Jochen Hoenicke, Ernst-Rüdiger Olderog, and Andreas Podelski. Fairness for dynamic control. In TACAS’10, volume 6015 of LNCS, pages 251–265. Springer, 2010.
31. Amos Israeli and Marc Jalfon. Token management schemes and random walks yield selfstabilizing mutual exclusion. In PODC, pages 119–131, 1990.
32. Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo.
Weakest precondition reasoning for expected run-times of probabilistic programs. In
ESOP’16, volume 9632 of LNCS, pages 364–389. Springer, 2016.
33. Marta Z. Kwiatkowska. Model checking for probability and time: from theory to practice.
In LICS, page 351, 2003.
34. D. Lehmann and M. Rabin. On the advantage of free choice: A symmetric and fully distributed solution to the dining philosophers problem (extended abstract). In POPL, pages
133–138, 1981.
35. E Lieberman, C Hauert, and M A Nowak. Evolutionary dynamics on graphs. Nature,433(7023):312–316, January 2005.
36. Anthony W. Lin and Philipp Rümmer. Liveness of randomised parameterised systems underarbitrary schedulers. In CAV’16 (2), volume 9779 of LNCS, pages 112–133. Springer, 2016.
37. Anthony Widjaja Lin. Accelerating tree-automatic relations. In FSTTCS, pages 313–324,
2012.
38. Nancy A. Lynch, Isaac Saias, and Roberto Segala. Proving time bounds for randomized
distributed algorithms. In PODC, pages 314–323, 1994.
39. David Monniaux. An abstract analysis of the probabilistic termination of programs. In SAS,pages 111–126. Springer, 2001.
40. Patrick A.P. Moran. Random processes in genetics. Mathematical Proceedings of the Cambridge Philosophical Society, 54(1):60–71, Jan 1958.
41. Daniel Neider and Nils Jansen. Regular model checking using solver technologies and automata learning. In NFM, pages 16–31, 2013.
42. M. Nilsson. Regular Model Checking. PhD thesis, Uppsala Universitet, 2005.
43. Ernst-Rüdiger Olderog and Krzysztof R. Apt. Fairness in parallel programs: The transformational approach. ACM Trans. Program. Lang. Syst., 10(3):420–455, 1988.
44. Ernst-Rüdiger Olderog and Andreas Podelski. Explicit fair scheduling for dynamic control. In Concurrency, Compositionality, and Correctness, Essays in Honor of Willem-Paul deRoever, volume 5930 of Lecture Notes in Computer Science, pages 96–117. Springer, 2010.
45. Amir Pnueli and Lenore D. Zuck. Verification of multiprocess probabilistic protocols. Distributed Computing, 1(1):53–72, 1986.
46. A. W. To. Model Checking Infinite-State Systems: Generic and Specific Approaches. PhD
thesis, LFCS, School of Informatics, University of Edinburgh, 2010.
47. Anthony Widjaja To and Leonid Libkin. Algorithmic metatheorems for decidable LTL model
checking over infinite systems. In FoSSaCS, pages 221–236, 2010.
48. Moshe Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In
FOCS, pages 327–338, 1985.

17