Probabilistic Bisimulation for Parameterized Systems(with applications to verifying anonymous protocols)?
Chih-Duo Hong1 , Anthony W. Lin2 , Rupak Majumdar3 , and Philipp Rümmer2
1

Oxford University, United Kingdom
2
TU Kaiserslautern, Germany
3
Uppsala University, Sweden
4
Max Planck Institute for Software Systems, Germany

Abstract. Probabilistic bisimulation is a fundamental notion of process equivalence for probabilistic systems. It has important applications, including the formalisation of the anonymity property of several communication protocols. While
there is a large body of work on verifying probabilistic bisimulation for finite
systems, the problem is in general undecidable for parameterized systems, i.e.,
for infinite families of finite systems with an arbitrary number n of processes.
In this paper we provide a general framework for reasoning about probabilistic
bisimulation for parameterized systems. Our approach is in the spirit of software
verification, wherein we encode proof rules for probabilistic bisimulation and use
a decidable first-order theory to specify systems and candidate bisimulation relations, which can then be checked automatically against the proof rules.
We work in the framework of regular model checking, and specify an infinitestate system as a regular relation described by a first-order formula over a universal automatic structure, i.e., a logical theory over the string domain. For probabilistic systems, we show how probability values (as well as the required operations) can be encoded naturally in the logic. Our main result is that one canspecify the verification condition of whether a given regular binary relation is a
probabilistic bisimulation as a regular relation. Since the first-order theory of theuniversal automatic structure is decidable, we obtain an effective method for verifying probabilistic bisimulation for infinite-state systems, given a regular relation
as a candidate proof. As a case study, we show that our framework is sufficiently
expressive for proving the anonymity property of the parameterized dining cryptographers protocol and the parameterized grades protocol. Both of these protocols hitherto could not be verified by existing automatic methods. Moreover,with the help of standard automata learning algorithms, we show that the candidate relations can be synthesized fully automatically, making the verification
fully automated.

1

Introduction

Equivalence checking using bisimulation relations plays a fundamental role in formal
verification. Bisimulation is the basis for substitutability of systems: if two systems?

This research was sponsored in part by the ERC Starting Grant 759969 (AV-SMP), ERC Synergy project 610150 (ImPACT), the DFG project 389792660-TRR 248 (Perspicuous Computing), the Swedish Research Council (VR) under grant 2018-04727, and by the Swedish
Foundation for Strategic Research (SSF) under the project WebSec (Ref. RIT17-0011).

are bisimilar, their behaviors are the same and they satisfy the same formulas in expressive temporal logics. The notion of bisimulation is defined both for deterministic[39] and for probabilistic transition systems [34]. In both contexts, checking bisimulation has many applications, such as proving correctness of anonymous communication
protocols [15], reasoning about knowledge [22], program optimization [32], and optimizations for computational problems (e.g. language equivalence and minimization) offinite automata [12].
The problem of checking bisimilarity of two given systems has been widely studied.
It is decidable in polynomial-time for both probabilistic and non-probabilistic finitestate systems [6, 17, 20, 52]. These algorithms form the basis of practical tools forchecking bisimulation. For infinite-state systems, such as parameterized versions ofcommunication protocols (i.e. infinite families of finite-state systems with an arbitrary
number n of processes), the problem is undecidable in general. Most research hitherto
has focused on identifying decidable subcases (e.g. strong bisimulations for pushdown
systems for probabilistic and non-probabilistic cases [25, 47, 48]), rather than on providing tool support for practical problems.
In this paper, we propose a first-order verification approach—inspired by software
verification techniques—for reasoning about bisimilarity for infinite-state systems. In
our approach, we provide first-order logic proof rules to determine if a given binary
relation is a bisimulation. To this end, we must find an encoding of systems and relations and a decidable first-order theory that can formalize the system, the property,
and the proof rules. We propose to use the decidable first-order theory of the universal automatic structure [8, 10]. Informally, the domain of the theory is a set of words
over a finite alphabet Σ, and it captures the first-order theory of the infinite |Σ|-ary treewith a relation that relates strings of the same level. The theory can express precisely
the class of all regular relations [8] (a.k.a. automatic relations [10]), which are relations ϕ(x1 , . . . , xk ) over strings Σ ∗ that can be recognized by synchronous multi-tapeautomata. It is also sufficiently powerful to capture many classes of non-probabilistic
infinite-state systems and regular model checking [3, 13, 49–51].
We demonstrate the effectiveness of the approach by encoding and automaticallyverifying some challenging examples from the literature of parameterized systems in
our logic: the anonymity property of the parameterized dining cryptographers protocol [16] and the grades protocol [29]. These examples were only automatically verified
for some fixed parameters using finite-state model checkers or equivalence checkers(e.g. see [28, 29]). Just as invariant verification for software separates out the proof
rules (verification conditions in a decidable logic) from the synthesis of invariants, we
separate out proof rules for bisimulation from the synthesis of bisimulation relations.
We demonstrate how recent developments in generating and refining candidate proofs
as automata (e.g. [18, 26, 27, 37, 38, 40, 41, 53]) can be used to automate the search of
proofs, making our verification fully “push button.”
Contributions. Our contributions are as follows. First, we show how probabilistic
infinite-state systems can be faithfully encoded in the first-order theory of universal
automatic structure. In the past, the theory has been used to reason about qualitative
liveness of weakly-finite MDPs (e.g. see [36, 37]), which allows the authors to disregard the actual non-zero probability values. To the best of our knowledge, no encoding

of probabilistic transition systems in the theory was available. In order to be able toeffectively encode probabilistic systems, our theory should typically be two-sorted: one
sort for encoding the configurations, and the other for encoding the probability values.
We show how both sorts (and the operations required for the sorts) can be encodedin the universal automatic structure, which requires only the domain of strings. In thesequel, such transition systems will be called regular transition systems.
Second, using the minimal probability assumption on the transition systems [34](i.e. there exists an ε > 0 such that any non-zero transition probability is at least ε)—which is often satisfied in practice—we show how the verification condition of whether
a given regular binary relation is a probabilistic bisimulation can be encoded in thetheory. The decidability of the first-order theory over the universal automatic structure
gives us an effective means of checking probabilistic bisimulation for regular transition
systems. In fact, the theory can be easily reduced to the weak monadic theory WS1S of
one successor (therefore, allowing highly optimized tools like Mona [31] and Gaston[23]) by interpreting finite words as finite sets (e.g. see [19, 46]).
Our framework requires the encoding of the systems and the proofs in the first-ordertheory of the universal automatic structure. Which interesting examples can it capture?
Our third contribution is to provide two examples from the literature of parameterizedverification: the anonymity property of the parameterized dining cryptographers protocol [16] and of the parameterized grades protocol [29]. We study two versions of dining
cryptographers protocol in this paper: the classical version where the secrets are single
bits, and a generalized version where the secrets are bit-vectors of arbitrary length.
Thus far, our framework requires a candidate proof to be supplied by the user. Our
final contribution is to demonstrate how standard techniques from the synthesis literature (e.g. automata learning [18, 26, 27, 37, 38, 40, 41, 53]) can be used to fully automate
the proof search. Using automata learning, we successfully pinpoint regular proofs forthe anonymity property of the three protocols: the two dining cryptographers protocols
are verified in 6 and 28 seconds, respectively, and the grades protocol in 35 seconds.
Other related work. The verification framework we use in this paper can be construed
as a regular model checking [3] framework using regular relations. The framework uses
first-order logic as the language, which makes it convenient to express many verification
conditions (as is well-known from first-order theorem proving [14]). The use of the universal automatic structure allows us to express two different sorts (configurations andprobability values) in one sort (i.e. strings). Most work in regular model checking focuses on safety and liveness properties (e.g. [2, 3, 11, 13, 27, 36, 37, 40, 42, 49, 51, 53]).
Some automated techniques can prove the anonymity property of the dining cryptographers protocol and the grades protocol in the finite case, e.g., the PRISM model
checker [28, 45] and language equivalence by the tool APEX [29]. To the best of ourknowledge, our method is the first automated technique proving the anonymity propertyof the protocols in the parameterized case.
Our work is in spirit of deductive software verification (e.g., [4, 14, 24, 35, 43, 44]),
where one provides inductive invariants manually, and a tool automatically checks correctness of the candidate invariants. In theory, our result yields a fully-automatic procedure by enumerating all candidate regular proofs, and at the same time enumerating all
candidate counterexamples (note that we avoid undecidability by restricting attention toproofs encodeable as regular relations). In our implementation, we use recent advancesin automata-learning based synthesis to efficiently encode the search [18, 37].

2Preliminaries

General notation. We use N to denote non-negative integers. Given a, b ∈ R, we use
a standard notation [a, b] := {c ∈ R : a ≤ c ≤ b} to denote real intervals. Givena 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 P
denote by ε. We call a function
f : S → [0, 1] a probability distribution over S if s∈S f (s) = 1. We shall use
Is to denote the probability distribution f with f (s) = 1, and DS to denote the setof probability distributions over S. Given a function f : X1 × · · · × Xn → Y , thegraph of f is the relation {(x1 , ..., xn , f (x1 , ..., xn )) : ∀i ∈ {1, . . . , n}. xi ∈ Xi }.
Whenever a relation R is an equivalence relation over set S, we use S/R to denote theset of equivalence classes created by R. Depending on the context, we may use p R q orR(p, q) to denote (p, q) ∈ R.
Words and automata. We assume basic familiarity with 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 the transition
relation δ. We may also denote the run ρ by the word ρ(0) · · · ρ(n) over the alphabet Q.
The run ρ is said to be accepting if ρ(n) ∈ F , in which case we say that the word w is
accepted by A. The language L(A) of A is the set of words in Σ ∗ accepted by A.
Transition systems. We fix a set ACT of action symbols. A transition system over ACT
is a tuple S := hS; {→a }a∈ACT i, where S is a set of configurations
and →a ⊆ S × S
S
is a binary relation over S. We use → to denote the relation a∈ACT →a . We say thata sequence s1 → · · · → sn+1 is a path in S if s1 , ..., sn+1 ∈ S and si → si+1
for i ∈ {1, . . . , n}. A transition system is called bounded branching if the number ofconfigurations reachable from a configuration in one step is bounded. Formally, thismeans that there exists an a priori integer N such that for all s ∈ S, |{s0 ∈ S : s →s0 }| ≤ N .
Probabilistic transition systems. A probabilistic transition system (PTS) [34] is a
structure S := hS; {δa }a∈ACT i where S is a set of configurations and δa : S →DS ∪ {0} maps each configuration to either a probability distribution or a zero function 0. Here δa (s) = 0 simply means that s is a “dead end” for action a. We shall use
δa (s, s0 ) to denote δa (s)(s0 ). In this paper, we always assume that δa (s, s0 ) is a rational
number and |{s0 : δa (s, s0 ) 6= 0}| < ∞. The underlying transition graph of a PTS is atransition system hS; {→a }a∈ACT i such that s →a s0 iff δa (s, s0 ) 6= 0.
It is standard (e.g. see [34]) to impose the minimal probability assumption on the
PTS that we shall be dealing with, i.e., there is  > 0 such that any transition with a
non-zero probability p satisfies p > . This assumption is practically sensible since it
is satisfied by most PTSs that we deal with in practice (e.g. finite PTS, probabilistic
pushdown automata [21], and most examples from probabilistic parameterized systems[36, 37] including our examples from Section 5). The minimal probability assumption,

among others, implies that the PTS is bounded-branching (i.e. that its underlying transition graph is bounded-branching). In the sequel, we shall adopt this assumption.
ρProbabilistic
bisimulations. Let S := hS; {δa }a∈ACT i be a PTS. We write s −→a S 0
P0if
s0 ∈S 0 δa (s, s ) = ρ. A probabilistic bisimulation for S is an equivalence relation
R over S, such that (p, q) ∈ R impliesρρ∀a ∈ ACT. ∀S 0 ∈ S/R. (p −→a S 0 ⇔ q −→a S 0 ).

(1)

We say that p and q are probabilistic bisimilar (written as p ∼ q) if there is a probabilistic bisimulation R such that (p, q) ∈ R. We can compute probabilistic bisimulation
between two PTSs S := hS; {δa }a∈ACT i and S0 := hS 0 ; {δa0 }a∈ACT i by computing
a probabilistic bisimulation R for the disjoint union of S and S0 , which is defined as
S t S0 := hS t S 0 ; {δa00 }a∈ACT i where δa00 (s) := δa (s) for s ∈ S, and δa00 (s) := δa0 (s)for s ∈ S 0 . In such case, we say R is a probabilistic bisimulation between S and S0 .

3

Framework of Regular Relations

In this section we describe the framework of regular relations for specifying probabilistic infinite-state systems, properties to verify, and proofs, all in a uniform symbolic
way. The framework is amenable to automata-theoretic algorithms in the spirit of regular model checking [3, 13].
The framework of regular relations [8] (a.k.a. automatic relations [9]) uses the firstorder theory of universal5 automatic structure
U := hΣ ∗ ; , eqL, {la }a∈Σ i,(2)where Σ is some finite alphabet,  is the (non-strict) prefix-of relation, eqL is thebinary equal length predicate, and la is a unary predicate asserting that the last letterof the word is a. The domain of the structure is the set of finite words over Σ, and forwords w, w0 ∈ Σ ∗ , we have w  w0 iff there is some w00 ∈ Σ ∗ such that w · w00 = w0 ,eqL(w, w0 ) iff |w| = |w0 |, and la (w) iff there is some w00 ∈ Σ ∗ such that w = w00 · a.
Next, we discuss the expressive power of first-order formulas over the universal automatic structures, and decision procedures for satisfiability of such formulas. In Section 4, we shall describe: (1) how to specify a PTS as a first-order formula in U , and (2)how to specify the verification condition for probabilistic bisimulation property in thistheory. In Section 5, we shall show that the theory is sufficiently powerful for capturing
probabilistic bisimulations for interesting examples.
Expressiveness and Decidability. The name “regular” associated with this framework
is because the set of formulas ϕ(x1 , . . . , xk ) first-order definable in U coincides withregular relations, i.e., relations definable by synchronous automata. More precisely, we∗ kdefine [[ϕ]] as the relation which contains all tuples (w1 , . . . , wk ) ∈ (Σ⊥) such that
U |= ϕ(w1 , . . . , wk ). In addition, we define the convolution w1 ⊗ · · · ⊗ wk of words
5

Here, “universal” simply means that all automatic structures are first-order interpretable in thisstructure.

kw1 , . . . , wk ∈ Σ ∗ as a word w over Σ⊥(where ⊥ ∈/ Σ) such that w[i] = (a1 , . . . , ak )with
wj [i] if |wj | ≥ i, oraj =⊥otherwise.

In other words, w is obtained by juxtaposing w1 , . . . , wk and padding the shorter words
with ⊥. For example, 010 ⊗ 00 = (0, 0)(1, 0)(0, ⊥). A k-ary relation R over Σ ∗ isregular if the set {w1 ⊗ · · · ⊗ wk : (w1 , . . . , wk ) ∈ R} is a regular language over thekalphabet Σ⊥. The relationship between U and regular relations can be formally statedas follows.
Proposition 1 ([8–10]).
1. Given a formula ϕ(x̄) over U , the relation [[ϕ]] is effectively regular. Conversely,
given a regular relation R, we can compute a formula ϕ(x̄) over U such that[[ϕ]] = R.
2. The first-order theory of U is decidable.
The decidability of the first-order theory of U follows using a standard automatatheoretic algorithm (e.g. see [9, 49]).
In the sequel, we shall also use the term regular relations to denote relations definable in U . In addition, to avoid notational clutter, we shall freely use other regular
relations (e.g. successor relation ≺succ of the prefix , and membership in a regular
language) as syntactic sugar.
We note that the first-order theory of U can also be reduced to weak monadic theory
WS1S of one successor (therefore, allowing highly optimized tools like MONA [31]and Gaston [23]) by translating finite words to finite sets. The relationship between
the universal automatic structure and WS1S can be made precise using the notion offinite-set interpretations [19, 46].

4

Probabilistic Bisimilarity within Regular Relations

In this section, we show how the framework of regular relations can be used to encode
a PTS, and the corresponding proof rules for probabilistic bisimulation.
4.1

Specifying a probabilistic transition system

Since we assume that all probability values specified in our systems are rational numbers, the fact that our PTS is bounded-branching implies that we can specify the probability values by natural weights (by multiplying the probability values by the least
common multiple of the denominators). For example, if a configuration c has an action
toss that takes it to c1 and c2 , each with probability 1/2, then the new system simply
changes both values of 1/2 to 1. This is a known trick in the literature of probabilistic
verification (e.g. see [1]). Therefore, we can now assume that the transition probability
functions have range N. The challenge now is that our encoding of a PTS in the universal automatic structure must encode two different sorts as words over a finite alphabet
Σ: configurations and natural weights.

Now we are ready to show how to specify a PTS S in our framework. Fix a finite
alphabet Σ containing at least two letters 0 and 1. We encode the domain of S as words
over Σ. In addition, a natural weight n ∈ N can be encoded in the usual way as a binary
string. This motivates the following definition.
Definition 1. Let S be a PTS hS; {δa }a∈ACT i. We say that S is regular if the domain
S is a regular subset of Σ ∗ (i.e. definable by a first-order formula ϕ(x) with one freevariable over U ), and if the graph of each function δa is a ternary regular relation (i.e.
definable by a first-order formula ϕ(x, y, z) over U , where x and y encode configurations, and z encodes a natural weight).
Definition 1 is quite general since it allows for an infinite number of different natural weights in the PTS. Note that we can make do without the second sort (of numeric weights) if we have only finitely many numeric weights n1 , . . . , nm . This canbe achieved by specifying a regular relation Ra,i for each action label a ∈ ACT andnumeric weight ni with i ∈ {1, . . . , m}.
Example 1. We show a regular encoding of a very simple PTS: a random walk on theset of natural numbers. At each position x, the system can non-deterministically choose
to loop or to move. If the system chooses to loop, it will stay at the same position withprobability 1. If the system chooses to move, it will move to x + 1 with probability 1/4,
or move to max(0, x − 1) with probability 3/4. Normalising the probability values bymultiplying by 4, we obtain the numeric weights of 4, 1, and 3 for the aforementioned
transitions, respectively.
To represent the system by regular relations, we encode the positions in unary andthe numeric weights in binary. The set of configurations is the regular language 1∗ . The
graph of the transition probability function can be described by a first-order formulaϕ(x, y, z) := ϕloop (x, y, z) ∨ ϕmove (x, y, z) over U , where
ϕloop (x, y, z) := x ∈ 1∗ ∧ y ∈ 1∗ ∧ ((x = y ∧ z = 100) ∨ (x 6= y ∧ z = 0)) ;ϕmove (x, y, z) := x ∈ 1∗ ∧ y ∈ 1∗ ∧ ((x ≺succ y ∧ z = 1) ∨(y ≺succ x ∧ z = 11) ∨ (x = ε ∧ y = ε ∧ z = 11) ∨(¬(x ≺succ y) ∧ ¬(y ≺succ x) ∧ ¬(x = ε ∧ y = ε) ∧ z = 0)).
tu
Example 2. As a second example, consider a PTS (from [25], Example 1) described bya probabilistic pushdown automaton with states Q = {p, q, r} and stack symbols Γ ={X, X 0 , Y, Z}. There is a unique action a, and the transition rules δa are as follows:
0.5

pX −−→ qXX
0.3
rX −−→ rY X
0.4
rX 0 −−→ rY X

0.5

pX −−→ p0.2
rX −−→ rY X 0
0.1
rX 0 −−→ rY X 0

1

qX −
→ pXX
0.5
rX −−→ r
0.5
rX 0 −−→ r

1

rY −
→ rXX

A configuration of the PTS is a word in QΓ ∗ , consisting of a state in Q and a word overthe stack symbols. A transition can be applied if the prefix of the configuration matches
the left hand side of the transition rules above. We encode the PTS as follows: the setof configurations is QΓ ∗ , the weights are represented in binary after normalization, andthe transition relation ϕ(x, y, z) encodes the transition rules in disjunction. For example,
0.5
the disjunct corresponding to the rule pX −−→ qXX isx ∈ QΓ ∗ ∧ y ∈ QΓ ∗ ∧ (∃u. x = pXu ∧ y = qXXu) ∧ z = 101.
Note that the PTS is bounded branching with a bound 3.
4.2

t
u

Proof rules for probabilistic bisimulation

Fix the set ACT of action symbols and the branching bound N ≥ 1, owing to the minimal probability assumption. Consider a two-sorted vocabulary σ = h{Pa }a∈ACT , R, +i,
where Pa is a ternary relation (with the first two arguments over the first sort, and thethird argument over the second sort of natural numbers), R is a binary relation over the
first sort, and + is the addition function over the second sort of natural numbers. The
main result we shall show next is summarized in the following theorem:
Theorem 1. There is a fixed first-order formula Φ over σ such that a binary relation
R is a probabilistic bisimulation over a bounded-branching PTS S = hS; {δa }a∈ACT i
iff (S, R) |= Φ. Furthermore, when S is a regular PTS and R is a regular relation,
we can compute in polynomial time a first-order formula Φ0 over U such that R is a
probabilistic bisimulation over S iff U |= Φ0 .
This theorem implies the following result:
Theorem 2. Given a regular relation E ⊆ Σ ∗ × Σ ∗ and a bounded-branching regular
PTS S = hS; {δa }a∈ACT i, there exists an algorithm that either finds (u, v) ∈ E which
are not probabilistically bisimilar or finds a regular probabilistic bisimulation relation
R over S such that E ⊆ R if one exists. The algorithm does not terminate iff E is contained in some probabilistic bisimulation relation but every probabilistic bisimulation
R containing E is not regular.
Note that when verifying parameterized systems we are typically interested inchecking bisimilarity over a set of pairs (instead of just one pair) of configurations,and hence E in the above statement.
Proof (of Theorem 2). To prove this, we provide two semi-algorithms, one for checking
the existence of R and the other for showing that a pair (v, w) ∈ E is a witness for nonbisimilarity.
By Theorem 1, we can enumerate all possible candidate regular relation R andeffectively check that R is a probabilistic bisimulation over S. The condition that E ⊆R is a first-order property, and so can be checked effectively.
To show non-bisimilarity is recursively enumerable, observe that if we fix (v, w) ∈E and a number d, then the restrictions Sv and Sw to configurations that are of distanceat most d away from v and w (respectively) are finite PTS. Therefore, we can devise
a semi-algorithm which enumerates all (v, w) ∈ E, and all probabilistic modal logic(PML) formulas [34] F over ACT containing only rational numbers (i.e. a formula ofthe form haiµ F 0 , where µ ∈ [0, 1] is a rational number, which is sufficient because
we assume only rational numbers in the PTS). We need to check that Sv , v |= F , but
Sw , w 2 F . Model checking PML formulas over finite systems is decidable (in fact,
the logic is subsumed by Probabilistic CTL [7]), which makes our check effective.

4.3

Proof of Theorem 1

In the rest of the section, we shall give a proof of Theorem 1. Given a binary relation
R ⊆ S × S, we can write a first-order formula Feq (R) for checking that R is anequivalence relation:∀s, t, u ∈ S. R(s, s) ∧ (R(s, t) ⇒ R(t, s)) ∧ ((R(s, t) ∧ R(t, u) ⇒ R(s, u)).
We shall next define a formula ϕa (p, q) for each a ∈ ACT, such that R is a probabilistic
bisimulation for S = hS; {δa }a∈ACT i iff (S, R) |= Φ(R), where^Φ(R) := Feq (R) ∧ ∀p, q ∈ S. R(p, q) ⇒(ψa (p) ∧ ψa (q)) ∨ ϕa (p, q). (3)
a∈ACT

0

0

The formula ψa (s) := ∀s ∈ S. δa (s, s ) = 0 states that configuration s cannot moveto any configuration through action a.
Before we describe ϕa (p, q), we provide some intuition and define some intermediate macros. Fix configurations p and q. Informally, ϕa (p, q) will first guess a set of
configurations u1 , . . . , uN containing the successors of p on action a, and a set of configurations v1 , . . . , vN containing the successors of q on action a. Second, it will guesslabellings α1 , . . . , αN and β1 , . . . , βN which correspond to partitionings of the configurations u1 , . . . , uN and v1 , . . . , vN , respectively. The intuition is that the α’s and β’s“name” the partitions: if αi = αj (resp. βi = βj ), then ui and uj (resp. vi and vj ) areguessed to be in the same partition. The formula then checks that the guessed partitioning is compatible with the equivalence relation R (i.e. if the labelling claims ui and uj
are in the same partition, then indeed R(ui , uj ) holds), and that the probability massesof the partitions assigned by configurations p and q satisfy the constraint given in (1).
For the first part, we define a formula^succa (w; u1 , . . . , uN ) :=ui 6= uj ∧1≤i<j≤N_∀u ∈ S. δa (w, u) 6= 0 ⇒u = ui ,1≤i≤N

stating that the successors of configuration w on action a are among the N distinct configurations u1 , . . . , uN . Note that a configuration may have fewer than N successors.
In this case, we can set the rest of the variables to arbitrary distinct configurations.
For the second part, we shall check that R is compatible with the guessed partitions,and that configurations p and q assign the same probability mass to the same partition.
Let k1 , . . . , kn be a labelling for configurations s1 , . . . , sn . To check that the partitioning induced by the labelling is compatible with R, we need to express the condition thatki = kj if and only if R(si , sj ) holds. To this end, we define a formula^compatR (s1 , . . . , sn ; k1 , . . . , kn ) :=(R(si , sj ) ⇔ ki = kj ) .
1≤i<j≤nNow, we are ready to define ϕa (p, q):
ϕa (p, q) := ∃u1 , . . . , uN , v1 , . . . , vN ∈ S. ∃α1 , . . . , αN , β1 , . . . , βN ∈ N.
succa (p; u1 , . . . , uN ) ∧ succa (q; v1 , . . . , vN ) ∧compatR (u1 , . . . , uN , v1 , . . . , vN ; α1 , . . . , αN , β1 , . . . , βN ) ∧X
X∀k ∈ N.
δa (p, ui ) =δa (q, vi ) .
i: αi =ki: βi =k

(4)

ρ

ρ

With this definition, ϕa (p, q) holds if and only if p −→a S 0 ⇔ q −→a S 0 holds for anyρ ≥ 0 and equivalence class S 0 ∈ S/R.
Example 3. Consider the PTS from Example 2. The configurations pXZ and rX areprobabilistic bisimilar. This can be seen using a probabilistic bisimulation relation withequivalence classes {pX k Z} ∪ {rw : w ∈ {X, X 0 }k } for all k ≥ 0 and {qX k+1 Z} ∪{rY w : w ∈ {X, X 0 }k } for all k ≥ 1. The probabilistic bisimulation relation isdefinable as the symmetric closure of a regular relation R, where (w1 , w2 ) ∈ R iff(w1 = w2 ) ∨(w1 ∈ pX ∗ Z ∧ w2 ∈ r(X + X 0 )∗ ⊥ ∧ |w1 | = |w2 |) ∨(w1 ∈ r(X + X 0 )∗ ∧ w2 ∈ r(X + X 0 )∗ ∧ |w1 | = |w2 |) ∨(w1 ∈ qX ∗ Z ∧ w2 ∈ rY (X + X 0 )∗ ⊥ ∧ |w1 | = |w2 |) ∨(w1 ∈ rY (X + X 0 )∗ ∧ w2 ∈ rY (X + X 0 )∗ ∧ |w1 | = |w2 |).
For this example, the formula (3) simplifies to Feq (R) ∧ ∀s, t ∈ S. ϕa (p, q) for theunique action a. This formula defines a condition that checks the bisimulation relation
for all states symbolically. To see the formula in action, fix configurations pXZ andrX which are probabilistic bisimilar. In the PTS, pXZ has two successors, qXXZ
and pZ, each with probability 0.5, and rX has three successors, rY X with probability
0.3, rY X 0 with probability 0.2, and r with probability 0.5. In the formula for ϕa (p, q),
we can set the successors ui of pXZ and the successors vj of rX as above (the third“successor” u3 is set to an arbitrary configuration not reachable from pXZ), and set
α1 = 1, α2 = 2, β1 = β2 = 1, and β3 = 2, corresponding to the equivalence classesof the bisimulation relation. One can check that the probability masses to these classes
are the same.
We remark that the first-order theory of U is sufficient to encode any probabilistic
pushdown automaton, not just this example.
tu
We proceed to show that if R and δa are first-order definable over U then so are ψaand ϕa . Suppose that δa is encoded using the ternary relation δa (x, y, z), as stated in
the previous section. (We shall re-use the symbol δ here to avoid a clash of names.)
We define ψa (s) := ∀s0 ∈ S. ∀z ∈ N. δa (s, s0 , z) ⇔ z = 0. To define ϕa , thekey is to express the sum of transition probabilities in the logic. We use the fact that
addition of integers in binary encoding is regular (see e.g. [9]), and write a formula that
performs iterated addition. Formally, for each a ∈ ACT we define a formula χa suchthatχa (u; u1 , . . . , uN ; α1 , . . . , αN ; k; z) :=∃z1 , . . . , zN +1 ∈ N. z1 = 0 ∧ zN +1 = z ∧

^
1≤i≤N

χ0a (u, ui , αi , k, zi , zi+1 ),whereχ0a (u, u0 , κ, k, x, y) := (κ = k ∧ ∃z. δa (u, u0 , z) ∧ y = x + z) ∨ (κ 6= k ∧ y = x)
performs a single addition—we use the fact that addition “y = x + z” in binary is
encodable as a regular relation—and z1 , . . . , zN +1 store the intermediate sums. Hence,

given k ∈ N, u1 , . . . , uN , v1 , . . . , vN ∈ S, and α1 , . . . , αN , β1 , . . . , βN ∈ N,X
X
δa (p, ui ) =δa (q, vi )i: αi =ki: βi =kif and only if∃z ∈ N. χa (p; u1 , . . . , uN ; α1 , . . . , αN ; k; z) ∧ χa (q; v1 , . . . , vN ; β1 , . . . , βN ; k; z).
It follows that ϕa (p, q) defined in (4) can be encoded in the first-order theory of U .
This concludes our proof of Theorem 1.
Remark. Note that it is decidable to check whether a given presentation of a regular PTS
is valid. To see this, suppose that a set ∆ := {δa (x, y, z)}a∈ACT of formulae is claimed
to encode the probabilistic transition functions of a PTS with a branching bound N .
Fix a formula δa ∈ ∆. First, we need to check that for all x ∈ S, there are at most N
distinct y’s such that δa (x, y, z) satisfies z 6= 0. Second, we need to check that [[δa ]] is afunction, i.e., ∀x, y. ∃!z. δa (x, y, z), where ∃!z. ϕ(x̄, z) is a shorthand for the formulaasserting there exists precisely one z such that ϕ(x̄, z) is true. Third, we need to checkthat [[δa ]] encodes a mapping S → {0} ∪ DS . The first two requirements are easily seen
to be expressible as a first-order formula and hence is algorithmic over U . The third
requirement amounts to checking the assertion that there exists wa ∈ N satisfying∀x ∈ S. (∀y ∈ S. ∀z ∈ N. δa (x, y, z) ⇔ z = 0) ∨(∃y1 , . . . , yN ∈ S. ∃z1 , . . . , zN ∈ N.
^
X
succa (x; y1 , . . . , yN ) ∧δa (x, yi , zi ) ∧
1≤i≤N

1≤i≤N

zi = wa ),which is a first-order formula and is algorithmic over U by the fact that summation of
a fixed number of weights is regular (as shown earlier in this section). Finally, since allof the wa ’s are expected to be the same common multiple of the denominators of thetransition probabilities, we need to check that there is w ∈ N such that wa = w for alla ∈ ACT. This is again algorithmic as we can pinpoint the exact value of each wa by
enumeration.

5

Application to Anonymity Verification

In this section, we show how to verify the anonymity property of cryptographic protocols via computation of probabilistic bisimulations. We shall first formalize the connection between the concepts of anonymity and probabilistic bisimulation. We thenintroduce a verification framework and apply it to verify the anonymity property of thedining cryptographers protocol [16] and the grades protocol [29].
A (discrete time) Markov chain (a.k.a. DTMC) is a structure M := hS; δ; Li where
S is a set of configurations, δ : S → DS is a family of probability distributions, and
L : S → ACT is a labelling of the states. We shall use δ(s, s0 ) to denote δ(s)(s0 ),the transition probability from s to s0 . A sequence s0 . . . sn ∈ S ∗ is called a path of
M if δ(si , si+1 ) > 0 for i ∈ {0, . . . , n − 1}. The probability distribution induced

by the paths in a DTMC can be defined using a standard cylinder construction (seee.g. [33]) as follows. Given a finite path π := s0 · · · sn ∈ S ∗ , we set Runπ to be a basic
cylinder, which is the set of all finite/infinite
paths with π as a prefix. We associate thisQn−1cylinder with probability Prs0 (Runπ ) = i=0 δ(si , si+1 ). This gives rise to a uniqueprobability measure for the σ-algebra over the set of all paths from s0 .
Given a PTS S := hS; {δa }a∈ACT i, an adversary f : S ∗ → ACT resolves thenon-determinacy of S and induces a DTMC Sf := hS 0 ; δ 0 ; L0 i. Here S 0 := S ∗ ∪ {$}contains all finite paths of S plus a “sink state” $ such that δ 0 (π) := I$ 6 if and only
if either π = $, or δf (π) is the zero function. We define δ 0 (π) := δf (π) otherwise. The
labelling of Sf is defined as L0 ($) := ⊥ and L0 (π) := f (π) for π ∈ S ∗ .
Given a DTMC hS; δ; Li, the trace of a path π := s0 · · · sn ∈ S ∗ is defined asτ (π) := L(s0 ) · · · L(sn ). A trace event T is a set of finite traces; theS probability of Twith respect to a configuration s is specified with Prs (T ) := Prs ( {Runπ : τ (π) ∈T , π starts from s}).
Now we are ready to define the concept of anonymity. Fix S := hS; {δa }a∈ACT i
and a set I ⊆ S of initial configurations. We say S is anonymous to an adversary f if
for all s ∈ I and trace event T , the value of Prs (T ) in Sf is solely determined by T .
Intuitively, this means that the adversary cannot obtain any information about a specificinitial configuration by experimenting on the system and observing the traces.
We shall only consider external adversaries in this paper. An adversary f : S ∗ →ACT is external if f (s0 · · · sn ) = f (s00 · · · s0n ) when L(si ) = L(s0i ) for i ∈ {0, . . . , n}.
That is, an external adversary takes action solely based on the trace she has observed sofar. We call a PTS anonymous if it is anonymous to any external adversary. The following result establishes a connection between the anonymity property and probabilistic
bisimulations.
Proposition 2. Let S := hS; {δa }a∈ACT i be a PTS and f be an external adversary for
S. Then for all u, v ∈ S such that u ∼ v, Pru (T ) = Prv (T ) holds for any trace event
T in Sf . That is, configurations u and v induce the same trace distribution in Sf .
Based on Proposition 2, we propose a framework to verify the anonymity propertyof S as follows. We first specify a “reference system” S0 := hS; {δa0 }a∈ACT i that has
the same initial configurations and actions as those of S, except that the trace distribution of S0f is independent of specific initial configurations for any adversary f . We thentry to find a bisimulation relation R between S and the reference system S0 satisfyingR ⊇ {(s, s0 ) ∈ I × I 0 : s = s0 }. When such a relation R is found, we can conclude
that the trace distribution of Sf is also independent of the initial configurations for any
adversary f , and hence prove the anonymity property of S.
The dining cryptographers protocol. Dining cryptographers protocol [16] is a multiparty computation algorithm aiming to securely compute the XOR of the secret bits heldby the participants. More precisely, consider a ring of n ≥ 3 participants p0 , . . . , pn−1such that each participant pi holds a secret bit xi . To compute x0 ⊕ · · · ⊕ xn−1 without
revealing information about the values of x0 , . . . , xn−1 , the participants carry out a6

Recall that Is denotes the point distribution at s, namely Is (s) = 1.

two-stage computation as follows: i) Each two adjacent participants pi , pi+1 computea random bit bi that is accessible only to them; ii) Each participant pi announces thevalue ai := xi ⊕ bi ⊕ bi−1 7 to the other participants. Hence, every participant pi canobserve the values of xi , bi , bi−1 and a0 , . . . , an−1 . It turns out that a0 ⊕ · · · ⊕ an−1 =x0 ⊕ · · · ⊕ xn−1 , so all participants are able to compute the XOR of the secret bits after
executing the protocol. Furthermore, the anonymity property of the protocol assuresthat any individual participant pi cannot infer the values of the other secret bits fromthe information she has observed during the execution of the protocol.
We model the protocol as a length-preserving regular PTS. The configurations ofa ring of n participants are encoded as words of size n. The initial configurations arewords w ∈ {0, 1}∗ such that w[i] represents xi for i ∈ {0, . . . , |w| − 1}. The transition relation consists of six transitions: observer non-deterministically tossing head (viaaction head), observer non-deterministically tossing tail (via action tail), non-observer
tossing head with probability 0.5 (via action toss), non-observer tossing tail with probability 0.5 (via action toss), participant announcing zero (via action zero), and participantannouncing one (via action one). The outcomes of the tosses by the observer are visible(i.e. as actions head and tail), while the outcomes of the tosses by the other participants are hidden (i.e. as action toss). Each maximal trace from an initial configurationof size n consists of n successive tossing actions, followed by n successive announcing
actions. Starting from an initial configuration w and for i ∈ {0, . . . , n − 1}, the i-th
toss action updates the value of w[j] to w[j] ⊕ bi for j ∈ {i, i + 1}, where bi = 1 if ahead is tossed and bi = 0 otherwise. Any configuration v reached after n tosses would
satisfy v[i] = xi ⊕ bi ⊕ bi−1 for i ∈ {0, . . . , n − 1}. The PTS then “prints out” theconfiguration by going through n announcement transitions via actions a0 , . . . , an−1 ,such that ai is one if v[i] = 1 and ai is zero if v[i] = 0.
We consider the case where the first participant of the protocol is the observer. The
maximal traces of the PTS in this case are in form of t · t0 , where |t| = |t0 |, t ∈{head, tail} toss∗ {head, tail}, and t0 ∈ {zero, one}∗ . For example, head toss tail one
zero zero is a maximal trace starting from initial configuration 010. To prove anonymity,
we define a reference system such that the initial configurations and the actions are
the same as those of the original PTS, except that the announcements a0 , . . . , an−1
encoded in the maximal traces from an initial configuration w are uniformly distributed
over {(a0 , . . . , an−1 ) : a0 ⊕ · · · ⊕ an−1 = w[0] ⊕ · · · ⊕ w[n − 1], a0 = w[0] ⊕b0 ⊕ bn−1 }.8 In this way, the distribution of the announcements is independent of theinitial configuration once the values of x0 ⊕ · · · ⊕ xn−1 , x0 , b0 , and bn−1 (i.e. theinformation revealed to the first participant) are fixed. We then compute a probabilistic
bisimulation between the original system and the reference system, establishing theanonymity property that the first participant cannot infer the secret bits of the otherparticipants from the information she observes.

7

All arithmetical operations on the subscripts are performed modulo n to take the ring structure
into account.
8
Such a distribution can be obtained by i) choose a1 , . . . , an−2 ∈ {0, 1} uniformly at random;ii) set a0 = w[0] ⊕ b0 ⊕ bn−1 ; iii) set an−1 = a0 ⊕ · · · ⊕ an−2 ⊕ w[0] ⊕ · · · ⊕ w[n − 1].

A generalized dining cryptographers protocol. We have also considered a generalized
dining cryptographers protocol where the secret messages x0 , . . . , xn−1 of the n participants are bit-vectors of the same size. Note that the set of the initial configurations
is not regular when the size of the secret messages is parameterized. To construct a regular model, we allow a configuration to encode secret messages of different sizes, anddevise the transition system such that an initial configuration w can finish the protocol(i.e. can have a trace containing all of the announcements a0 , . . . , an−1 ) if and only
if the messages encoded in w have same size. The resulting PTS is a regular system;
it over-approximates the PTS of the generalized dining cryptographers protocol in thesense that the anonymity property of the former implies that of the latter.
The grades protocol. The grades protocol [29] is a multi-party computation algorithm
aiming to securely compute the sum of the secrets held by the participants. The settingof the protocol is pretty similar to that of the dining cryptographers: given n ≥ 3 andg ≥ 2, we have a ring of n participants p0 , . . . , pn−1 where each participant pi holds asecret xi ∈ {0, . . . , g − 1}. Note that both g and n are parameterized in this protocol.
The goal of the participants is to compute the sum x0 + · · · + xn−1 without revealing
information about the individual secrets. Define M := (g − 1) · n + 1. The protocol
consists of two steps: i) Each two adjacent participants pi , pi+1 compute a random
number yi ∈ {0, . . . , M − 1}; ii) Each participant pi announces ai := (xi + yi −yi−1 ) mod M to the other participants. After executing the protocol, the participants
compute a := a0 + · · · + an−1 mod M . Because of the ring structure, the yi ’s will becancelled out in the sum. Thus the value of a will equal to the sum of all secrets. The
anonymity property of the protocol asserts that no participant can infer the secrets heldby the other participants from the information she has observed.
We consider a variant of the grades protocol where M can be any power of two
greater than (g − 1) · n. Observe that the same anonymity and correctness property ofthe original protocol also holds for this variant. To verify the anonymity property, we
model an over-approximation of the protocol where the secrets are allowed to range
over {0, . . . , M − 1}. This model is similar to the one we have constructed for the generalized dining cryptographers protocol except that, e.g., the XOR operations are now
replaced with bitwise additions and negations. A reference system is specified such thatthe announcements a1 , . . . , an−1 observed by the first participant p0 are uniformly distributed over the values satisfying a0 + · · · + an−1 mod M = x0 + · · · + xn−1 mod M .
By computing a probabilistic bisimulation between the original system and the reference system, we establish the anonymity property that the grades protocol is anonymous
whenever M is chosen as a power of two with M ≥ (g − 1) · n + 1.

6

Learning Probabilistic Bisimulations

We propose an automata learning method to automatically compute regular probabilistic bisimulations R, focusing on the case of length-preserving PTSs, which covers all examples given in the previous section. The approach uses active automata
learning, for instance Angluin’s L∗ method [5] or refinements of it, to compute R.

Algorithm 1: Equivalence check for L∗
Input: Candidate automaton H over Σ × Σ, PTS S, and regular relation E ⊆ (Σ × Σ)∗ .
Result: NoSolution(v, w)
if there is no bisimulation R with E ⊆ R;
PositiveCEX (v, w) if H should accept (v, w), but does not;
NegativeCEX (v, w) if H accepts (v, w), but should not;Correct
if H encodes a correct bisimulation for S and E ⊆ L(H).
Check whether E ⊆ L(H), and whether S |= Φ(L(H)) using the Φ from (3);if there is a counterexample of minimal length n then3
Compute the greatest bisimulation R̄n restricted to configurations of length n;
4
if there is (v, w) ∈ E \ R̄n with |v| = |w| = n then5
Output NoSolution(v, w) and abort;
6else if there is (v, w) ∈ L(H) \ R̄n with |v| = |w| = n then7
return NegativeCEX (v, w);
8else if there is (v, w) ∈ R̄n \ L(H) then9
return PositiveCEX (v, w);
10 else11
return Correct;
1

2

This approach is inspired by previous work on using active automata learning for invariant inference [18, 54]. Our procedure assumes (i) as input a bounded-branching
PTS S = hS; {δa }a∈ACT i, as well as a length-preserving regular relation E ⊆ (Σ×Σ)∗
supposed to be covered by R; (ii) an effective way to check the correctness of R, i.e.,a decision procedure in the sense of Theorem 1; and (iii) a procedure to compute thegreatest probabilistic bisimulation R̄n ⊆ (Σ × Σ)n for S restricted to configurationsof any length n ∈ N. The last assumption can easily be satisfied for length-preserving
PTSs. Indeed, such systems, restricted to configurations of length n, are finite-state, sothat efficient existing methods [6, 17, 20, 52] apply. A solution R is presented as a deterministic letter-to-letter transducer, i.e., as a deterministic finite-state automaton over
the alphabet Σ × Σ.
Since L∗ -style learning requires the taught language to be uniquely defined, ourapproach attempts to learn a representation of the greatest length-preserving probabilistic bisimulation relation R̄ ⊆ (Σ × Σ)∗ , which is the unique bisimulation relation formedby the union of all length-preserving probabilistic bisimulations of S, i.e.,SR̄ = n≥1 R̄n . Because R̄ is not in general computable, the learning process might diverge and fail to produce any probabilistic bisimulation. It can also happen that learningterminates, but yields a probabilistic bisimulation relation strictly smaller than R̄.
The L∗ method requires a teacher that is able to answer two kinds of queries:– membership queries, i.e., whether a pair (v, w) of words should be accepted by theautomaton to be learned. Since our learner tries to learn the greatest bisimulation,
the teacher can answer this query by checking whether the configurations v, w arebisimilar; this is done by computing the greatest bisimulation R̄|v| restricted toconfigurations of any length |v| = |w|, and checking whether or not (v, w) ∈ R̄|v| .
– equivalence queries, i.e., whether a candidate automaton H is the correct language
to be learned. Such queries can essentially be answered by checking whether thelanguage L(H) satisfies the formula Φ(R) from (3). The complete algorithm for answering equivalence queries is given in Algorithm 1. The algorithm first attempts tofind a shortest counterexample to the proof rule. If a counterexample of length n isfound, then the difference set L(H) ∆ R̄n must contain at least one pair of length n.
Any of such pairs is a valid counterexample for automata learning since the learnertries to learn the greatest bisimulation. The teacher thus reports one such pair to bea positive or negative counterexample according to its membership in R̄n .
Properties of the Learning Algorithm. The learning procedure terminates when theteacher outputs NoSolution or returns Correct for an equivalence query. In the former case, the teacher explicitly provides a pair of non-bisimilar configurations in E.
In the latter case, the procedure computes an automaton H such that E ⊆ L(H) andL(H) is a correct probabilistic bisimulation (as it satisfies the proof rule based on Theorem 1), though not necessarily the greatest one. Since all counterexamples reported by
the teacher are contained in L(H) ∆ R̄, the learning procedure is guaranteed to terminate for PTSs where the greatest probabilistic bisimulation R̄ is regular.
Optimization with Inductive Invariants. There is a natural way to optimize the learning
procedure by only considering a regular inductive invariant Inv such that Inv contains
the set of reachable configurations and E ⊆ Inv × Inv . The optimization is done bysimply replacing the greatest finite-length bisimulations R̄i in Algorithm 1, and whenanswering membership queries, with the greatest bisimulation R̄iI = R̄i ∩ Inv on the
inductive invariant. Since R̄iI can be a lot smaller than R̄i , this can lead to significant
speed-ups. Note that a bisimulation R0 on Inv can be extended to a bisimulation R on
all configurations by setting R = R0 ∪ {(v, v) : v 6∈ Inv }. The inductive invariant Inv
may be manually specified, or automatically generated using techniques like in [18, 54].
Experimental Results and Conclusion. We have implemented a prototype in Scala totest our learning method. Given a PTS specified over U , our tool first translates it to
WS1S formulas and obtains finite automata for these formulas using the Mona tool [30].
Our prototype then applies the L∗ learning procedure as described in this section, including the optimization to consider only the configurations of valid format. When answering an equivalence query, our tool invokes Mona to verify candidate automata andobtain counterexamples (line 1-2 of Algorithm 1). We use the prototype tool to prove
the anonymity property of the three protocols described in Section 5. The proofs generated by our tool are finite-state automata encoding the desired probabilistic bisimulation
relations. The experimental results are summarized in Table 1.

References
1. P. A. Abdulla, N. B. Henda, and R. Mayr. Decisive markov chains. Logical Methods in
Computer Science, 3(4), 2007.
2. P. A. Abdulla, B. Jonsson, M. Nilsson, J. d’Orso, and M. Saksena. Regular model checking
for LTL(MSO). STTT, 14(2):223–241, 2012.
3. P. A. Abdulla, B. Jonsson, M. Nilsson, and M. Saksena. A survey of regular model checking.
In CONCUR, pages 35–48, 2004.

Case study#states #trans mona bisim total
Dining Cryptographers, single-bit 13
832
2s
2s 6s
Dining Cryptographers, multi-bit
16 1024 3s 24s 28s
The grades protocol
25 1600 5s 28s 35s
Table 1. Experimental results. For each case study, we list the size of the final proof produced byour tool, the time taken by Mona to verify the candidate automata, the time taken by our tool tocompute the fixed-length bisimulations, and the total computation time of the learning procedure.
Experiments are run on a Windows laptop with 2.4GHz Intel i5 processor and 2GB memory limit.

4. W. Ahrendt, B. Beckert, R. Bubel, R. Hähnle, P. H. Schmitt, and M. Ulbrich, editors. Deductive Software Verification - The KeY Book - From Theory to Practice, volume 10001 of
Lecture Notes in Computer Science. Springer, 2016.
5. D. Angluin. Learning regular sets from queries and counterexamples. Inf. Comput.,75(2):87–106, Nov. 1987.
6. C. Baier. Polynomial time algorithms for testing probabilistic bisimulation and simulation.
In Computer Aided Verification, 8th International Conference, CAV ’96, New Brunswick, NJ,
USA, July 31 - August 3, 1996, Proceedings, pages 50–61, 1996.
7. C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008.
8. M. Benedikt, L. Libkin, T. Schwentick, and L. Segoufin. Definable relations and first-orderquery languages over strings. J. ACM, 50(5):694–751, 2003.
9. A. Blumensath. Automatic Structures. Diploma thesis, RWTH-Aachen, 1999.
10. A. Blumensath and E. Grädel. Finite presentations of infinite structures: Automata and interpretations. Theory Comput. Syst., 37(6):641–674, 2004.
11. B. Boigelot, A. Legay, and P. Wolper. Iterating transducers in the large (extended abstract).
In CAV, pages 223–235, 2003.
12. F. Bonchi and D. Pous. Checking NFA equivalence with bisimulations up to congruence. In
The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13, Rome, Italy - January 23 - 25, 2013, pages 457–468, 2013.
13. A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili. Regular model checking. In Computer
Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19,
2000, Proceedings, pages 403–418, 2000.
14. A. R. Bradley and Z. Manna. The Calculus of Computation: Decision Procedures with
Applications to Verification. Springer, 1998.
15. K. Chatzikokolakis, G. Norman, and D. Parker. Bisimulation for demonic schedulers. In
Foundations of Software Science and Computational Structures, 12th International Conference, FOSSACS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, pages 318–332,
2009.
16. D. Chaum. The dining cryptographers problem: Unconditional sender and recipient untraceability. Journal of cryptology, 1(1):65–75, 1988.
17. D. Chen, F. van Breugel, and J. Worrell. On the complexity of computing probabilistic
bisimilarity. In Foundations of Software Science and Computational Structures - 15th International Conference, FOSSACS 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, pages 437–451, 2012.
18. Y. Chen, C. Hong, A. W. Lin, and P. Rümmer. Learning to prove safety over parameterised
concurrent systems. In 2017 Formal Methods in Computer Aided Design, FMCAD 2017,
Vienna, Austria, October 2-6, 2017, pages 76–83, 2017.

19. T. Colcombet and C. Löding. Transforming structures by set interpretations. Logical Methods in Computer Science, 3(2), 2007.
20. S. Derisavi, H. Hermanns, and W. H. Sanders. Optimal state-space lumping in markov
chains. Inf. Process. Lett., 87(6):309–315, 2003.
21. J. Esparza and K. Etessami. Verifying probabilistic procedural programs. In FSTTCS 2004:
Foundations of Software Technology and Theoretical Computer Science, 24th International
Conference, Chennai, India, December 16-18, 2004, Proceedings, pages 16–31, 2004.
22. R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning About Knowledge. MIT Press,
Cambridge, MA, USA, 2003.
23. T. Fiedor, L. Holı́k, P. Janků, O. Lengál, and T. Vojnar. Lazy automata techniques for WS1S.
In TACAS’17, volume 10205 of LNCS, pages 407–425. Springer, 2017.
24. C. Flanagan, K. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static
checking for Java. In PLDI 02: Programming Language Design and Implementation, pages
234–245. ACM, 2002.
25. V. Forejt, P. Jancar, S. Kiefer, and J. Worrell. Bisimilarity of probabilistic pushdown automata. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012, December 15-17, 2012, Hyderabad, India, pages
448–460, 2012.
26. P. Garg, D. Neider, P. Madhusudan, and D. Roth. Learning invariants using decision trees andimplication counterexamples. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA,
January 20 - 22, 2016, pages 499–512, 2016.
27. P. Habermehl and T. Vojnar. Regular model checking using inference of regular languages.
Electr. Notes Theor. Comput. Sci., 138(3):21–36, 2005.
28. A. Hinton, M. Z. Kwiatkowska, G. Norman, and D. Parker. PRISM: A tool for automatic verification of probabilistic systems. In Tools and Algorithms for the Construction and Analysis
of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European
Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 April 2, 2006, Proceedings, pages 441–444, 2006.
29. S. Kiefer, A. S. Murawski, J. Ouaknine, B. Wachter, and J. Worrell. APEX: an analyzer for
open probabilistic programs. In Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, pages 693–698, 2012.
30. N. Klarlund and A. Møller. Mona version 1.4: User manual. BRICS, Department of Computer Science, University of Aarhus Denmark, 2001.
31. N. Klarlund, A. Møller, and M. I. Schwartzbach. MONA implementation secrets. International Journal of Foundations of Computer Science, 13(4):571–586, 2002. World Scientific
Publishing Company. Earlier version in Proc. 5th International Conference on Implementation and Application of Automata (CIAA) 2000, Springer-Verlag LNCS vol. 2088.
32. S. Kundu, Z. Tatlock, and S. Lerner. Proving optimizations correct using parameterized program equivalence. In Proceedings of the 30th ACM SIGPLAN Conference on Programming
Language Design and Implementation, PLDI ’09, pages 327–337, New York, NY, USA,2009. ACM.
33. M. Z. Kwiatkowska. Model checking for probability and time: from theory to practice. In
18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa,
Canada, Proceedings, page 351, 2003.
34. K. G. Larsen and A. Skou. Bisimulation through probabilistic testing. Inf. Comput., 94(1):1–
28, 1991.
35. K. R. M. Leino. Dafny: An automatic program verifier for functional correctness. In E. M.
Clarke and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010,

Revised Selected Papers, volume 6355 of Lecture Notes in Computer Science, pages 348–
370. Springer, 2010.
36. O. Lengál, A. W. Lin, R. Majumdar, and P. Rümmer. Fair termination for parameterizedprobabilistic concurrent systems. In TACAS, pages 499–517, 2017.
37. A. W. Lin and P. Rümmer. Liveness of randomised parameterised systems under arbitraryschedulers. In CAV’16 (2), volume 9779 of LNCS, pages 112–133. Springer, 2016.
38. C. Löding, P. Madhusudan, and D. Neider. Abstract learning frameworks for synthesis. In
Tools and Algorithms for the Construction and Analysis of Systems - 22nd International
Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory andPractice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, pages 167–185, 2016.
39. R. Milner. Communication and Concurrency. Prentice Hall, 1989.
40. D. Neider and N. Jansen. Regular model checking using solver technologies and automata
learning. In NASA Formal Methods, 5th International Symposium, NFM 2013, Moffett Field,
CA, USA, May 14-16, 2013. Proceedings, pages 16–31, 2013.
41. D. Neider and U. Topcu. An automaton learning approach to solving safety games overinfinite graphs. In TACAS, pages 204–221, 2016.
42. M. Nilsson. Regular Model Checking. PhD thesis, Uppsala Universitet, 2005.
43. O. Padon, G. Losa, M. Sagiv, and S. Shoham. Paxos made EPR: decidable reasoning about
distributed protocols. PACMPL, 1(OOPSLA):108:1–108:31, 2017.
44. O. Padon, K. L. McMillan, A. Panda, M. Sagiv, and S. Shoham. Ivy: safety verification
by interactive generalization. In Proceedings of the 37th ACM SIGPLAN Conference on
Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA,
June 13-17, 2016, pages 614–630, 2016.
45. PRISM case study: Dining Cryptographers. http://www.prismmodelchecker.
org/casestudies/diningcrypt.php.
46. S. Rubin. Automatic Structures. PhD thesis, University of Auckland, New Zealand, 2004.
47. G. Sénizergues. The bisimulation problem for equational graphs of finite out-degree. SIAM
J. Comput., 34(5):1025–1106, 2005.
48. J. Srba. Roadmap of Infinite results, volume Vol 2: Formal Models and Semantics. World
Scientific Publishing Co., 2004.
49. A. W. To. Model Checking Infinite-State Systems: Generic and Specific Approaches. PhD
thesis, LFCS, School of Informatics, University of Edinburgh, 2010.
50. A. W. To and L. Libkin. Recurrent reachability analysis in regular model checking. In LPAR,
pages 198–213, 2008.
51. A. W. To and L. Libkin. Algorithmic metatheorems for decidable LTL model checking overinfinite systems. In Foundations of Software Science and Computational Structures, 13th
International Conference, FOSSACS 2010, Held as Part of the Joint European Conferenceson Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010.
Proceedings, pages 221–236, 2010.
52. A. Valmari and G. Franceschinis. Simple O(m logn) time markov chain lumping. In Tools
and Algorithms for the Construction and Analysis of Systems, 16th International Conference,
TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice ofSoftware, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, pages 38–52,
2010.
53. A. Vardhan. Learning To Verify Systems. PhD thesis, Department of Computer Science,
University of Illinois at Urbana-Champaign, 2006.
54. A. Vardhan, K. Sen, M. Viswanathan, and G. Agha. Learning to verify safety properties.
In J. Davies, W. Schulte, and M. Barnett, editors, Formal Methods and Software Engineering, 6th International Conference on Formal Engineering Methods, ICFEM 2004, Seattle,

WA, USA, November 8-12, 2004, Proceedings, volume 3308 of Lecture Notes in Computer
Science, pages 274–289. Springer, 2004.