{'fraction_non_alphanumeric': 0.05658517350157729, 'fraction_numerical': 0.008995465299684542, 'mean_word_length': 3.851617145931727, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 25, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 47, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Axiomatising Infinitary Probabilistic Weak Bisimilarity of Finite-State Behaviours

In concurrency theory, weak bisimilarity is often used to relate processes exhibiting the same observable behaviour. The probabilistic environment gives rise to several generalisations; we study the infinitary semantics, which abstracts from a potentially unbounded number of internal actions being performed when something observable happens. Arguing that this notion yields the most desirable properties, we provide a sound and complete axiomatisation capturing its essence. Previous research has failed to achieve completeness in the presence of unguarded recursion, as only the finitary variant has been axiomatised, yet.


Introduction
A major branch of concurrency theory is concerned with categorising semantic resemblances of processes modelled as labelled transition systems, by studying the interconnections and differences of a diverse set of equivalence relations on processes. In his papers on the linear time -branching time spectrum [8,10], the second author arranged many relevant equivalences in a lattice structure: A 'horizontal' dimension of the lattice of [10] distinguishes the relevant relations according to divergence sensitivity while the 'vertical' dimension orders them with respect to their discriminating power concerning the processes' branching structure, ranging from branching bisimilarity as the finest relation to trace equivalences. Several of these relations, especially bisimilarities, have been captured axiomatically [9,12], rooted in the seminal work of Robin Milner [14] in the setting of a process language involving recursion.
In this work, we consider a more general setting involving probabilities, so as to be able to reason about randomised concurrent systems. The linear time -branching time spectrum carries over; however, in this more general context it makes sense to introduce another dimension into the spectrum. As depicted in Figure 1, each equivalence comes in four different flavours: On the one hand, we distinguish between convex (c) and non-convex relations and, on the other hand, we discriminate finitary (fin) and infinitary (inf) probabilistic behaviours. The convexity property is thoroughly investigated and is mentioned in various axiomatisations [1,4], so far exclusively interwoven with the finitary probabilistic character, while the infinitary version has not been axiomatised yet, to the best of our knowledge.
The finitary and infinitary semantics arise from different definitions of the underlying weak transitions. As an example consider the two processes depicted in Figure 2; τ denotes the silent action that is assumed to be invisible for external observers. The finitary semantics yields weak transitions that can only hide a finite number of τ actions. Here, after a bounded number of steps, the process on the right-hand side is guaranteed to perform an observable a action, while the left-hand side still resides in its initial state with positive probability. Hence, the processes are distinguished by ≈ fin . However, if we allow infinitary transitions there is no step bound and the probability of residing in the initial state of the left process, i.e. the probability of looping forever, becomes 0. Consequently, the a action happens almost surely as well and ≈ inf relates both systems.
The infinitary semantics is not to be confused with divergence sensitivity; both processes are said to be convergent. Even though we allow weak transitions of unbounded size, there essentially exists no diverging trace, i.e. an infinite sequence of τ transitions occurring with positive probability.
Both transition variants frequently occur in literature: Finitary weak transitions form the basis of [1,4,5]. Infinitary weak transitions have been proposed in different, (nearly) equivalent shapes, mainly defined by means of schedulers [16,2,7,11], derivations [3] and transition trees [6]. Note that a distinction between finitary and infinitary behaviours only arises when dealing with recursion (or infinite processes). This insight may justify a simplified formalisation in some settings, as for instance in [1].
In this paper, we focus on the most prominent equivalence of the linear time -branching time spectrum, namely weak bisimilarity, ≈. We argue that the convex infinitary relation ≈ inf c , as the coarsest variant, yields the most natural and desirable semantics. We choose the convex form of weak bisimilarity, because the non-convex one either leads to a non-transitive bisimilarity, or to a notion that fails to be a congruence, or fails to satisfy some natural axioms. Additionally, the convex form is more in line with the way randomised algorithms resolve nondeterminism. We choose the infinitary form for two reasons: Firstly, systems involving lossy channels or Las Vegas algorithms that keep resending information until successfully delivered (conceptually similar to the left process of Figure 2) are most commonly not intended to be differentiated from their respective deterministic versions. Secondly, the authors of [5] have established an axiomatisation of ≈ fin c that turns out to be incomplete for expressions containing unguarded variables. They even conjecture that the relation is undecidable, so that a finite axiom set cannot exist.
Even though decision [2,11] and minimisation [6] algorithms have been developed, there is no axiomatisation of infinitary probabilistic weak bisimilarity, yet. An axiomatisation is interesting from a theoretical point of view, since it allows a concise characterisation of the respective relation, here ≈ inf c . We propose a conservative extension of Milner's foundational work [14], generalising some laws appropriately and introducing a fresh axiom expressing the nature of infinitary semantics.
As to be expected, the main challenge turns out to be the proof of completeness of the axiom set. We  follow Milner's proof steps closely, but encounter some additional obstacles: Several proofs by induction on the length or the number of weak transitions become infeasible. We manage to overcome this by exploiting some facts of Markov Decision Theory. Often we need to leap from induction to coinduction (at least conceptually), while the proof ideas remain similar. This paper is organised as follows: Section 2 introduces all necessary preliminary definitions, section 3 presents the axiom set and the sections 4 and 5 prove the axiomatisation sound and complete, respectively. Section 6 concludes and gives an outlook on further work.
The support ⌈µ⌉ of a subprobability distribution µ is a set containing an element s ∈ S iff µ(s) > 0 and the size |µ| = ∑ s∈S µ(s) of µ states the probability mass distributed over all supported elements. If |µ| = 1, then we call µ a probability distribution. We shall denote the set of all subprobability distributions (resp. probability distributions) over S by D ≤1 (S) (resp. D =1 (S)), which is usually ranged over by Greek letters µ, ν, γ, η, π, . . .. Let / 0 denote the empty distribution supporting no elements and for s ∈ S, we define δ (s) as a Dirac distribution, assigning 1 to s and 0 to all other elements. Occasionally, we write {s i → p i } to express a distribution assigning p i to s i , for each i.
Moreover, we define some straightforward operations on (sub-)probability distributions: Let ≤ be introduced as a pointwise comparison of distributions, i.e. µ ≤ ν, if µ(s) ≤ ν(s) for all s ∈ S. We find natural notions for addition and subtraction as well: For µ, ν with |µ| + |ν| ≤ 1, let µ + ν denote the distribution assigning µ(s) + ν(s) to s ∈ S and given ν ≤ µ, let µ − ν be defined in the obvious way. Finally, for any scalar 0 < λ < 1 |µ| , λ µ denotes the pointwise rescaling of µ. When not considering probabilities, we argue about processes represented by transition systems. In our context, (simple) probabilistic automata [16] generalise this concept naturally and therefore form the semantics of the process algebra to be established. Our understanding of probabilistic automata agrees with the probabilistic transition systems of [3]. • s 0 ∈ S is the initial state.
We will often use transition diagrams to describe probabilistic automata. The empty circles represent states, while the filled circles 'split' a transition leading to multiple target states.

Process algebra
Our process algebra extends the process algebra of [14] by a binary operator for probabilistic choice.
Equivalently it extends the process algebra of [17] with an operator + for nondeterministic choice, and it extends the process algebra of [1] by a recursion operator, such that every finite-state system involving finitely many nondeterministic and probabilistic choices becomes expressible. We are not considering a prefix operator with the same generality as in [4], since this operator leads to generalised probabilistic automata as described in [16].

Syntax
We distinguish between two syntactic categories, namely nondeterministic expressions (collected in E and ranged over by E, F, . . .) and probabilistic expressions (collected in P and ranged over by P, Q, . . .). Let V denote a set of process variables and let A be a set of action labels, where τ ∈ A represents the internal action. Then the syntax is given by: E + E, (nondeterministic choice) P ::= ∂ (E) (Dirac choice) (probabilistic choice, 0 < p < 1) The nondeterministic expressions stem from Milner's CCS [13]. As usual, 0 denotes the inactive process yielding no outgoing transitions. We use process variables in addition to the recursion operator to express arbitrary loops and the + operator expresses choice. In contrast to [13], a prefixing expression consists of an action α and a probabilistic expression, which may be read as a probability distribution over nondeterministic expressions. ∂ (E) represents a Dirac distribution supporting E, while P p ⊕Q constructs a convex combination of the distributions corresponding to P and Q. Here, to avoid corner cases, we require 0 < p < 1. We sometimes abbreviate α.∂ (E) with α.E.
Hereinafter, we will often write ∑ i∈I E i as a notation for the nondeterministic sum E 1 + . . . + E n for some index set I = {1, . . . , n}. The set nature will be justified by the commutativity and associativity of +. Moreover, let • ∑ i∈I [p i ] P i , always assuming ∑ i∈I p i = 1, denote P 1 q 1 ⊕ (P 2 q 2 ⊕ (. . . q n−1 ⊕ P n ) . . .) for some appropriate values q i , such that p i indicates the probability of choosing P i , respectively, and let An occurrence of a variable X in an expression E is called free if it does not lay within some subexpression µX . F; we gather all variables occurring free in E in V(E). E is called closed if V(E) = / 0 and open otherwise; let C ⊂ E denote the set of all closed expressions. For expressions F = (F 1 , . . . , F n ) and variables X = (X 1 , . . . , X n ), E{ F/ X } denotes the expression E after simultaneously replacing each free occurrence of X i in E with F i , while renaming bound variables in E as needed to avoid free variables in F to become bound in E{ F/ X }. Finally, let ≡ denote syntactical equality of expressions.

Semantics
As usual, the semantics of an expression E is given by the PA is the smallest relation satisfying the inference rules given in Table 1, where α ranges over A.
The operational rules characterise the auxiliary relation −→ ⊆ P × D =1 (E) as follows: Given some probabilistic expression P, it points to the probability distribution over all nondeterministic expressions occurring in P.
However, the probabilistic case is somehow ambiguous, since one could think of multiple different generalisations. We are going to analyse two important properties before fixing our final understanding of weak transitions.

Convexity
First of all, we design =⇒ c to be convex, meaning that whenever E =⇒ c µ and E =⇒ c ν, then there is also a transition leading to every convex combination of µ and ν: E =⇒ c p · µ + (1 − p) · ν for any p ∈ [0, 1]. The motivation behind this convexity property arises from the concept of schedulers: Essentially, any weak transition performs a run through a PA following the transitions chosen by some scheduler in every state. If we consider randomised schedulers, i.e. schedulers that may randomly choose a transition instead of deterministically fixing a decision, then the resulting weak transitions happen to be convex. Analogously, the non-convex variant corresponds to deterministic schedulers. It seems desirable to assume randomised schedulers, such that potentially randomised algorithms may resolve nondeterminism [16].
In subsection 2.5 we will revisit this decision, and try to define a notion of weak bisimilarity based on non-convex weak transitions. The technical problems that ensue are another argument for using convex weak transitions.
Preliminarily, we introduce the convex lifting of a relation , which is the smallest relation satisfying: Sometimes, we refer to α −→ c as combined strong transitions.

Finitary vs. Infinitary
Next, we continue discriminating further between finitary and infinitary weak transitions. The difference is best explained by an example: Consider the probabilistic automaton depicted in Figure 3; it does not introduce nondeterministic choices. We raise the question, whether there exists an a-labelled weak as an infinite transition tree on the right. transition leading from s to u. Certainly, the PA would be required to move silently from s to t with probability 1. We simulate a run through the automaton by the transition tree depicted on the right: Each internal node represents an intermediate state of the run and each leaf represents a state in which the transition stops. Now distinguish two cases: If the transition tree is finite, i.e. of arbitrary, yet limited depth k, the desired transition cannot exist! Clearly, there is a remaining probability of ( 1 2 ) k > 0 of still residing in the initial state s. This semantics corresponds exactly to finitary transitions =⇒ fin c , being defined inductively in Table 2. As long as the transition tree is of finite depth, it can be constructed by the inference rules of =⇒ fin c , but a transition s =⇒ fin c δ (t) cannot exist. However, if we allow infinite trees, the probability of staying in s becomes lim k→∞ ( 1 2 ) k = 0, i.e. with probability 1 the transition leads to t: s =⇒ inf c δ (t). We continue defining =⇒ inf c formally, which requires more effort than for finitary transitions. The following construction is borrowed from [3].
as an infinite sequence of τ transitions, which is allowed to stop partially after each step:

Basic properties
As argued before, we focus on convex infinitary transitions from now on. Thus, we assign =⇒ = =⇒ inf c and discontinue explicitly annotating c, fin and inf. The distinction between α −→ and α −→ c will be clear from the context.
It is vital to assert some basic properties about =⇒ as defined by derivations. Most of the results are established by [3]; note that even seemingly easy statements have led to exhausting proofs.
We state some more propositions that turn out to be particularly helpful in the proofs to come.
The direction (b) implies (a) is immediate by reflexivity of =⇒. Moreover, (b) and (c) are easily proven equivalent by some rewriting. ✷ Simply take γ = µ × 0 , then obviously γ ≤ µ and γ ≤ ν. Now think of the derivation from before, after assigning PROOF. Although the statement should hold in general, our context allows us to assume a finite state space S, with finitely many transitions. Then [3] shows that the set {ν | µ 0 =⇒ ν} is closed. Hence, for an arbitrary convergent sequence (γ i ) i∈AE :

Weak bisimilarity and weak congruence
Given a relation R ⊆ S × S, we lift it to a relation R p ⊆ D ≤1 (S) × D ≤1 (S) on subdistributions as follows [3]: Let R p be the smallest relation satisfying Definition 4 (Weak bisimilarity) A relation R ⊆ C × C is called a weak bisimulation if, for every pair (E, F) ∈ R, the following conditions hold: (i) whenever E α −→ µ, then there is some ν, such that Fα =⇒ ν and µ R p ν, (ii) whenever F α −→ ν, then there is some µ, such that Eα =⇒ µ and µ R p ν. This definition matches Segala's weak probabilistic bisimilarity [16]. It is well-known that ≈ is not a congruence relation with respect to +. So instead, we prefer dealing with the coarsest congruence relation contained in ≈, which is equivalently defined as follows: Definition 5 (Weak congruence) Two closed expressions E, F are called weakly congruent, denoted E ≃ F, if the following conditions hold: (i) whenever E α −→ µ, then there is some ν, such that F α =⇒ ν and µ ≈ p ν, (ii) whenever F α −→ ν, then there is some µ, such that E α =⇒ µ and µ ≈ p ν.
Formally, weak bisimilarity and weak congruence only differ in their respective choice of weak transitions (α =⇒ vs. α =⇒). For α = τ both characterisations agree, the difference is spotted in the case that α = τ: If E ≃ F and E τ −→ µ, F is guaranteed to evolve into some distribution ν ≈ µ by actually making progress (F τ =⇒ ν), while in the case of E ≈ F, the only guarantee is F =⇒ ν, that is, F could also idle.
From now on, we will no longer explicitly annotate R p , when addressing the probabilistic lifting of some relation R.
We proceed with some useful facts concerning weak bisimilarity and weak congruence.
PROOF. By the definition of convex lifting µ and µ ′ must have the forms ∑ i∈I p i δ (E i ) and ∑ i∈I p i µ ′ i for The definition of the lifting of ≈ from nondeterministic expressions to subdistributions implies that ν has the form ∑ i∈I p i ν i with ν i ≈ δ (E i ) for all i. This, in turn, implies that each ν i has the form i, j for all i and j, and we reach the same conclusion in three steps. ✷ In the exact same way one obtains: Visualise the next proposition as the following completable diagram. A similar statement holds for weak congruence, as well.
PROOF. We find it convenient to first prove the statement for the case α = τ.
; from now on we ensure that this invariant keeps maintained for all i that have already been considered.

Non-convex weak bisimilarity
Let us further motivate why we only focus on an axiomatisation of the convex weak bisimilarity. A non-convex version =⇒ fin of the finitary weak transition relation can be defined as in Table 2, but changing the second rule into s τ −→ µ s =⇒ fin µ ; this yields the non-convex finitary transition relation proposed in [5]. The non-convex version of the infinitary transitions is then defined in such a way that for finite (recursion-free) processes it coincides with the finitary version.
Suppose we would define non-convex weak bisimilarity exactly as in Definition 4, but using the (finitary or infinitary) non-convex weak transition relation instead of the infinitary convex one. Then, as documented in [5], the resulting notion fails to be transitive. 1 The following is a mild simplification of the counterexample of [5].
A crucial difference between convex and non-convex finitary transitions is that R =⇒ fin c µ whereas R =⇒ fin µ, for µ = {a.0 → 1 2 , b.0 → 1 2 }. However, since R =⇒ fin a.0 and R + 0 =⇒ fin b.0 it follows that τ.(∂ (R) 1/2 ⊕ ∂ (R + 0)) =⇒ fin µ. Using this, it is easy to see that E is non-convex weakly bisimilar to F. Furthermore, since R is non-convex (weakly) bisimilar to R + 0, it follows immediately from the definition of lifting that {R → 1 2 , R + 0 → 1 2 } is non-convex (weakly) bisimilar to δ (R). Hence also F and G are non-convex weakly (even strongly) bisimilar. Yet, E and G are not non-convex weakly bisimilar, for E =⇒ fin µ, and this transition cannot be matched by G (or R). One might wish to give a different definition of non-convex weak bisimilarity that avoids this problem. The only reasonable way appears to make F and G non-bisimilar. This can be done by reformulating the condition of Definition 4: whenever E α =⇒ µ, then there is some ν, such that Fα =⇒ ν and µ R p ν. The price for this would be, however, that non-convex weak bisimilarity does not include non-convex strong bisimilarity as defined in [16], and moreover, either axioms N4 or P3 of section 3, or the congruence property, needs to be given up.

Guardedness
Milner's complete axiomatisation of CCS [14] crucially depends on the guardedness property of CCS expressions. He defines X to be unguarded in E if there is some occurrence of X not being in the scope of some α-prefixing with α = τ, and guarded otherwise. We refer to this definition as nonprobabilistic guardedness. However, this notion turns out to be too restrictive in our setting, so instead we define a probabilistic lifting: Table 3, and (probabilistically) guarded otherwise. An expression E is called (probabilistically) guarded, if for every recursion µX . F, occurring as a subterm of E, X is guarded in F.
When considering the fragment of our process algebra without the operator p ⊕, one has E ✄ V only when V is a singleton. In that case E ✄ {X } holds exactly when X occurs free and unguarded in E as defined by Milner [14,13], and our definition yields the same notion of a guarded expression as used in CCS.
To understand Definition 6 better, call an occurrence of a variable X in a nondeterministic expression E strongly unguarded if it is free and does not occur within a subexpression α.P, including the case that α = τ. Now E ✄ V , for V a set of variables, guarantees that, by executing a weak transition, E can evolve into a probability distribution µ, such that, for each expression F ∈ ⌈µ⌉, one of the variables in V occurs strongly unguarded in F. In case V has the form {X } this means that X occurs strongly unguarded in each expression F ∈ ⌈µ⌉. Here we mention this for the sake of intuition only; in Appendix A we will make this more precise and use it to obtain the soundness of our only axiom that depends on guardedness.

Example 3 Consider the expression
It holds that X is probabilistically guarded in E, E ✄ {X }, although X occurs nonprobabilistically unguarded in E! However, we have E ✄ {X ,Y }. This confirms the explanation above, as there is a silent move from E to the distribution {X → 1 3 ,Y + a.0 → 2 3 }. From E ✄ {X ,Y }, infer that also µY. E ✄ {X }. The correspondence still holds: µY. E =⇒ δ (X ).

Axiomatisation
We give equational laws that precisely capture the essence of ≃. More formally, we introduce a relation =, which relates two expressions E and F if and only if E may be transformed into F by applying the axioms of Table 4 only. Importantly, = is designed to be a congruence relation, meaning that an axiom may be applied to some subexpression of E, as well. Besides, = always allows appropriate renaming of variables. In the end, our goal is proving that ≃ and = coincide. Given this use of the symbol =, we use ≡ for syntactic identity. In this section, we have a closer look at the provided axioms. First of all, N1-N4 express basic algebraic properties of nondeterministic choice: commutativity, associativity, idempotence and 0 being the neutral element of +. These axioms on their own are sound and complete for strong bisimilarity in the absence of recursion [13,14].
The axioms P1-P3 stem from [17] and state simple properties of probabilistic choice. Normally, we do not tag applications of these laws. Instead, we often implicitly assume the convenient shape Next, focus on T1-T4. The axioms T1 and T4 are conservative generalisations of Milner's [14] axioms α.τ.E = α.E and α.(E + τ.F) + α.F = α.(E + τ.F), respectively. However, we are required to introduce two extensions of E + τ.E = τ.E. On the one hand, if E is a prefix expression, then T3 allows some transformations potentially involving quantities. On the other hand, we still rely on T2 if E is a variable, for instance. Remark that each closed instance of T2 becomes derivable in the presence of T3 when not considering recursion [1]. The axioms T1, T3 and T4 first appeared in [1] and T1-T4 occurred in [5], too, in almost equal forms.
The convexity axiom C captures the convex property of combined transitions: Whenever E α −→ µ and E α −→ ν, C essentially allows to add or remove transitions leading to a convex combination of µ and ν.
Finally, we analyse the recursion axioms. R1 and R2 establish existence and uniqueness of equation's solutions; R2 premises the equation E to probabilistically guard X . Fortunately, R2 can be shown to remain sound even after having loosened the guardedness notion. The axiom R3 is new. It expresses exactly the infinitary character of weak transitions: Suppose that P is of the shape • ∑ n i=1 [p i ] G i and consider the following depiction: The processes E, F may be ignored for now; they are only required to fit in a most general context. Now, there is a transition targeting G 1 , . . . , G n with some probability < 1. The remaining probability mass reaches some state providing the exact same transition, again. So intuitively, R3 allows unrolling this transition infinitely many times, until some G i is certainly reached. This weak transition corresponds to a scheduler that always schedules the aforenamed transition while no G i is visited, and halts otherwise. We continue presenting the remaining axioms: In Milner's context, R4-R6 serve the purpose of transforming an arbitrary expression into a guarded one. Here, the law R5 will also be required again in a later part of the completeness proof. Both R4 and R5 agree with their original versions exactly [14], whereas R6 describes an interesting generalisation: Think of a random experiment with outcomes E 1 , . . . , E n ; we ignore F for now. Now R6 states: If we are allowed to repeat the experiment unboundedly often and halt whenever convenient, then in fact, the actual probabilities p i do not matter, as we can nondeterministically choose which outcome is selected. More formally, suppose you want to visit some state offering E i on the left-hand side. Then we follow the weak transition corresponding to a scheduler that always loops, until the respective target state is reached. This transition does not diverge, as the probability of not visiting the desired state converges to 0. So R6 exploits the infinitary property, again.
Deng and Palamidessi [4,5] established axiomatisations taking the finitary transition variant as a basis. Consequently, the law R6 is not sound in their context, and there is no other obvious generalisation of Milner's original. Thus, that axiomatisation turns out to be incomplete for nonprobabilistically unguarded expressions. In fact, the authors conjecture that the problem even becomes undecidable when considering arbitrary expressions.
The next sections are concerned with proving the soundness and completeness of =.

Soundness
Soundness asserts that whenever some expressions E, F are equal according to the axioms, then indeed, E ≃ F. Once we establish that ≃ is a congruence (Theorem 1), each axiom may be considered on its own and a soundness proof typically finds a weak bisimulation relating the desired expressions, before additionally checking the root condition of weak congruence. Thanks to the definition of ≃, it suffices to show the soundness of these laws for closed expressions only. Most axioms are proven correct easily: We are not giving proper proofs for the axioms N1-N4, the interested reader may refer to [13]. The axioms P1-P3 essentially express some rewriting identities that lead back to basic mathematical properties. T1-T4 rely on some characteristics of probabilistic weak transitions, however, they do not depend on =⇒ being infinitary! Therefore, the proofs of [4] carry over naturally. Moreover, the axiom C is immediate by the convexity property of α =⇒. We distinguish further between the recursion axioms; the axioms R1, R4 and R5 are identical to Milner's versions, thus, we omit the proofs and, again, refer to [13]. However, the remaining axioms R3 and R6 turn out to be particularly interesting, as they strongly rely on the infinitary property of =⇒. Lastly, R2 takes a special role just like in the nonprobabilistic setting, which results in an exhausting proof, but interesting insights. We continue focusing on these challenging laws in this section.
Before, we shall lift some already known terminology to (sub-)probability distributions: We say a distribution µ is (probabilistically) guarded, if every expression supported by µ is probabilistically guarded. Moreover, let µ{E/X } denote the subdistribution µ after substituting E for X in every supported expression.
Some of the following proofs rely on Milner's 'bisimulation up to' technique [13], merely adapted to our context: Definition 7 (Rooted weak bisimulation up to ≈) A relation R ⊆ C × C is called a one-sided rooted weak bisimulation up to ≈, if the following conditions hold for all (E, F) ∈ R: , then there is some µ, such that E α =⇒ µ and µ ≈R≈ ν. Here, R≈ (≈R≈) denotes the composition of (≈ p and) R p and ≈ p . For the two-sided variant, we add the convenient assumption |µ| = 1, such that we are only required to deal with convergent transitions E α =⇒ µ.
It turns out that any two expressions related by a rooted weak bisimulation up to ≈ are in fact weakly congruent, as shown by the following lemmas. We benefit from this approach by not being obliged to find an exact weak bisimulation relating two given processes, but rather proving the relaxed statement tolerating additional ≈-relations in between.
We are left to prove ( * ), so let γ =⇒ γ ′ be derived by PROOF. By Lemma 3, we can assume that R is a two-sided rooted weak bisimulation up to ≈. We first show that ≈R≈ is a weak bisimulation.
and the desired transition is constructed as a convex combination. Next, let α = τ. Then trivially We still need to consider the root condition of congruence (Definition 5): and for all probabilistic expressions P, Q, R ∈ P with P ≃ Q we have: Here we write P ≃ Q when the unique distributions pointed to by P and Q are weakly congruent.
PROOF. The transitivity of ≃ follows immediately by Proposition 10. Reflexivity and symmetry are trivial, thus, ≃ is an equivalence relation. The proofs of (2)(a), (c), (d) and (e) are straightforward, and the proof of (2)(b) is similar to [13], using the one-sided 'up to' technique of Definition 7 and Lemma 4. ✷ Lemma 5 (Soundness of R3) Let E, F ∈ E and P ∈ P.
PROOF. Without loss of generality we may assume that the other direction then becomes obvious. We perform an induction on the inference tree deriving K{H/X } α −→ µ while making a case distinction on the shape of K: the transition, then we are easily finished, by induction. So let τ.P{H/X } α −→ µ. It follows that α = τ and with P being of the PROOF. Without loss of generality we may assume that Define R as the relation containing a pair for all expressions K with free variables in {X }. It is enough show that R is a one-sided rooted weak bisimulation up to ≈. First, pick some pair (K{G/X }, K{H/X }) ∈ R and assume K{G/X } α −→ µ. We prove that K{H/X } α −→ ν ≈R −1 µ for some ν by carrying out an induction on the inference tree deriving the transition; proceed as in Lemma 5. Again, the case K ≡ X turns out to be most interesting: Then either The latter case is easy; conclude by induction. The former case entails α = τ and µ ≡ {G We perform a similar induction and focus on the case The transitions γ → i τ −→ γ i+1 obtain naturally, so indeed, there is a transition PROOF. By induction on the proof of E = F. Such a proof can be formalised as a finite tree of which the nodes are labelled with equations G = H with G, H ∈ E or G, H ∈ P, the root is labelled with E = F, and each node applies either reflexivity, symmetry or transitivity of =, the congruence property of Theorem 1, or one of the axioms of Table 4. Axioms are applied only in leaf nodes, except for R2. The induction is a straightforward application of Theorem 1 and the soundness of the individual axioms. ✷

Completeness
The completeness proof follows Milner's proof [14] as far as possible. It might be helpful to be familiar with his fundamental work ( Figure 4 outlines the major steps), however, we feel confident that the prospective proofs are well-understandable without prior knowledge, too.

Example 4
The upcoming steps are illustrated by the example depicted in Figure 5; here Note that E and F are in fact weakly congruent. It is easy to find a weak bisimulation (relate E to F and to both τ successors of E and F); the root condition is trivial.

Reduction to guarded expressions
The initial step of the completeness proof transforms an arbitrary expression into an equal, yet guarded one. It turns out that guardedness is a particularly useful property when dealing with equation systems later on. Before we begin, let us briefly discuss which guardedness notion suits our context. Recall that we introduced probabilistic and nonprobabilistic guardedness; it might not be obvious why we cannot reduce to nonprobabilistically guarded expressions in general! To see this, consider the PA depicted in Figure 6, which is induced by the expression G with G happens to be probabilistically guarded, but nonprobabilistically unguarded. Now, a nonprobabilistically guarded, equal PA is required to collapse the states G and H that currently establish the problematic τ-loop. Clearly this is not possible; the state G is able to reach the left state with maximal probability < 1 2 , whereas H may reach the same state with probability > 1 2 . Hence, G and H are not bisimilar and there cannot exist a nonprobabilistically guarded expression equal to G.
Fortunately, it is possible to transform any expression into a probabilistically guarded expression. We begin by asserting the following lemma: PROOF. The statement is shown by proving a stronger claim. Let E ✄ V for some V ⊂ V. Then one of the following statements holds: for some expressions F i, j and probabilities p i and q i, j .
First, analyse the two cases: (1) primitively extends the non-probabilistic case, whereas (2) is new in the context of probabilistic prefixing. Intuitively, this case states that even if there are two or more variables unguarded in E, then there has to be some τ prefixing in E, that may be dragged out. We show the claim by an induction on the structure of E.
We obtain (1) by axiom N3. The other case implies |V | > 1 and hence leads to a contradiction.
Thus, for an arbitrary probabilistic expression P: If |V k | > 1 instead, then by induction there are expressions G k,i, j , such that In any case: the former case is easier, so we focus only on the latter one. • ∑ j∈J [r j ] (H j +Y )) for some expressions G j and H j . Now: The case (2) is solved analogously.
The second case is shown trivially, too. ✷ Again, the transformations performed by the next theorem are basically identical to Milner's ideas: First, we collapse all strongly connected components (sets of states in which any two states may reach each other according to =⇒) into single states using R6. Finally, all τ-transitions looping in a state with probability 1 are removed by R5. Before stating the general proof, recall the example from before: The expression F is already probabilistically guarded, so consider E; the transformation is shown in Figure 7.

Theorem 3 For every expression E, there exists a guarded expression E
PROOF. To transform E into a guarded expression, we need to transform every recursion µX . F occurring as a subterm in E. We perform an induction over the nesting depth of the recursion µX . F to assert that there is some expression F ′ satisfying: (1) µX . F ′ is guarded, (2) no free, unguarded occurrence of a variable Y in F ′ lies within a recursion in F ′ , If there is no recursion occurring as a subterm of F, we may skip one paragraph by choosing F ′ ≡ F. Otherwise, we assume inductively that every top-level nested recursion µY. G yields some expression G ′ satisfying (1), (2) and (3). Here, a top-level recursion shall denote a recursion contained in F, but not contained in any recursion in between. By (3) and R1 we have µY.
Then obviously F = F ′ . Moreover, we observe that (2) is also satisfied. To see that, consider a free, unguarded occurrence of a variable Z in F ′ . Suppose that Z occurs within a recursion, i.e. within some term µY. G ′ , where µY. G ′ only occurs within some term G ′ {µY. G ′ /Y }. However, due to (1) we know that each occurrence of Y within G ′ is guarded, leading to the contradiction that every occurrence of Z within µY. G ′ within F ′ is guarded.
In both cases we find an expression F ′ = F satisfying (2). It remains to transform F ′ into an expression F ′′ that preserves (2) and additionally satisfies (1) and (3). If X only occurs guarded in F ′ , then we trivially choose F ′′ ≡ F ′ and conclude.
Thus, assume that X occurs unguarded in F ′ . We repeat the following steps, until each unguarded occurrence of X in F ′ is eliminated. Recall that none of these occurrences is contained within a recursion, due to (2).
If each unguarded occurrence of X does not lie within a prefix expression, then F ′ = X + F ′′ , where X does not occur unguarded in F ′′ . By R4, we are allowed to remove the X term, which establishes (3).
Each non-prefixed unguarded occurrence of X within some G i or H is eliminated as in the previous case. Note that the maximum nesting-depth of τ prefixes around X in all G i has decreased, so we inductively continue this transformation until the G i and H are free of unguarded X occurrences. Ultimately, it remains to apply R5 to get rid of the τ.∂ (X ) term; we conclude by taking F ′′ ≡ τ.(∑ i∈I G i + H). ✷

Equation systems
As already mentioned, equation systems (ESs) are an important ingredient of our completeness proof.
We prefer reasoning about ESs over plain expressions, because the former naturally express recursions in a standardised form. Formally, for variables X = (X 1 , . . . , X n ) and expressions S = (S 1 , . . . , S n ), let S : X = S denote an equation system with formal variables X. Sometimes we writeX to address the corresponding set {X 1 , . . . , X n }. All non-formal variables occurring in some expression S i are called free and we denote V(S ) as the set of all free variables in S . We say an ES S : X = S is satisfied by some expression E, if there exist expressions E = (E 1 , . . . , E n ) with E ≡ E 1 , such that E = S{ E/ X } according to our axioms.
Before we continue clarifying the intuition behind ESs, let us first introduce an important property, which we almost always presuppose: Definition 8 (Standardness) An equation system S : X = S with X = (X 1 , . . . , X n ) and S = (S 1 , . . . , S n ) is called standard if every expression S i has the shape Intuitively, just like expressions, we continue visualising standard equation systems (SESs) as PA: The formal variables may be interpreted as states and the transition relation according to our operational semantics. Note that this definition crucially depends on the standardness property; otherwise µ might support expressions not contained inX.
Example 6 Consider the expressions E and F from Example 4, after being transformed into guarded expressions. The following SES S (resp. T ) is satisfied by E (resp. F): Let us prove that F satisfies T , exemplary. Choose expressions F = (F 1 , . . . , There are some other important properties that we rely on later in this proof. We have already defined a strong transition relation α −→ S on SESs, let weak transitions =⇒ S and α =⇒ S be defined as before using derivations.

Definition 9 (Guardedness) A standard equation system
Definition 10 (Saturatedness) A standard equation system S : X = S is called saturated, if the following conditions hold: Note that both definitions essentially coincide with Milner's versions in the nonprobabilistic setting. However, asserting these properties when dealing with infinitary probabilistic weak transitions results in a substantial overhead in many of the following steps.
Hereinafter, it proves useful to introduce some handy notation: When considering some probability distribution µ overX, we sometimes write µ[ X] to clarify the domain of µ. Furthermore, we may write µ[ S] to cast µ to a distribution over the expressions in S, i.e. µ[ S] = {S j → µ(X j )}.

Equational characterisation
The completeness proof continues by transforming a given (guarded) expression E into an SES S satisfied by E. In fact, we construct S to be guarded and maintain this property until the very end of the completeness proof, where it becomes highly significant.
Although the general ideaà la Milner carries over easily, the details of proving S being guarded turn out to be quite complex.
Theorem 4 (Equational characterisation) Given some guarded expression E, there is a guarded SES S with free variables in V(E) satisfied by E.
PROOF. See Appendix B. ✷

Saturation
The next step of the completeness proof transforms the guarded SESs obtained by the previous section into saturated, guarded SESs. Milner's saturation proof proceeds essentially as follows: We simply shortcut along every weak transition of the ES until we reach saturatedness. Note that there are two implicit assumptions: There is only a finite number of different weak transitions and each weak transition is of finite length. Unfortunately, both assumptions fail in our context! We use infinitary probabilistic weak transitions defined by derivations, i.e. infinite sequences. Furthermore, the number of weak transitions is not guaranteed to be bounded: Consider the PA in Figure 3. There exist transitions s . ., more precisely: there exists a transition s Even worse: We already observed that weak transitions are convex, thus the amount of different weak transitions is uncountable.
We deal with these issues by strongly exploiting an important result of [3], originating from Markov Decision Theory [15]: Using this fact, the first infinity is solved: In every ES S : X = S, there is only a finite number of 'states' X i , and for each one Proposition 11 yields a finite number of interesting transitions. So all in all, there is only a finite number of weak transitions left that needs to be translated into strong transitions. We continue with another related result of [3]:
Here, a stationary policy Θ : S → D ≤1 (S) resolves the nondeterministic choice in each state of the PA by scheduling a target subdistribution, i.e. whenever Θ(s) = µ, then |µ| · δ (s) τ −→ µ. The non-assigned part of the subdistribution corresponds to stopping in the respective state. A weak transition ν =⇒ µ is derivable by some stationary policy Θ, denoted by ν =⇒ Θ µ, if 3

Transition trees
So now each transition to be considered is derivable by some stationary policy. The derivation might still be infinite. However, a certain degree of regularity is introduced, which we are going to exploit. To be properly prepared, we introduce a concept equivalent to derivations, namely transition trees. A derivation only yields information about the linear course of a transition, meaning that after every step, all target distributions are combined into one single distribution. A transition tree also keeps track of the branching structure, i.e. it assigns probabilities to all possible runs s 0 · · · s i ∈ S + .
Definition 11 (Transition Tree) A transition tree (TT) is a mapping ϑ : S * → D ≤1 (S) satisfying the following conditions, for all s 0 · · · s i ∈ S + : We will argue precisely about the correspondence between derivations and transition trees in the next proof (even though we only show one direction), before, we need some definitions: We refer to a node as a sequence s 0 · · · s i ∈ S + . ϑ (s 0 · · · s i )(s i+1 ) is interpreted as the probability of following a path with prefix s 0 · · · s i s i+1 in the weak transition and the probability of stopping right after reaching s i is given by ϑ (s 0 · · · s i−1 )(s i ) − |ϑ (s 0 · · · s i )|. This motivates the next term: The volume of some node s 0 · · · s i is defined as which expresses the target probability distribution of the transition induced by ϑ after following the sequence s 0 · · · s i through the PA. We say that ϑ starts from ϑ (ε) and leads to ∑ s 0 ∈S V ϑ (s 0 ), which we sometimes denote by ϑ (ε) =⇒ ϑ ∑ s 0 ∈S V ϑ (s 0 ). As already mentioned, transition trees in general are equipotent to derivations, so we are focusing on a restricted subclass, namely stationary transition trees: Definition 12 A transition tree ϑ is called stationary (STT) if for all nodes s 0 · · · s i and t 0 · · ·t j with ϑ (s 0 · · · s i−1 )(s i ) > 0, ϑ (t 0 · · ·t j−1 )(t j ) > 0 and s i = t j , .
So in a stationary transition tree ϑ , the volume of any node s 0 · · · s i only depends on s i , up to some scalar. This property now allows a finite representation of transition trees, as explained in the following. We call a node s 0 · · · s i pioneer if there is no state occurring more than once in the sequence s 0 · · · s i . Furthermore, we call s 0 · · · s i stopping if ϑ (s 0 · · · s i ) = / 0 and non-stopping otherwise. As an example, consider the automaton depicted in Figure 8a; think of a weak transition that stops in both s and t with probability 1 2 and halts in u certainly. Otherwise, in t, the combined transition leading to both s and u with probability 1 2 , respectively, is scheduled. That weak transition is induced exactly by the following stationary policy Θ: This transition may as well be drawn as an STT; Figure 8b shows every pioneer, non-stopping node (here each node is labelled only with its last state). The dashed connection leading from t back to s symbolises a recursion. Formally, the tree continues here infinitely long, however, the stationary property allows us to think of a recursive loop instead. It is easy to see that this correspondence between stationary policies and STTs holds in general:    Lemma 9 Whenever ν =⇒ µ, there is some transition tree ϑ , such that ν =⇒ ϑ µ. Furthermore, if ν =⇒ Θ µ is derivable by some stationary policy Θ, then ϑ is stationary.
We proceed by presenting two operations on STTs: shortcutting and linearising. Roughly speaking, shortcutting removes a node and connects its incoming and outgoing transitions appropriately, whereas linearising means removing a node's self-loop. After repeatedly applying these operations, we lastly achieve a TT of depth 1, which is (nearly) equivalent to a strong transition.
The authors of [6] have developed an algorithm to compute the minimal quotient PA with respect to ≈, which conceptually uses both procedures reversely: Instead of expanding the PA by adding transitions, the respective transitions are removed.
Technically, we perform an induction on the size of the transition tree, which is yet to be defined: On the one hand, whenever we shortcut a node, then the number of non-stopping pioneer nodes decreases. On the other hand, whenever a loop is linearised, the number of recursions is guaranteed to decrease. Therefore, the size |ϑ | of some stationary transition tree ϑ is defined as the sum of all non-stopping, pioneer states and all recursions. Formally, a pioneer node s 0 · · · s i recurs on some node s 0 · · · s j with j < i, if ϑ (s 0 · · · s i )(s j ) > 0.
Recall that we are concerned with weak transitions induced by ESs in this section. So whenever we perform one of the two operations, the underlying ES is transformed (only using the axioms), such that the modified STT remains derivable. Hence, given an SES S : X = S, we make sure that both operations return an SES T : X = T , which is augmented with respect to S , that is, T is satisfied by exactly all expressions satisfying S and meets the syntactical requirement T i ≡ S i + T ′ i for some expressions T ′ i . The last condition ensures that every strong transition in S occurs in T , too.

Shortcutting
This operation essentially extends the nonprobabilistic case; the infinitary property of weak transitions does not play a role, here. Nevertheless, we still give a detailed proof, as the technical skeleton introduced in this section requires careful treatment.
Lemma 10 (Shortcutting) Let S : X = S be a guarded SES and let µ =⇒ ϑ S ν for some STT ϑ . If there is a non-stopping, pioneer node · · · X i X j , such that there exists no node recurring in · · · X i X j , then there is some augmented guarded SES T : X = T with µ =⇒ ϑ ′ T ν for some STT ϑ ′ with |ϑ ′ | < |ϑ |.
PROOF. The key idea is to bypass the node · · · X i X j whenever it is possible. In detail, if there is a transition leaving · · · X i X j , we might as well combine this transition with the incoming transition to · · · X i X j , such that · · · X i X j is not visited in between. It remains possible that · · · X i X j is reachable with positive probability, however, then the TT stops here inevitably. The crucial modification of the underlying ES is justified by the axiom T3 (or T4, in fact both axioms are equivalent in this context, since we are only dealing with τ actions).
By ϑ being a transition tree, we infer that |ϑ (· · · X i )| > 0 and |ϑ (· · · X i X j )| > 0. Moreover, there are transitions Therefore, we conclude that the expressions S i and S j may be transformed to Note that (1) and (2) only imply combined transitions. Thus, beside the usual + axioms, it might have been necessary to apply the convexity axiom C.
We choose T : X = T as follows: This assignment of T i yields a transition which is required in the later part of the proof. First, we assert that any expression E satisfies S if and only if it satisfies T . So let E satisfy S , i.e. we gain expressions E, such that E = S{ E/ X}. For any So consider the interesting case: · · · · · · (I) m < k or t 0 · · ·t k = s 0 · · · s k (II) m = k and t 0 · · ·t k = s 0 · · · s k (III) m > k and t 0 · · ·t k = s 0 · · · s k and t k+1 = s k+1 (IV) m > k and t 0 · · ·t k = s 0 · · · s k and t k+1 = s k+1 Figure 9: Each sequence t 0 · · ·t m ∈X * is contained in a specially treated region of ϑ .
Recall that ϑ is a transition tree, thus it is guaranteed that ϑ (· · · X i )(X j ) ≥ |ϑ (· · · X i X j )|. This justifies the following expansion: So T is satisfied by some expression E if and only if S is satisfied by E. Moreover, the syntactical condition is clearly met, so T is in fact augmented with respect to S . Note that the only strong transition derivable in T , but not in S , (5), exists as a weak transition in S . So by some elementary reasoning about weak transitions, we find that the guardedness property holds on T as well. It remains to show, that there is some STT ϑ ′ smaller than ϑ and deriving µ =⇒ ϑ ′ T ν. Let s 0 · · · s k s k+1 denote the designated sequence from before, i.e. s k = X i and s k+1 = X j . We assign ϑ ′ (t 0 · · ·t m ) depending on the region in which t 0 · · ·t m is contained in ϑ . Figure 9 distinguishes the four cases: To visualise this construction, recall the example from before considering Figure 8. After shortcutting the node t in Figure 8b, we obtain the STT depicted in Figure 8c. t is originally reached with probability 1 3 and both s and u are reachable from t with probability 1 4 . Now, the shortcutting connects these transitions, such that both s and u become immediate successors of s with probability 1 3 · 1 4 = 1 12 , respectively; u is already reachable with probability 1 6 , so we end up with 1 6 + 1 12 = 1 4 . It is important to observe that t remains a successor of s with a positive probability of 1 6 . However, t itself has no successor any longer, which makes t stopping.
We continue by asserting that ϑ ′ is in fact a transition tree. So let t 0 · · ·t m ∈X + be some sequence and distinguish as before: The cases (I) and (IV) are trivial. If (II) arises, we make use of (5) to prove (ii). Moreover, it is easy to see that |ϑ ′ (s 0 · · · s k )| = |ϑ (s 0 · · · s k )|, thus (i) holds as well. So consider the case (III). (ii) is straightforward by ϑ being a transition tree. In order to show (i), we need to distinguish further between m = k + 1 and m > k + 1. The latter case is easy; the former case is solved by: It turns out to be exhausting, yet technically easy to prove that ϑ ′ is indeed stationary; we omit the details here. Moreover, we then find that ϑ ′ leads to ν, too.
We continue by showing that |ϑ ′ | < |ϑ |. It is easy to check that any recursion in ϑ ′ results from at least one recursion in ϑ , so the number of recursions is not increasing. However, there are fewer non-stopping pioneer nodes in ϑ ′ than in ϑ : For any non-stopping pioneer node t 0 · · ·t m in ϑ ′ , we find (at least) one corresponding non-stopping node in ϑ . If m ≤ k or t 0 · · ·t k = s 0 · · · s k , then we choose t 0 · · ·t m . Otherwise, if m > k and t 0 · · ·t k = s 0 · · · s k is non-stopping and pioneer in ϑ ′ , then so is s 0 · · · s k+1 t k+1 · · ·t m or t 0 · · ·t m in ϑ . Here comes into play that there exists no node recurring on s 0 · · · s k+1 in ϑ ; this assumption is necessary, since otherwise s 0 · · · s k+1 t k+1 · · ·t m might be non-stopping, but not pioneer. Note that this correspondence is injective and s 0 · · · s k+1 in ϑ finds no non-stopping partner in ϑ ′ . Hence, the number of non-stopping pioneer nodes in ϑ ′ is strictly smaller in comparison to ϑ . ✷

Linearising
The next operation seems far more interesting in our context: Intuitively, we unroll transitions that partially loop back to their origin state until reaching their 'limit transitions'; clearly, this problem emerges not before considering probabilistic finite-state systems. The infinitary nature of weak transitions, captured by R3, does the trick here.
Lemma 11 (Linearising) Let S : X = S be a guarded SES and let µ =⇒ ϑ S ν for some STT ϑ . If there is a pioneer node · · · X i with ϑ (· · · X i )(X i ) > 0, then there is some augmented guarded SES T : PROOF. There are two possible cases: Either there is another variable X j = X i with ϑ (· · · X i )(X j ) > 0, or there is not. The latter case represents X i stopping with a certain probability and self-looping, otherwise. We easily find an STT ϑ ′ that immediately stops once reaching X i . So let us focus on the first case. ϑ is a TT, so we have Importantly, this implies ϑ (· · · X i )(X i ) < |ϑ (· · · X i )| ≤ ϑ (· · · )(X i ), since there would exist a weak transition δ (X i ) τ =⇒ S δ (X i ) otherwise, but S is guarded. We continue transforming the underlying ES, such that possibly using C. Now assign T as follows: Note that T derives a strong transition which is going to be important when reducing the STT. We show that S and T are satisfied by the same Moreover: Notice that E i satisfies the equation with variable X i . We are certain that X i occurs guarded in S i {E k /X k | k = i}, since S is guarded, and obviously, the right-hand side of the + operator guards X i as well. Hence, by R2, infer: Evidently, T is augmented with respect to S . Similar to the proof of Lemma 10, the ES T is guarded; there is only one strong transition existing in T exclusively, (8), which exists in S as a weak transition, nevertheless.
It remains to construct ϑ ′ as desired. Let s 0 · · · s k denote the designated sequence from before, such that s k = X i and let s k+1 = X i , too. Consider Figure 9 again, which illustrates the cases we distinguish; ϑ ′ is designed following the key idea, namely not revisiting X i , after X i is reached once: Again, the construction is illustrated by Figure 8: After linearising s, as depicted in Figure 8d, the selfloop has been removed, i.e. the probability of reaching s multiple times is set to 0. The probabilities of all branches descending from s are scaled by λ = 1 1−1/12 = 12 11 . It is easy to prove that ϑ ′ is a TT. The cases (I) and (IV) are trivial. In the case (II), (i) follows after observing that |ϑ ′ (s 0 · · · s k )| = |ϑ (s 0 · · · s k )|. (ii) exploits the transition freshly introduced by T , (8). So focus on the remaining case (III): most properties are immediate by ϑ satisfying the properties of a TT. The only interesting case obtains if m = k + 1, and we would like to prove (i): Besides, it is not hard to prove that ϑ ′ is stationary.
There is one last part missing: We are still required to show that indeed |ϑ ′ | < |ϑ |. Clearly, any node is non-stopping and pioneer in ϑ ′ if and only if it is in ϑ . The number of recursions, however, has decreased: The recursion leading from s 0 · · · s k to itself does not exist in ϑ ′ anymore. The existence of any other recursion remains untouched (although the actual probabilities may have been scaled). ✷ We finally gathered all necessary preparations; all parts are assembled in the proof of the next theorem:

Theorem 5 (Saturation) Let S be a guarded SES satisfied by some expression E. Then there is a guarded, saturated SES T satisfied by E.
PROOF. We begin proving the first condition of Definition 10. Let S : X = S; repeat the following transformations for every X k and for every action α occurring as a prefix in S . By Proposition 11, we only need to consider a finite number of weak transitions δ (X k ) = µ =⇒ γ α −→ η =⇒ ν, and, by Proposition 12, µ =⇒ γ (and η =⇒ ν analogously) is a convex combination of weak transitions µ =⇒ Θ i γ i generated by stationary schedulers Θ i . Fix some i, Lemma 9 translates the respective transition into a STT µ =⇒ ϑ γ. Now perform an induction on the size of ϑ : If |ϑ | > 1, pick an arbitrary pioneer node s 0 · · · s j , such that any non-stopping continuation of s 0 · · · s j is no longer pioneer; one might think of s 0 · · · s j as a leaf in the finite tree representation. Now distinguish: First, assume that there is a node recurring on s 0 · · · s j . Then, by the choice of s 0 · · · s j , that node must be s 0 · · · s j s j , so we can linearise. Formally, apply Lemma 11 to obtain an augmented ES and a smaller STT, and conclude by induction. Otherwise, if there is no node recurring on s 0 · · · s j , observe that j ≥ 1 since |ϑ | > 1, so we exactly meet the requirements of Lemma 10 and shortcut instead.
If |ϑ | ≤ 1, then the only non-stopping node in ϑ (if there is any) is the root. So simply by the definition of a TT, there are transitions a a, b Figure 10: The SES T becomes saturated step-by-step.
for µ ′ , η ′ with µ ′ ≤ µ, µ ′ ≤ γ, η ′ ≤ η and η ′ ≤ ν. Additionally, recall that γ α −→ η, so by a very similar argumentation as in Lemma 10, we can shortcut these transitions using both laws T3 and T4 once (here, the full generality of T4 is exploited). The result is a guarded SES S ′ , which is augmented with respect to S and yields µ α −→ S ′ ν. It remains to establish Definition 10 (ii), so suppose there was some transition δ (X i ) =⇒ µ, where S j ✄ V for all j with and µ(X j ) > 0, but S i ✄ V . Now apply the same procedure as before: δ (X i ) =⇒ µ is decomposed into several weak transitions that result into STTs; then shortcut and/or linearise until S i ✄ V . Although the linearising method remains as it is, using R3, the shortcutting is modified to rely on T2 instead of T3. ✷ As the proof of Theorem 5 might seem hard to visualise, we demonstrate the transformations exemplary: . Then, we add the missing τ and α transitions by shortcutting. (See Figure 10.)

Joining equation systems
We achieve the next milestone by creating an SES U satisfied by both E and F. To this end, we finally take into account that E ≃ F. However, as we are not dealing with expressions anymore, we are required to find a similar correspondence on the level of SESs. Therefore, in the original proof, Milner assumed (a nonprobabilistic version of) the following proposition: "Let E = (E 1 , . . . , E n ) satisfy S : X = S. Whenever E i α =⇒ µ, then X i α =⇒ S ν[ X] and µ ≈ ν[ S]". A formal proof may for instance be found in [12]. Certainly, this statement holds in our probabilistic setting as well. Still, it turns out to be hard to show. So instead, let us simplify: We assume an even stronger statement: Obviously, this statement does not hold for arbitrary expressions E, so we call a solution E perfect if expressions E exist as desired. Intuitively, the PA induced by S and by a perfect solution E of S are isomorphic, i.e. identical up to renaming of states. Theorem 6, illustrated in Figure 11, assumes perfect solutions E and F, whose existence will be justified by the next section.
Theorem 6 Let S (resp. T ) be a guarded, saturated SES with perfect solution E (resp. F) and let E ≃ F. Then there is a guarded SES U satisfied by both E and F. Figure 11: Depicts the SESs S and T after being saturated on the left; the dashed regions designate the equivalence classes induced by ≈. The right PA shows the SES U constructed as in Theorem 6. For the sake of readability, we omit all quantities and all transitions leading from Z 1,1 , Z 1,2 , Z 2,1 and Z 2,2 to Z 4,4 , labelled with a or b.
PROOF. Let S : X = S and T : Y = T . Since E (resp. F) satisfies S (resp. T ), there are expressions We begin by proving the following implications for all E i ≈ F j : , then one of the following cases holds: , then one of the following cases holds: Focus on (1) first, (2) can be shown analogously. Suppose that X i By S i { E/ X } ≃ E i due to soundness and E i ≈ F j , we conclude that F jα =⇒ ν with ν ≈ µ[ E]. Since F is a perfect solution of T , we know that ν is a distribution only over expressions inF, write ν[ F]. Moreover, there is a transition Y jα =⇒ ν[ Y ]. Finally, distinguish two cases: If α = τ or there is a transition Y j τ =⇒ ν[ Y ], then we have shown (1)(b), by T being saturated. So suppose that α = τ and there is no . Then, by Proposition 7, Y j idles with some probability p > 0 and there is a transi- . Again, after exploiting the saturatedness of T , we end up with (1)(a).
(3) is straightforward by S and T being standard and E i ≈ F j . If we restrict E i and F j further to be weakly congruent, E i ≃ F j , then we find stricter implications following an analogous argumentation: Both cases (1)(a) and (2)(a) must not occur, since weak congruence is more restrictive by requiring τ transitions to not be simulated by idling.
It suffices to show that E satisfies U ; the same can be shown analogously for F. For (i, j) ∈ I, we distinguish the following two (exhaustive and mutually exclusive) cases: where X is a fresh variable and H i, j contains a summand that cannot be matched by X i as described in (2)(b), but only as in (2)(a). Every case p = 1 may be treated as an expression τ.∂ (X ) here, nevertheless, we omit these corner cases for the sake of simplicity. Next, we assert that for all q and P. The statement is trivial if (i) holds for (i, j), so assume (ii). Consider the equation posed by τ.∂ (E i + H i, j ) in which X is guarded. We show that τ.∂ (µX . (E i + H i, j )) yields a solution: . . . · · · α τ Figure 12: Conceptual procedure of transforming a transition to not target its origin state anymore.
Recall that each distribution µ is the target of some transition (1 − p) · δ (X i ) τ −→ S µ, so by convexity, idempotence of + and E i = S i { E/ S}: Finally, we obtain the desired equality: Figure 12 visualises abstractly how to understand the transformations above.
In order to show that E satisfies U , it suffices to show that E ≡ E 1 ≡ G 1,1 and G = U{ G/ Z}. The former requirement is easy: Recall that E 1 ≃ F 1 implies (2)(b), so we have (i) and by definition E 1 ≡ G 1,1 . Next, fix some pair (i, j) ∈ I; it remains to check that indeed G i, j = U i, j { G/ Z}. We begin by assuming (i) for (i, j), then the shape of U i, j simplifies to Note that the first, second and last row characterise exactly S i { E/ X}. The third row is eliminated by convexity and idempotence, again.
Now consider the case (ii). In contrast to before, U i, j features summands resulting from some transi- , for which (2)(a) holds, but (2)(b) does not. After applying the same transformations as before: and only (2)(a)} (9) So both E and F satisfy the SES U . Clearly U is standard, however, it takes some effort to prove that U is guarded. For a subdistribution µ[ Z], let µ[ X ] denote the projection of µ on X, i.e. µ[ X ] ≡ {X k → ∑ ℓ:(k,ℓ)∈I µ(Z k,ℓ )} and analogously for µ[ Y ]. It is now easy to check that each non- The sequence (γ → j , γ × j ) j∈AE is constructed as: Now, by Proposition 8 it suffices to assert γ → j =⇒ S γ j+1 for all j. The base case j = 0 is solved by (10).
so we have Finally, given (12) and (13), there is a transition: which contradicts S being guarded. ✷ There is one additional remark worth mentioning: The proof of Theorem 6 applies the axiom R5, which originally served only the purpose of reducing from arbitrary to probabilistically guarded expressions! Consequently, our guardedness notion turns out to be too weak in this context; in fact, one could wish for an additional condition preventing certain non-initial τ transitions. For the sake of convenience, we have not introduced such a condition, as it doubtlessly leads to a considerable overhead of checking additional properties in each step of the completeness proof. Nevertheless, note that probabilistic guardedness still proves itself necessary altogether, as it suffices to guarantee a unique solution of equations up to ≃ and results in a simple version of R2.

Unique solution of equations
The last step of the completeness proof asserts the existence and uniqueness of equation's solutions: For every SES S , there exists a solution E of S , and, provided that S is guarded, any expression F satisfying S , too, is provably equal to E: E = F.
In the case of a single equation, both properties are guaranteed by the laws R1 and R2, respectively; the general case follows by an easy inductive argument. The additional requirement that E be a perfect solution of S only seemingly leads to complications: In fact, the original proof [14] already constructs a perfect solution, without explicitly mentioning it.

Assembling all parts
We are finally ready to obtain the completeness theorem! The proof follows the preceding sections exactly, without bringing up any surprises.
PROOF. By Theorem 3, assume that both E and F are guarded. Next, by Theorem 4 and Theorem 5, we obtain guarded, saturated SESs S and T , satisfied by E and F, respectively. Theorem 7 finds a perfect solution E ′ = E (resp. F ′ = F) of S (resp. T ), which satisfies the joint guarded SES U , given by Theorem 6. Finally, Theorem 7 yields E = E ′ = F ′ = F. ✷

Conclusion and further work
In this paper, we established a sound and complete axiomatisation of infinitary probabilistic weak bisimilarity -a conservative extension of the nonprobabilistic setting. It turned out that allowing infinitary transitions is not only desirable from a modelling perspective, as randomised and deterministic implementations of the same problem should usually be indistinguishable, but also enables sound and complete axioms even (or especially) in the presence of unguarded recursion. The main difficulty was obviously given by the completeness proof. Although most transformations followed Milner's steps, asserting properties like guardedness of ESs led to a tremendous overhead, since weak transitions =⇒ were here defined as infinite sequences.
We are confident that this approach carries over nicely to the other points in the branching time spectrum [10]. Further work might address for instance the development of an axiomatisation of branching bisimilarity as an extension of [9] or focus on the interesting connection of infinitary and divergencesensitive semantics [12].
Moreover, we only considered finite-state systems, so follow-up work could study the consequences of adding parallel composition and restriction operators.

A Soundness of R2
Recall that R2 guarantees that, for expressions E and G, whenever G = E{G/X }, in which case we say that G is a solution of the equation E in variable X , then G = µX . E, provided that X is probabilistically For H a potentially different solution of E, we must have that G = µX . E = H, therefore, R2 expresses an interesting property of = and ≃ consequently, namely that any equation E has a unique solution up to ≃.
However, note that the premise that X be probabilistically guarded in E cannot be omitted. It might be helpful to understand the following counterexample: turn out to be solutions of E. Yet, clearly G ≃ H, since H contains the action b, which does neither occur in G, nor in E. So how is this possible? Intuitively, E not guarding X yields a weak transition reaching X with full probability 1. Hence, the alien action b sneaking into the left-hand side of the equation may now be simulated by some transition b =⇒ of the right-hand side, although b does not occur in E, originally. Fortunately, any expression E guarding X prevents this effect.
Before we prove that every guarded equation has a unique solution, we need to gather some additional results related to weak transitions and guardedness.
Definition 13 (Strong guardedness) A free variable X is said to occur strongly unguarded in E if E ◮ X according to Table 5.
PROOF. A straightforward induction on the derivation of E ◮ X from the rules of Table 5, using the rules of Table 1. ✷ Corollary 2 If π ◮ X and |π| · δ (G) (2) for each E ∈ ⌈π⌉ there is an X ∈ V with E ◮ X . A term F is a +-resolution of a term E if F is obtained from E by recursively replacing each subterm E 1 + E 2 of E by either E 1 or E 2 . Thus, a +-resolution is +-free and hence has at most one outgoing transition (to a +-free distribution).
Lemma 13 E ✄ V iff F =⇒ π for some +-resolution F of E and a distribution π ∈ D =1 (E) with π ◮ V .

PROOF. A straightforward induction on E. ✷
Corollary 3 E ✄ X iff F =⇒ π for some +-resolution F of E and a distribution π ∈ D =1 (E) with π ◮ X .

Lemma 14
For each E ∈ E with E ✄ X there exists a p E > 0 such that if E =⇒ p · π 1 + (1−p) · π 2 with π i ∈ D =1 (E) and π 2 ◮ X then p ≥ p E .
PROOF. Let E ∈ E be such that there is no such p E > 0. As there are only finitely many states reachable from E, the distributions reachable from E can be seen as points in a finite-dimensional Euclidean space. According to [3] the set Π := {π ∈ D =1 (E) | E =⇒ π} is compact (i.e. bounded and topologically closed). Now consider an infinite sequence (µ i ) i∈AE in Π where µ i has the form p · π 1 + (1−p) · π 2 with π 2 ◮ X and p < 1 i . Since each infinite sequence in a compact space has a convergent subsequence, which has a limit within that space, there must be a distribution µ ∈ Π with µ ◮ X . This contradicts Corollary 4. ✷ In the following statements E, F, G, H ∈ E and µ, ν, π, γ ∈ D ≤1 (E). Moreover, we assume G, H, µ, ν to be closed, while E, F, π and γ are allowed to contain only the free variable X .
The next lemma says that a transition from π{G/X } can always be decomposed in a part that stems from π and a part originating from G.
Using this, as well as Lemma 12 (or Corollary 2 with α −→ instead of α =⇒), "if" (i.e. the implication from right to left) follows immediately from the convex lifting of −→ to a relation between subdistributions.

B Equational characterisation
To be prepared properly, we first establish some useful foundations: Definition 14 (Cut) Let S , T be equation systems over the formal variables X. A weak transition µ =⇒ T π + γ is called a cut through µ =⇒ S ν, if the following conditions are satisfied: The formal definition might seem deterrent, however, the intuition behind cuts is easily explained: Let µ =⇒ S ν; now try to mimic this transition in T . In general this is not possible, since we could reach points γ i where the original transition continues with γ i τ −→ S γ ′ i , but γ i τ −→ T γ ′ i does not hold. At these points, we simply stop. The remaining transition is of the shape µ =⇒ T π + γ, where π is the remainder of ν that could actually be reached in T and γ is the sum of all cut points. Intuitively, it is clear that there is a cut through any transition µ =⇒ S ν. Nevertheless, a precise proof is not obvious, due to the demanding specification given in Definition 14.
such that µ ≡ µ 0 ≡ µ → 0 + µ × 0 and ∑ i∈AE µ × i ≡ ν. We construct a sequence (ν → i , ν × i + γ i ) i∈AE as follows: In each step, using ( * ), we cut off a maximal branch γ i that is not derivable in T ; this branch stops in the new derivation. We are going to define ν → i , ν × i , γ i and the auxiliary values η i recursively, as shown in the following diagram; the dashed connections represent transitions that are not (even partially) derivable in T .
For the base case, let η 1 ≡ µ 1 . We instantiate (14) to obtain Then, we define where we split (15) by ( * ) into where the second transition is not (even partially) derivable in T . So let i > 0 and assume that all values are defined up to i − 1. Observe that γ ′ i−1 ≤ η i ≤ µ i , thus, by some basic reasoning about subprobability distributions, there is a split γ ′ i−1 ≡ γ ′→ i−1 + γ ′× i−1 and η i ≡ 0 + ν × 0 + γ 0 , hence, in order to prove (20), it suffices to show that (ν → i , ν × i + γ i ) i∈AE is a derivation. This result is straightforward: For all i, we obtain by (16) and (19). We continue by proving that (20) is indeed a cut; each desired property of Definition 14 is considered separately: (i) is easily shown by both (ii) and (iii) are immediate by (16) and (19). Proving (iv) requires a little more effort. First, we need to assert µ =⇒ S π + γ ′ .
PROOF. We strengthen the statement by additionally asserting the following property for all V ⊂ V: ( §) If E ✄ V , then there exists no µ, such that X 1 =⇒ S µ and each X ∈ V occurs in some expression supported by µ[ S].
Here, S : X = S. The statement is proven by an induction on the structure of E. Sometimes, we write S ∪ T to denote the union of two ESs S , T ; the result is an ES containing every equation either occurring in S or in T .
We inductively obtain SESs S i with leading equations X i,1 = S i,1 , satisfied by S is obviously standard, both the guardedness property and ( §) follow by induction.
E ≡ F + G: We obtain SESs T and U with leading equations Y 1 = T 1 and Z 1 = U 1 , satisfied by F and G, respectively. We construct S = {X 1 = T 1 +U 1 } ∪ T ∪ U with distinguished variable X 1 ; again, all properties follow easily by induction.
E ≡ µX . F: We find an SES T : X = T satisfied by F by induction. Since E is guarded, we infer that X is guarded in F. The variable X cannot occur in T 1 , due to ( §). We now construct S : X = S, where S = T {T 1 /X }; note that X does not occur in S anymore. By R1, we conclude that E provably satisfies S . Moreover, it is easy to see that S is standard; the other properties require more effort.
We may again apply Lemma 20 in order to obtain a cut 1 |γ ′ | · γ ′ =⇒ T (1 − |ν|) · δ (X k ) + ν (29) through (28) with cut points ν i , such that ν = ∑ i∈AE ν i ; again, we could immediately rewrite the remaining part of δ (X k ) as (1 − |ν|) · δ (X k ). Following the same argumentation as above, we observe that whenever X j ∈ ⌈ν i ⌉ for some i, then X occurs in T j . There is one last piece missing: Recall that each transition γ i τ −→ γ ′ i is derived by expressions T 1 substituting the variable X . Thus, there is also a transition We are now ready to construct the weak transition leading to a contradiction: The sequence (µ → i , µ × i ) i∈AE is constructed with Note that µ 0 ≡ µ → 0 + µ × 0 ≡ δ (X 1 ) and since |γ| > 0. By Proposition 8, it suffices to show that µ → i =⇒ µ i+1 ≡ µ → i+1 + µ × i+1 for all i in order to prove (31). The cases i = 0 and i = 1 follow from (30) and (29), respectively. All remaining cases i ≥ 2 are proven by (25) and linearity.
It still remains to point out how to cause a contradiction: Recall that both γ[ S] and ν[ S] support only expressions in which X occurs. Consequently, (ν + 1−|ν| |γ| · γ)[ S] fulfils this property, too. Additionally, we know that F ✄ δ (X ), thus, (31) contradicts ( §), which is guaranteed to hold for T by induction.
We continue by proving that ( §) holds for S , so let E ✄ V . Again, we prove the statement by contradiction: Suppose there is some transition such that each Y ∈ V is contained in an expression supported by µ[ S]. Observe that X ∈ V , as X does not occur in S , anymore. Besides, note that each Y ∈ V also occurs in some expression supported by µ[ T ], since every variable other than X occurs in S j if and only if it occurs in T j . We know there exists some cut δ (X 1 ) =⇒ T π + γ (33) through (32), where π ≤ µ and γ ≡ ∑ i∈AE γ i . Analogously to before, we find that each expression supported by γ[ T ] contains X . In addition to that, we may assume w.l.o.g. that each Y ∈ V occurs in some expression supported by π[ T ]. Suppose there was some Y contradicting this assumption. Then the branch reaching Y in the original transition (33) has been cut off, so we continue cutting the respective continuation until some expression containing Y is reached. Now, distinguish two cases: First, let |γ| = 1. Then δ (X 1 ) =⇒ T γ, where all expressions in the support of γ[ T ] contain X . Thus, ( §) entails F ✄ X , which contradicts E being guarded.

C Unique solution of equations
Up to this point, we exclusively considered standard ESs. This section's theorem destructures a given ES, such that we need to settle with a weaker property: An ES S : X = S is called semi-standard if, within every subexpression of an expression S j , a formal variable X i occurs only within subexpressions of the form α.(∂ (X i ) p ⊕ P). Thus, we still prohibit jumping between variables without taking transitions in between, however, we now permit nested prefixing and recursions in the defining expressions S. For some expression E, we define R(E) as the set of all expressions reachable from E with positive probability. Let S : X = S be a semi-standard ES. We define R(S ) to collect all expressions reachable from some S j 4 . Moreover, we define a transition relation −→ S ⊆ R(S ) × A × D =1 (R(S )) as follows: Note that this transition relation coincides with the earlier characterisation (Definition 8) if S is standard: Then R(S ) ⊆X , so the second case never occurs.
After defining α =⇒ S as usual, we finally generalise our understanding of guardedness: A semistandard ES S is called (probabilistically) guarded if there is no i, such that δ (X i ) τ =⇒ S δ (X i ).
Theorem 7 (Unique solution of equations up to =) Let S be a guarded SES. There is a perfect solution E of S with free variables in V(S ). Furthermore, if F satisfies S , then E = F.
PROOF. The theorem is proven by showing a stronger claim: Contrary to what is required above, we let S : X = S be not necessarily standard, but semi-standard. We wish to find expressions E = (E 1 , . . . , E n ), such that E = S{ E/ X }. However, we do not require E :≡ E 1 to be a perfect solution of S (after all, we have not introduced an adapted definition), but rather show the following property: Here, • denotes functional composition. Intuitively, ( * ) states that the PA induced by E and S , respectively, are isomorphic. In the case that S is standard, ( * ) implies that E is a perfect solution of S .
So let n > 1 and let S contain the equations X = S and X n = S n . We are now constructing expressions E i , such that: E = S{ E/ X , E n /X n }, E n = S n { E/ X , E n /X n }.
To obtain these, we define T ≡ S{µX n . S n /X n } at first. Consider the ES T : X = T containing n − 1 equations. One can easily check that T is semi-standard and for now, assume that T is guarded; we will show this fact later. Then, by induction, we obtain n − 1 expressions E, such that E = T { E/ X }. We continue by assigning E n ≡ µX n . S n { E/ X }. By using R1 and some straight-forward identities involving substitution, we conclude that ≡ S{µX n . S n /X n }{ E/ X } = S n {µX n . S n /X n }{ E/ X } ≡ S{µX n . S n { E/ X}/X n }{ E/ X} ≡ S n {µX n . S n { E/ X}/X n }{ E/ X} ≡ S{E n /X n }{ E/ X } ≡ S n {E n /X n }{ E/ X } ≡ S{ E/ X , E n /X n }, ≡ S n { E/ X , E n /X n }.
If G ≡ X n , then b ′ (X n ) ≡ µX n . S n . Obviously, µX n . S n If G ≡ X i for all i, then b ′ (G) ≡ G{µX n . S n /X n }. Since T is semi-standard, we conclude that the substitution does not introduce fresh transitions. Thus, G{µX n . S n /X n } α −→ T µ iff G α −→ S µ • b ′ . By induction, we obtain some b ′′ : R(T ) → R(E) satisfying ( * ). So we choose b as the composition b ′′ • b ′ , which clearly meets the condition ( * ). Moreover, the bijection b ′ entails that T is guarded: Suppose there was some transition δ (X i ) τ =⇒ T δ (X i ), then we could use b ′ to translate each participating strong transition into a strong transition in S . So we would find a transition δ (X i ) τ =⇒ S δ (X i ), which contradicts S being guarded.
Next, assume there are expressions F and F n satisfying S , i.e. F = S{ F/ X , F n /X n }, F n = S n { F/ X , F n /X n }.
Since S n { F/ X} guards X n and F n = S n { F/ X}{F n /X n }, R2 implies F n = µX n . S n { F/ X}. Moreover, we refine the n − 1 equations: F = S{F n /X n }{ F/ X } = S{µX n . S n /X n }{ F/ X }, such that F = T { F/ X}, i.e. F satisfies T . It follows that E = F, by induction. Lastly, we obtain the remaining equality: F n = µX n . S n { F/ X} = µX n . S n { E/ X } = E n . ✷