Probabilistic Thread Algebra

arXiv:1409.6873v3 [cs.LO] 22 Jul 2015

J.A. Bergstra and C.A. Middelburg
Informatics Institute, Faculty of Science, University of Amsterdam,
Science Park 904, 1098 XH Amsterdam, the Netherlands
J.A.Bergstra@uva.nl,C.A.Middelburg@uva.nl

Abstract. We add probabilistic features to basic thread algebra and
its extensions with thread-service interaction and strategic interleaving. Here, threads represent the behaviours produced by instruction sequences under execution and services represent the behaviours exhibited
by the components of execution environments of instruction sequences.
In a paper concerned with probabilistic instruction sequences, we proposed several kinds of probabilistic instructions and gave an informal
explanation for each of them. The probabilistic features added to the
extension of basic thread algebra with thread-service interaction make
it possible to give a formal explanation in terms of non-probabilistic instructions and probabilistic services. The probabilistic features added to
the extensions of basic thread algebra with strategic interleaving make
it possible to cover strategies corresponding to probabilistic scheduling
algorithms.
Keywords: basic thread algebra, probabilistic thread, probabilistic service, probabilistic interleaving strategy, probabilistic instruction.
1998 ACM Computing Classification: D.3.3, D.4.1, F.1.1, F.1.2.

1

Introduction

In [6], an approach to the semantics of programming languages was presented
which is based on the perspective that a program is in essence an instruction
sequence. The groundwork for the approach is formed by PGA (ProGram Algebra), an algebraic theory of single-pass instruction sequences, and BTA (Basic
Thread Algebra), an algebraic theory of mathematical objects that represent
the behaviours produced by instruction sequences under execution (for a comprehensive introduction to these algebraic theories, see [15]). To increase the
applicability of the approach, BTA was extended with thread-service interaction
in [16]. In the setting of BTA and its extension with thread-service interaction,
threads are mathematical objects that represent the behaviours produced by instruction sequences under execution and services are mathematical objects that
represent the behaviours exhibited by components of execution environments of
instruction sequences.
As a continuation of the work presented in [6,16], (a) the notion of an instruction sequence was subjected to systematic and precise analysis using the

groundwork laid earlier, (b) various issues, including issues relating to computability and complexity of computational problems, efficiency of algorithms,
and verification of programs, were rigorously investigated thinking in terms of
instruction sequences (for a comprehensive survey of a large part of the work referred to under (a) and (b), see [15]), and (c) the form of interleaving concurrency
that is relevant to the behaviours of multi-threaded programs under execution,
called strategic interleaving in the setting of BTA, was rigorously investigated
by means of extensions of BTA (see e.g. [8,9,10]).
In the course of the work referred to above under (b), we ran into the problem
that BTA and its extension with thread-service interaction do not allow issues
relating to probabilistic computation to be investigated thinking in terms of instruction sequences. In the course of the work referred to above under (c), we ran
into the problem that BTA also does not allow probabilistic strategic interleaving to be investigated by means of extensions of BTA. This paper concerns the
addition of features to BTA and its extensions with thread-service interaction
and strategic interleaving that will take away these limitations.
We consider it important to take probabilistic computation into account in
future investigations. The primary reasons for this are the following: (a) the existence of probabilistic algorithms that are highly efficient, possibly at the cost
of a probability of correctness less than one (e.g. primality testing, see [29]);
(b) the existence of probabilistic algorithms for which no deterministic counterparts exist (e.g. symmetry breaking, see [26]); (c) the gradually created evidence
for the hypothesis that it is relevant for a diversity of issues in computer science
and engineering to think in terms of instruction sequences. This constitutes the
basis of our motivation for the work presented in this paper.
In [12], we gave an enumeration of kinds of probabilistic instructions that
were chosen on the basis of direct intuitions and therefore not necessarily the
best kinds in any sense. We only gave an informal explanation for each of the
enumerated kinds because we considered it premature at the time to add probabilistic features to BTA that would make it possible to give a formal explanation.
We were doubtful whether the ad hoc addition of features to BTA was the right
way to go.
Later, we have found that the ramification of semantic options with the addition of probabilistic features to BTA is well surveyable because of (a) the
limitation of the scope to behaviours produced by instruction sequences under
execution and (b) the semantic constraints brought about by the informal explanations of the kinds of probabilistic instructions enumerated in [12] and the
desired elimination property of all but one kind. In the case of a general process
algebra, such as ACP [3], CCS [27] or CSP [24], the ramification becomes much
more complex, particularly because a limitation of the scope to behaviours of a
special kind is lacking. In this paper, we add probabilistic features to BTA and
an extension of BTA with thread-service interaction.
The probabilistic features added to the extension of BTA with thread-service
interaction make it possible to give a formal explanation for each of the kinds
of probabilistic instructions enumerated in [12] in terms of non-probabilistic in-

2

structions and probabilistic services. To demonstrate this, we add the kind of
probabilistic instructions that cannot be eliminated to PGLB (ProGramming
Language B), a program notation rooted in PGA and close to existing assembly languages, and give a formal definition of the behaviours produced by the
instruction sequences from the resulting program notation. We opted for PGLB
because in the past it has proved itself suitable for the investigation of various
issues. The added kind of probabilistic instructions allow probabilistic choices to
be made during the execution of instruction sequences.
In [8] and subsequent papers, we extended BTA with kinds of interleaving where interleaving takes place according to some deterministic interleaving
strategy. Interleaving strategies are abstractions of scheduling algorithms. Interleaving according to an interleaving strategy differs from arbitrary interleaving,
but it is what really happens in the case of multi-threading as found in programming languages such as Java [21] and C# [23]. The extension of BTA with a
probabilistic feature does not only allow of probabilistic services, but also allows
of probabilistic interleaving strategies. In this paper, we also generalize the extensions of BTA with specific kinds of deterministic strategic interleaving to an
extension for a large class of kinds of deterministic and probabilistic strategic interleaving. Thus, strategies corresponding to probabilistic scheduling algorithms
such as the lottery scheduling algorithm [33] are covered.
The main results of this paper are probabilistic versions of BTA and its extensions with thread-service interaction and strategic interleaving which pave the
way for (a) investigation of issues related to probabilistic computation thinking
in terms of instruction sequences and (b) investigation of probabilistic interleaving strategies.
In this paper, we take functions whose range is the carrier of a signed cancellation meadow as probability measures. In [18], meadows are proposed as
alternatives for fields with a purely equational axiomatization. A meadow is a
commutative ring with a multiplicative identity element and a total multiplicative inverse operation satisfying two equations which imply that the multiplicative inverse of zero is zero. A cancellation meadow is a field whose multiplicative
inverse operation is made total by imposing that the multiplicative inverse of
zero is zero, and a signed cancellation meadow is a cancellation meadow expanded with a signum operation. In [17], Kolmogorov’s probability axioms for
finitely additive probability spaces are rephrased for the case where probability measures are functions whose range is the carrier of a signed cancellation
meadow.
This paper is organized as follows. First, we review signed cancellation meadows (Section 2). Next, we add probabilistic features to BTA and an extension
of BTA with thread-service interaction (Sections 3 and 4). Then, we add a kind
of probabilistic instructions to PGLB (Section 5). Following this, we add probabilistic features to the extensions of BTA with strategic interleaving (Section 6).
Finally, we make some concluding remarks (Section 7).
It should be mentioned that BTA is introduced in [6] under the name BPPA
(Basic Polarized Process Algebra) and services are called state machines in [16].

3

2

Signed Cancellation Meadows

We will take functions whose range is the carrier of a signed cancellation meadow
as probability measures. Therefore, we review signed cancellation meadows in
this section.
In [18], meadows are proposed as alternatives for fields with a purely equational axiomatization. A meadow is a commutative ring with a multiplicative
identity element and a total multiplicative inverse operation satisfying two equations which imply that the multiplicative inverse of zero is zero. Thus, all meadows are total algebras and the class of all meadows is a variety. At the basis of
meadows lies the decision to make the multiplicative inverse operation total by
imposing that the multiplicative inverse of zero is zero. All fields in which the
multiplicative inverse of zero is zero, called zero-totalized fields, are meadows,
but not conversely.
A cancellation meadow is a meadow that satisfies the cancellation axiom
x 6= 0 ∧ x · y = x · z ⇒ y = z. The zero-totalized fields are exactly the cancellation meadows that satisfy in addition the separation axiom 0 6= 1. A paradigmatic example of cancellation meadows is the field of rational numbers with the
multiplicative inverse operation made total by imposing that the multiplicative
inverse of zero is zero (see e.g. [18]). An example of a meadow that is not a zerototalized field is the initial algebra of the equational axiomatization of meadows
(see e.g. [5]).
A signed cancellation meadow is a cancellation meadow expanded with a
signum operation. The usefulness of the signum operation lies in the fact that
the predicates < and ≤ can be defined using this operation (see below).
The signature of signed cancellation meadows consists of the following constants and operators: the constants 0 and 1, the binary addition operator + ,
the binary multiplication operator · , the unary additive inverse operator −, the
unary multiplicative inverse operator −1 , and the unary signum operator s.
Terms are built as usual. We use infix notation for the binary operators +
and · , prefix notation for the unary operator −, and postfix notation for the
unary operator −1 . We use the usual precedence convention to reduce the need
for parentheses. We introduce subtraction and division as abbreviations: t − t′
−1
abbreviates t + (−t′ ) and t/t′ abbreviates t · (t′ ).
The constants and operators from the signature of signed cancellation meadows are adopted from rational arithmetic, which gives an appropriate intuition
about these constants and operators.
Signed cancellation meadows are axiomatized by the equations in Tables 1
and 2 and the above-mentioned cancellation axiom. The axioms for the signum
operator stem from [4].
The predicates < and ≤ are defined in signed cancellation meadows as follows:
x < y ⇔ s(y − x) = 1 and x ≤ y ⇔ s(s(y − x)+ 1) = 1. Because s(s(y − x)+ 1) 6=
−1, we have 0 ≤ x ≤ 1 ⇔ s(s(x) + 1) · s(s(1 − x) + 1) = 1. We will use this
equivalence below to describe the set of probabilities.

4

Table 1. Axioms of a meadow
(x + y) + z = x + (y + z)

(x · y) · z = x · (y · z)

(x−1 )−1 = x

x+y =y+x

x·y =y·x

x · (x · x−1 ) = x

x+0=x

x·1 =x

x + (−x) = 0

x · (y + z) = x · y + x · z

Table 2. Additional axioms for the signum operator

3

s(x/x) = x/x

s(x−1 ) = s(x)

s(1 − x/x) = 1 − x/x

s(x · y) = s(x) · s(y)

s(−1) = −1

(1 −

s(x)−s(y)
s(x)−s(y) )

· (s(x + y) − s(x)) = 0

Probabilistic Basic Thread Algebra

In this section, we introduce prBTA (probabilistic Basic Thread Algebra), a
probabilistic version of BTA. The objects considered in BTA are called threads.
In BTA, a thread represents a behaviour which consists of performing actions
in a deterministic sequential fashion. Upon each action performed, a reply from
an execution environment determines how the thread proceeds. The possible
replies are the values t and f. In prBTA, a thread represents a behaviour which
consists of performing actions in a probabilistic sequential fashion. That is, performing actions may alternate with making internal choices according to discrete
probability distributions.
In the sequel, it is assumed that a fixed but arbitrary signed cancellation
meadow M has been given. We denote the carrier of M by M as well, and we
denote the interpretations of the constants and operators in M by the constants
and operators themselves. We write P for the set {π ∈ M | s(s(π) + 1) · s(s(1 −
π) + 1) = 1} of probabilities.
In prBTA, it is moreover assumed that a fixed but arbitrary set A of basic
actions, with tau 6∈ A, has been given. In addition, there is the special action tau.
Performing tau, which is considered performing an internal action, will always
lead to the reply t. We write Atau for A ∪ {tau} and refer to the members of Atau
as basic actions.
The algebraic theory prBTA has one sort: the sort T of threads. We make
this sort explicit to anticipate the need for many-sortedness later on. To build
terms of sort T, prBTA has the following constants and operators:
– the inaction constant D : → T;1
– the termination constant S : → T;
– for each a ∈ Atau , the binary postconditional composition operator E a D :
T × T → T;
1

In earlier work, the inaction constant is sometimes called the deadlock constant.

5

Table 3. Axioms of prBTA
x E tau D y = x E tau D x
x +π y = y +1−π x

T1
prA1

π
y) +π+ρ−π·ρ z prA2
x +π (y +ρ z) = (x + π+ρ−π·ρ

x +π x = x

prA3

x +1 y = x

prA4

– for each π ∈ P, the binary probabilistic composition operator +π :T×T →
T.
Terms of sort T are built as usual in the one-sorted case. We assume that there
are infinitely many variables of sort T, including x, y, z. We use infix notation for
postconditional composition and probabilistic composition. We introduce basic
action prefixing as an abbreviation: a ◦ t, where t is a prBTA term, abbreviates
t E a D t. We identify expressions of the form a ◦ t with the prBTA terms they
stand for.
The thread denoted by a closed term of the form t E a D t′ will first perform
a, and then proceed as the thread denoted by t if the reply from the execution
environment is t and proceed as the thread denoted by t′ if the reply from the
execution environment is f. The thread denoted by a closed term of the form
t +π t′ will behave like the thread denoted by t with probability π and like the
thread denoted by t′ with probability 1 − π. The thread denoted by S will do
no more than terminate and the thread denoted by D will become inactive. A
thread becomes inactive if no more basic actions are performed, but it does not
terminate.
The inaction constant, the termination constant and the postconditional
composition operators are adopted from BTA. Counterparts of the probabilistic
composition operators are found in most probabilistic process algebras that offer
probabilistic choices of the generative variety (see e.g. [2]).
The axioms of prBTA are given in Table 3. In this table, π and ρ stand for
arbitrary probabilities from P. Axiom T1 reflects that performing tau will always
lead to the reply t and axioms prA1–prA4 express that probabilistic composition
provides probabilistic choices of the generative variety (see [20]). From prA1 and
prA4, we can derive both x +0 (y +0 z) = z and (x +0 y) +0 z = z, and hence
also x +0 (y +0 z) = (x +0 y) +0 z. This last equation can be immediately derived
from prA2 as well because in meadows 0/0 = 0.
Axiom T1 is adopted from BTA. Counterparts of axioms prA1–prA3 are
found in most probabilistic process algebras that offer probabilistic choices of
the generative variety (see e.g. [2]). However, in the process algebras concerned
the probabilities 0 and 1 are excluded in probabilistic choices to prevent division
by zero. Owing to this exclusion, axiom prA4 is lacking in these process algebras.
Each closed prBTA term denotes a finite thread, i.e. a thread with a finite
upper bound to the number of basic actions that it can perform. Infinite threads,
6

Table 4. Axioms for the guarded recursion constants
hX|Ei = htX |Ei

if X = tX ∈ E RDP

E ⇒ X = hX|Ei if X ∈ V(E)

RSP

i.e. threads without a finite upper bound to the number of basic actions that
it can perform, can be described by guarded recursion. A guarded recursive
specification over prBTA is a set of recursion equations E = {X = tX | X ∈ V },
where V is a set of variables of sort T and each tX is a prBTA term in which only
variables from V occur and each occurrence of a variable in tX is in a subterm
of the form t E a D t′ . We write V(E) for the set of all variables that occur on
the left-hand side of an equation in E.
We are only interested in models of prBTA in which guarded recursive specifications have unique solutions. A model of prBTA in which guarded recursive
specifications have unique solutions is the projective limit model of prBTA. This
model is constructed along the same line as the projective limit model of BTA
presented in [15]. It is based on the view that two threads are identical if their
approximations up to any finite depth are identical. The approximation up to
depth n of a thread is obtained by cutting it off after it has performed n actions
if it has not yet terminated or become inactive.
We confine ourselves to the projective limit model of prBTA, which has an
initial model of prBTA as a submodel, for the interpretation of prBTA terms.
An outline of this model is given in Appendix A.1. In the sequel, we use the term
probabilistic thread or simply thread for the elements of the carrier of the model.
Regular threads, i.e. finite or infinite threads that can only be in a finite number
of states, can be defined by means of a finite guarded recursive specification.
We extend prBTA with guarded recursion by adding constants for solutions
of guarded recursive specifications and axioms concerning these additional constants. For each guarded recursive specification E and each X ∈ V(E), we add a
constant standing for the unique solution of E for X to the constants of prBTA.
The constant standing for the unique solution of E for X is denoted by hX|Ei.
Moreover, we use the following notation. Let t be a prBTA term and E be a
guarded recursive specification. Then we write ht|Ei for t with, for all X ∈ V(E),
all occurrences of X in t replaced by hX|Ei. We add the axioms for guarded recursion given in Table 4 to the axioms of prBTA. In this table, X, tX and E
stand for an arbitrary variable of sort T, an arbitrary prBTA term and an arbitrary guarded recursive specification, respectively. Side conditions are added to
restrict the variables, terms and guarded recursive specifications for which X,
tX and E stand.
The additional axioms for guarded recursion are known as the recursive definition principle (RDP) and the recursive specification principle (RSP). The
equations hX|Ei = htX |Ei for a fixed E express that the constants hX|Ei make
up a solution of E. The conditional equations E ⇒ X = hX|Ei express that
this solution is the only one.

7

Pn
≤ n and
i=k [πi ]ti with 1 ≤ kP
PnIn Section 6, we will use the notation
n
π
=
1
for
right-nested
probabilistic
composition.
The
term
i
i=k
i=k [πi ]ti
with 1 ≤ k ≤ n is defined by induction on n − k as follows:
Pn
if k = n ,
i=k [πi ]ti = tk
Pn
Pn
πi
[π
]t
=
t
+
(
[
]t
)
k
πk
i=k i i
i=k+1 1−πk i if k < n .
Pn
The thread denoted by i=k [πi ]ti will behave like the thread denoted by tk with
probability πk and . . . and like the thread denoted by tn with probability πn .

4

Interaction of Threads with Services

Services are objects that represent the behaviours exhibited by components of
execution environments of instruction sequences at a high level of abstraction.
A service is able to process certain methods. The processing of a method may
involve a change of the service. At completion of the processing of a method,
the service produces a reply value. Execution environments are considered to
provide a family of uniquely-named services. A thread may interact with the
named services from the service family provided by an execution environment.
That is, a thread may perform a basic action for the purpose of requesting a
named service to process a method and to return a reply value at completion of
the processing of the method. In this section, we extend prBTA with services,
service families, a composition operator for service families, an operator that is
concerned with this kind of interaction, and a general operator for abstraction
from the internal action tau.
In SFA, the algebraic theory of service families introduced below, it is assumed that a fixed but arbitrary set M of methods has been given. Moreover,
the following is assumed with respect to services:
– a signature ΣS has been given that includes the following sorts:
• the sort S of services;
• the sort B of Boolean values;
and the following constants and operators:
• the empty service constant δ : → S;
• the reply constants t, f : → B;
∂
: S → S;
• for each m ∈ M, the derived service operator ∂m
• for each m ∈ M and π ∈ P, the service reply operator ̺πm : S → B;
– a minimal ΣS -algebra S has been given in which the following holds:
• tV6= f;
V
∂
• Vm∈M ( ∂m
(s) = δ ⇔ π∈P ̺πm (s) = f);
• π,ρ∈P (̺πm (s) = t ∧ ̺ρm (s) = t ⇒ π = ρ).
The intuition concerning
process method m:

∂
∂m

and ̺πm is that on a request to service s to

– if ̺πm (s) = t, s processes m, produces the reply t with probability π and the
∂
reply f with probability 1 − π, and then proceeds as ∂m
(s);
8

Table 5. Axioms of SFA
u⊕∅= u

SFC1

u⊕v =v⊕u

SFC2

∂F (∅) = ∅
∂F (f.s) = ∅

SFE1
if f ∈ F

SFE2

(u ⊕ v) ⊕ w = u ⊕ (v ⊕ w) SFC3

∂F (f.s) = f.s if f ∈
/F

SFE3

f.s ⊕ f.s′ = f.δ

∂F (u ⊕ v) = ∂F (u) ⊕ ∂F (v) SFE4

SFC4

– if ̺πm (s) = f for each π ∈ P, s is not able to process method m and proceeds
as δ.
The empty service δ itself is unable to process any method. A service is fully
deterministic if, for all m, for all s, ̺πm (s) = t only if π ∈ {0, 1}.
The assumptions with respect to services made above are the ones made
before for the non-probabilistic case in e.g. [15] adapted to the probabilistic
case.
It is also assumed that a fixed but arbitrary set F of foci has been given.
Foci play the role of names of services in a service family.
SFA has the sorts, constants and operators from ΣS and in addition the sort
SF of service families and the following constant and operators:
–
–
–
–

the empty service family constant ∅ : → SF;
for each f ∈ F , the unary singleton service family operator f. : S → SF;
the binary service family composition operator ⊕ : SF × SF → SF;
for each F ⊆ F , the unary encapsulation operator ∂F : SF → SF.

We assume that there are infinitely many variables of sort S, including s, and
infinitely many variables of sort SF, including u, v, w. Terms are built as usual in
the many-sorted case (see e.g. [31,34]). We use prefix notation for the singleton
service family operators and infix notation for the service family composition
operator.
The service family denoted by ∅ is the empty service family. The service
family denoted by a closed term of the form f.t consists of one named service
only, the service concerned is the service denoted by t, and the name of this
service is f . The service family denoted by a closed term of the form t ⊕ t′
consists of all named services that belong to either the service family denoted
by t or the service family denoted by t′ . In the case where a named service from
the service family denoted by t and a named service from the service family
denoted by t′ have the same name, they collapse to an empty service with the
name concerned. The service family denoted by a closed term of the form ∂F (t)
consists of all named services with a name not in F that belong to the service
family denoted by t.
The axioms of SFA are given in Table 5. In this table, f stands for an arbitrary
focus from F and F stands for an arbitrary subset of F . These axioms simply
formalize the informal explanation given above.
The constants, operators, and axioms of SFA were presented for the first time
in [14].
9

Table 6. Axioms for the use operator
D/u=D

prU1

S/u=S

prU2

(tau ◦ x) / u = tau ◦ (x / u)

prU3

(x E f.m D y) / ∂{f }(u) = (x / ∂{f }(u)) E f.m D (y / ∂{f }(u))
(x E f.m D y) / (f.t ⊕ ∂{f }(u)) = tau ◦ ((x +π y) /
(x E f.m D y) / (f.t ⊕ ∂{f }(u)) = tau ◦ D

∂
t ⊕ ∂{f }(u)))
(f. ∂m
π
if ̺m (t) = t
V
if π∈P ̺πm (t) = f

(x +π y) / u = (x / u) +π (y / u)

prU4
prU5
prU6
prU7

Table 7. Axioms for the abstraction operator
τtau (S) = S

TA1

τtau (D) = D

TA2

τtau (tau ◦ x) = τtau (x)

TA3

τtau (x E f.m D y) = τtau (x) E f.m D τtau (y) TA4
τtau (x +π y) = τtau (x) +π τtau (y)

TA5

For the set A of basic actions, we now take {f.m | f ∈ F , m ∈ M}. Performing a basic action f.m is taken as making a request to the service named f to
process method m.
We combine prBTA with SFA and extend the combination with the following
operators:
– the binary use operator / : T × SF → T;
– the unary abstraction operator τtau : T → T;
and the axioms given in Tables 6 and 7, and call the resulting theory prTAtsi . In
these tables, f stands for an arbitrary focus from F , m stands for an arbitrary
method from M, π stands for an arbitrary probability from P, and t stands for
an arbitrary term of sort S. The axioms formalize the informal explanation given
below. We use infix notation for the use operator.
The thread denoted by a closed term of the form t / t′ is the thread that
results from processing the method of each basic action performed by the thread
denoted by t by the service with the focus of the basic action as its name in the
service family denoted by t′ each time that a service with the name in question
really exists and as long as the method concerned can be processed. In the case
that a service with the name in question does not really exist, the processing of
a method is simply skipped (axiom prU4). When the method of a basic action
performed by the thread can be processed by the named service, that service
changes in accordance with the method and the thread is affected as follows: the
basic action is turned into the internal action tau and then an internal choice is
made between the two ways to proceed according to the probabilities of the two
10

possible reply values in the case of the method concerned (axiom prU5). When
the method of a basic action performed by the thread cannot be processed by the
named service, inaction occurs after the basic action is turned into the internal
action tau (axiom prU6).
The thread denoted by a closed term of the form τtau (t) is the thread that
results from concealing the presence of the internal action tau in the thread
denoted by t.
The use operator and the abstraction operator are adopted from the extension of BTA with thread-service interaction presented before in [15]. With the
exception of axiom prU7, the axioms for the use operator are the ones given
before for the non-probabilistic case in [15] adapted to the probabilistic case.
With the exception of axiom TA5, the axioms for the abstraction operator are
adopted from the extension of BTA with thread-service interaction presented
in [15]. Axiom prU7 and TA5 are new.
The following theorem concerns the question whether the operators added to
prBTA in prTAtsi are well axiomatized by the equations given in Tables 6 and 7
in the sense that these equations allow the projective limit model of prBTA to
be expanded to a projective limit model of prTAtsi .
Theorem 1. The operators added to prBTA are well axiomatized, i.e.:
(a) for all closed prTAtsi terms t of sort T, there exists a closed prBTA term t′
such that t = t′ is derivable from the axioms of prTAtsi ;
(b) for all closed prBTA terms t and t′ , t = t′ is derivable from the axioms of
prBTA iff t = t′ is derivable from the axioms of prTAtsi ;
(c) for all closed prTAtsi terms t of sort T, closed prTAtsi terms t′ of sort SF
and n ∈ N, πn (t / t′ ) = πn (πn (t) / t′ ) is derivable from the axioms of prTAtsi
and the following axioms for the unary operators πn (which are explained
below):2
π0 (x) = D ,
πn+1 (D) = D ,

πn+1 (x E a D y) = πn (x) E a D πn (y) ,

πn+1 (S) = S ,

πn+1 (x +π y) = πn+1 (x) +π πn+1 (y) .

where n stands for an arbitrary natural number from N, a stands for an
arbitrary basic action from Atau , and π is an arbitrary probability from P;
(d) for all closed prTAtsi terms t of sort T and n ∈ N, there exists a k ∈ N such
that, for all m ∈ N with m ≥ k, πn (τtau (t)) = πn (τtau (πm (t))) is derivable
from the axioms of prTAtsi and the axioms for the operators πn introduced
in part (c).
Proof. Part (a) is easily proved by induction on the structure of t, and in the case
where t is of the form t1 / t2 and the case where t is of the form τtau (t1 ) by induction on the structure of t1 . In the subcase where t is of the form t′1 E a D t′1 / t2 ,
2

Holding on to the usual conventions leads to the double use of the symbol π: without
subscript it stands for a probability value and with subscript it stands for a projection
operator.

11

we need the easy to prove fact that, for each f ∈ F and closed term t of sort
SF, either t = ∂f (t) is derivable or there exists a closed term t′ of sort S such
that t = f.t′ ⊕ ∂f (t) is derivable.
In the case of part (b), the implication from left to right follows immediately
from the fact that the axioms of prBTA are included in the axioms of prTAtsi .
The implication from right to left is not difficult to see either. From the axioms of
prTAtsi that are not axioms of prBTA, only axioms prU1, prU2, prU6, TA1, and
TA2 may be applicable to a closed prBTA term t. If one of them is applicable,
then the application yields an equation t = t′ in which t′ is not a closed prBTA
term. Moreover, only the axiom whose application yielded t = t′ is applicable to
t′ , but now in the opposite direction. Hence, applications of axioms of prTAtsi
that are not axioms of prBTA do not yield additional equations.
By part (a), it is sufficient to prove parts (c) and (d) for all closed prBTA
terms t. Parts (c) and (d) are easily proved by induction on the structure of t,
and in each case by case distinction between n = 0 and n > 0. In the proof of
both parts, we repeatedly need the easy to prove fact that, for all closed prBTA
terms t and n ∈ N, πn (t) = πn (πn (t)) is derivable. In the proof of part (c), in
the case where t is of the form t1 E a D t2 , we need again the fact mentioned at
the end of the proof outline of part (a).
⊓
⊔
The unary operators πn are called projection operators. The thread denoted by
a closed term of the form πn (t) is the thread that differs from the thread denoted
by t in that it becomes inactive as soon as it has performed n actions.
By parts (a) and (b) of Theorem 1, we know that the carrier of the projective
limit model of prBTA can serve as the carrier of a projective limit model of
prTAtsi if it is possible to define on this carrier operations corresponding to
the added operators such that the added equations are satisfied. By parts (c)
and (d) of Theorem 1, we know that it is possible to do so. Thus, we know that
the projective limit model of prBTA can be expanded to a projective limit model
of prTAtsi .
The actual expansion goes along the same lines as in the non-probabilistic
case (see [15]). An outline of this expansion is given in Appendix A.2. Because
the depth of the approximations of a thread may decrease by abstraction, we do
not have that, for all n and t, πn (τtau (t)) = πn (τtau (πn (t))) is derivable. However,
it is sufficient that there exists a k ∈ N such that, for all m ∈ N with m ≥ k,
πn (τtau (t)) = πn (τtau (πm (t))) is derivable (see also [15]).

5

A Probabilistic Program Notation

In this section, we introduce the probabilistic program notation prPGLB (probabilistic PGLB). In [6], a hierarchy of program notations rooted in program
algebra is presented. One of the program notations that belong to this hierarchy is PGLB (ProGramming Language B). This program notation is close to
existing assembly languages and has relative jump instructions. The program
notation prPGLB is PGLB extended with probabilistic instructions that allow
probabilistic choices to be made during the execution of instruction sequences.
12

In prPGLB, it is assumed that a fixed but arbitrary non-empty finite set A of
basic instructions has been given. The intuition is that the execution of a basic
instruction in most instances modifies a state and in all instances produces a
reply at its completion. The possible replies are the values t and f, and the actual
reply is in most instances state-dependent. Therefore, successive executions of
the same basic instruction may produce different replies. The set A is the basis for
the set of all instructions that may appear in the instruction sequences considered
in prPGLB. These instructions are called primitive instructions.
The program notation prPGLB has the following primitive instructions:
–
–
–
–
–
–
–
–
–

for each a ∈ A, a plain basic instruction a;
for each a ∈ A, a positive test instruction +a;
for each a ∈ A, a negative test instruction −a;
for each π ∈ P, a plain random choice instruction %(π);
for each π ∈ P, a positive random choice instruction +%(π);
for each π ∈ P, a negative random choice instruction −%(π);
for each l ∈ N, a forward jump instruction #l;
for each l ∈ N, a backward jump instruction \#l;
a termination instruction !.

A prPGLB instruction sequence has the form u1 ; . . . ; uk , where u1 , . . . , uk are
primitive instructions of prPGLB.
On execution of a prPGLB instruction sequence, these primitive instructions
have the following effects:
– the effect of a positive test instruction +a is that basic instruction a is
executed and execution proceeds with the next primitive instruction if t
is produced and otherwise the next primitive instruction is skipped and
execution proceeds with the primitive instruction following the skipped one
– if there is no primitive instruction to proceed with, execution becomes
inactive;
– the effect of a negative test instruction −a is the same as the effect of +a,
but with the role of the value produced reversed;
– the effect of a plain basic instruction a is the same as the effect of +a, but
execution always proceeds as if t is produced;
– the effect of a positive random choice instruction +%(π) is that first t is
produced with probability π and f is produced with probability 1−π and then
execution proceeds with the next primitive instruction if t is produced and
otherwise the next primitive instruction is skipped and execution proceeds
with the primitive instruction following the skipped one – if there is no
primitive instruction to proceed with, execution becomes inactive;
– the effect of a negative random choice instruction −%(π) is the same as the
effect of +%(π), but with the role of the value produced reversed;
– the effect of a plain random choice instruction %(π) is the same as the effect
of +%(π), but execution always proceeds as if t is produced;
– the effect of a forward jump instruction #l is that execution proceeds with
the lth next primitive instruction – if l equals 0 or there is no primitive
instruction to proceed with, execution becomes inactive;
13

– the effect of a backward jump instruction \#l is that execution proceeds with
the lth previous primitive instruction – if l equals 0 or there is no primitive
instruction to proceed with, execution becomes inactive;
– the effect of the termination instruction ! is that execution terminates.
With the exception of the random choice instructions, the primitive instructions of prPGLB are adopted from PGLB. Counterparts of the random choice
instructions are especially found in probabilistic extensions of Dijkstra’s guarded
command language (see e.g. [22]).
In order to describe the behaviours produced by prPGLB instruction sequences on execution, we need a service that behaves as a random Boolean
generator. This service is able to process the following methods:
– for each π ∈ P, a get random Boolean method get(π).
For each π ∈ P, the method get(π) can be explained as follows: the service
produces the reply t with probability π and the reply f with probability 1 − π.
For the carrier of sort S, we take the set {RBG, δ}. For each m ∈ M and
∂
π ∈ P, we take the functions ∂m
and ̺πm such that:
∂
∂get(π) (RBG) = RBG
̺πget(π) (RBG) = t ,

,

∂
∂m (RBG) = δ
̺πm (RBG) = f

if m 6∈ {get(π) | π ∈ P} ,
if m 6= get(π) .

Moreover, we take the name RBG used above to denote the element of the
carrier of sort S that differs from δ for a constant of sort S. It is assumed that
get(π) ∈ M for each π ∈ P. It is also assumed that rbg ∈ F .
The behaviours produced by prPGLB instruction sequences on execution are
considered to be probabilistic threads, with the basic instructions taken as basic
actions. The thread extraction operation | | defines, for each prPGLB instruction sequence, the behaviour produced on its execution. The thread extraction
operation is defined by
|u1 ; . . . ; uk | = τtau (|1, u1 ; . . . ; uk | / rbg.RBG) ,
where | , | is defined by the equations given in Table 8 (for a ∈ A, π ∈ P, and
l, i ∈ N)3 and the rule that |i, u1 ; . . . ; uk | = D if ui is the beginning of an infinite
jump chain.4
If 1 ≤ i ≤ k, τtau (|i, u1 ; . . . ; uk | / rbg.RBG) can be read as the behaviour
produced by u1 ; . . . ; uk on execution if execution starts at the ith primitive
instruction. By default, execution starts at the first primitive instruction.
In [12], we proposed several kinds of probabilistic jump instructions (bounded
and unbounded, according to uniform probability distributions and geometric
probability distributions). The meaning of instruction sequences from extensions
of prPGLB with these kinds of probabilistic instructions can be given by a
translation to instruction sequences from prPGLB.
3

4

.
.
.
We write i −
j for the monus of i and j, i.e. i −
j = i − j if i ≥ j and i −
j = 0
otherwise.
This rule can be formalized, cf. [11].

14

Table 8. Defining equations for the thread extraction operation
|i, u1 ; . . . ; uk | = D

if ¬ 1 ≤ i ≤ k

|i, u1 ; . . . ; uk | = a ◦ |i + 1, u1 ; . . . ; uk |

if ui = a

|i, u1 ; . . . ; uk | = |i + 1, u1 ; . . . ; uk | E a D |i + 2, u1 ; . . . ; uk |

if ui = +a

|i, u1 ; . . . ; uk | = |i + 2, u1 ; . . . ; uk | E a D |i + 1, u1 ; . . . ; uk |

if ui = −a

|i, u1 ; . . . ; uk | = rbg.get(π) ◦ |i + 1, u1 ; . . . ; uk |

if ui = %(π)

|i, u1 ; . . . ; uk | = |i + 1, u1 ; . . . ; uk | E rbg.get(π) D |i + 2, u1 ; . . . ; uk | if ui = +%(π)
|i, u1 ; . . . ; uk | = |i + 2, u1 ; . . . ; uk | E rbg.get(π) D |i + 1, u1 ; . . . ; uk | if ui = −%(π)

6

|i, u1 ; . . . ; uk | = |i + l, u1 ; . . . ; uk |

if ui = #l

.
|i, u1 ; . . . ; uk | = |i −
l, u1 ; . . . ; uk |

if ui = \#l

|i, u1 ; . . . ; uk | = S

if ui = !

Probabilistic Strategic Interleaving of Threads

Multi-threading refers to the concurrent existence of several threads in a program under execution. It is the dominant form of concurrency provided by contemporary programming languages such as Java [21] and C# [23]. Theories of
concurrent processes such as ACP [3], CCS [27], and CSP [24] are based on arbitrary interleaving. In the case of multi-threading, more often than not some
interleaving strategy is used. We abandon the point of view that arbitrary interleaving is the most appropriate abstraction when dealing with multi-threading.
The following points illustrate why we find difficulty in taking that point of
view: (a) whether the interleaving of certain threads leads to inactiveness depends on the interleaving strategy used; (b) sometimes inactiveness occurs with
a particular interleaving strategy whereas arbitrary interleaving would not lead
to inactiveness, and vice versa. Demonstrations of (a) and (b) are given in [8]
and [7], respectively.
The probabilistic features of prBTA allow it to be extended with interleaving
strategies that correspond to probabilistic scheduling algorithms. In this section,
we take up the extension of prBTA with such probabilistic interleaving strategies.
The presented extension covers an arbitrary probabilistic interleaving strategy
that can be represented in the way that is explained below.
We write A′tau for Atau ∪ {nt, S, D} and we write H for (N1 × N1 )∗ .5 The
elements of H are called interleaving histories. The intuition concerning interleaving histories is as follows: if the jth pair of an interleaving history is (i, n),
then the ith thread got a turn in the jth interleaving step and after its turn
there were n threads to be interleaved.
With regard to interleaving of threads, it is assumed that the following has
been given:
– a set S;
5

We write N1 for the set {n ∈ N | n ≥ 1} of positive natural numbers.

15

– an indexed family of functions hσn in∈N1 where σn :H×S → ({1, . . . , n} → P)
for each n ∈ N1 ;
– an indexed family of functions hϑn in∈N1 where ϑn :H×S×{1, . . . , n}×A′tau →
S for each n ∈ N1 .
The elements of S are called control states, σn is called an abstract scheduler
(for n threads), and ϑn is called a control state transformer (for n threads). The
intuition concerning S, hσn in∈N1 , and hϑn in∈N1 is as follows:
– the control states from S encode data relevant to the interleaving strategy
(e.g., for each of the threads being interleaved, the set of all foci naming
services on which it currently keeps a lock);
– for each h ∈ H and s ∈ S, σn (h, s) is the probability distribution on n
threads that assigns to each of the threads the probability that it gets the
next turn after history h in state s;
– for each h ∈ H, s ∈ S, i ∈ {1, . . . , n}, and a ∈ A′tau , ϑn (h, s, i, a) is the
control state that arises after history h in state s on the ith thread doing a.
Thus, S, hσn in∈N1 , and hϑn in∈N1 provide a way to represent a probabilistic
interleaving strategy. The abstraction of a scheduler used here is essentially the
notion of a scheduler defined in [30].
We extend prBTA with the following operators:
– the ternary forking postconditional composition operator E nt( ) D : T ×
T × T → T;
– for each n ∈ N1 , h ∈ H, and s ∈ S, the n-ary strategic interleaving operator
knh,s :T × · · · × T → T;
– for each n, i ∈ N1 with i ≤ n, h ∈ H, and s ∈ S, the n-ary positional strategic
n,i
interleaving operator ⌋⌊h,s :T × · · · × T → T;
– the unary deadlock at termination operator SD : T → T;
and the axioms given in Table 9,6 and call the resulting theory prTAsi . In this
table, n and i stand for arbitrary numbers from N1 with i ≤ n, h stands for
an arbitrary interleaving history from H, s stands for an arbitrary control state
from S, a stands for an arbitrary basic action from Atau , and π stands for an
arbitrary probability from P.
The forking postconditional composition operator has the same shape as
the postconditional composition operators introduced in Section 3. Formally, no
basic action is involved in forking postconditional composition. However, for an
operational intuition, in t E nt(t′′ ) D t′ , nt(t′′ ) can be considered a thread forking
action. It represents the act of forking off thread t′′ . Like with real basic actions,
a reply is produced upon performing a thread forking action.
The thread denoted by a closed term of the form knh,s (t1 , . . . , tn ) is the thread
that results from interleaving of the n threads denoted by t1 , . . . , tn after history
6

We write h i for the empty sequence, d for the sequence having d as sole element,
and α y α′ for the concatenation of sequences α and α′ . We assume that the usual
identities, such as h i y α = α and (α y α′ ) y α′′ = α y (α′ y α′′ ), hold.

16

Table 9. Axioms for strategic interleaving
kn
h,s (x1 , . . . , xn ) =

Pn

i=1 [σn (h, s)(i)]

⌋⌊n,i
h,s (x1 , . . . , xn )

⌋⌊1,i
h,s (D) = D

prSI1
prSI2

⌋⌊n+1,i
(x1 , . . . , xi−1 , D, xi+1 , . . . , xn+1 ) =
h,s
SD (kn
hy(i,n),ϑn+1 (h,s,i,D) (x1 , . . . , xi−1 , xi+1 , . . . , xn+1 ))
1,i
⌋⌊h,s (S) = S
⌋⌊n+1,i
(x1 , . . . , xi−1 , S, xi+1 , . . . , xn+1 ) =
h,s
n
khy(i,n),ϑn+1 (h,s,i,S) (x1 , . . . , xi−1 , xi+1 , . . . , xn+1 )

prSI3
prSI4
prSI5

′
′′
⌋⌊n,i
h,s (x1 , . . . , xi−1 , xi E nt(x) D xi , xi+1 , . . . , xn ) =
′
tau ◦ kn+1
hy(i,n+1),ϑn (h,s,i,nt) (x1 , . . . , xi−1 , xi , xi+1 , . . . , xn , x)
n,i
′
′′
⌋⌊h,s (x1 , . . . , xi−1 , xi E a D xi , xi+1 , . . . , xn ) =
′
kn
hy(i,n),ϑn (h,s,i,a) (x1 , . . . , xi−1 , xi , xi+1 , . . . , xn )

prSI6

EaD
′′
kn
hy(i,n),ϑn (h,s,i,a) (x1 , . . . , xi−1 , xi , xi+1 , . . . , xn )
′
′′
⌋⌊n,i
h,s (x1 , . . . , xi−1 , xi +π xi , xi+1 , . . . , xn ) =

prSI7

′
⌋⌊n,i
h,s (x1 , . . . , xi−1 , xi , xi+1 , . . . , xn )

+π
′′
⌋⌊n,i
h,s (x1 , . . . , xi−1 , xi , xi+1 , . . . , xn )

prSI8

SD (D) = D

DT1

SD (S) = D

DT2

SD (x E nt(z) D y) = SD (x) E nt(SD (z)) D SD (y)

DT3

SD (x E a D y) = SD (x) E a D SD (y)

DT4

SD (x +π y) = SD (x) +π SD (y)

DT5

h in state s, according to the interleaving strategy represented by S, hσn in∈N1 ,
and hϑn in∈N1 . By the interleaving, a number of threads is turned into a single
thread. In this single thread, the internal action tau arises as a residue of each
thread forking action encountered. Moreover, the possibility that f is produced as
a reply upon performing a thread forking action is ignored. This reflects our focus
on the case where capacity problems with respect to thread forking never arise.
The positional strategic interleaving operators are auxiliary operators used
to axiomatize the strategic interleaving operators. The role of the positional
strategic interleaving operators in the axiomatization is similar to the role of
the left merge operator found in process algebra (see e.g. [3]). The deadlock at
termination operator is an auxiliary operator as well. It is used in axiom prSI3
to express that in the event of inactiveness of one thread, the whole become
inactive only after all other threads have terminated or become inactive. The
thread denoted by a closed term of the form SD (t) is the thread that results from
turning termination into inactiveness in the thread denoted by t.
17

The forking postconditional composition operator and the deadlock at termination operator are adopted from earlier extensions of BTA with strategic interleaving. The strategic interleaving operators and the positional strategic interleaving operators are not adopted from earlier extensions of BTA with strategic
interleaving. To our knowledge, no probabilistic process algebras with counterparts of these operators has been proposed until now. Axioms prSI1–prSI8 and
DT5 are new. Axioms DT1–DT4 are adopted from the extension of BTA with
strategic interleaving and thread forking presented in [13].
Consider the case where S is a singleton set, for each n ∈ N1 , σn is defined
by
σn (h i, s)(i) = 1
if i = 1 ,
σn (h i, s)(i) = 0

if i 6= 1 ,

σn (h y (j, n) , s)(i) = 1 if i = (j + 1) mod n ,
σn (h y (i, n) , s)(i) = 0 if i 6= (j + 1) mod n
and, ϑn is defined by
ϑn (h, s, i, a) = s .
In this case, the interleaving strategy corresponds to the round-robin scheduling
algorithm. This deterministic interleaving strategy is called cyclic interleaving in
our earlier work on interleaving strategies (see e.g. [8]). In the current setting, an
interleaving strategy is deterministic if, for all n, for all h, s, and i, σn (h, s)(i) ∈
{0, 1}. In the case that S and ϑn are as above, but σn is defined by
σn (h i, s)(i) = 1

if i = 1 ,

σn (h i, s)(i) = 0

if i 6= 1 ,

σn (h y (j, n) , s)(i) = 1/n if i ≤ n ,
σn (h y (i, n) , s)(i) = 0

if i > n ,

the interleaving strategy is a purely probabilistic one. The probability distribution used is a uniform distribution.
More advanced strategies can be obtained if the scheduling makes use of the
whole interleaving history and/or the control state. For example, the individual
lifetimes of the threads to be interleaved and their creation hierarchy can be
taken into account by making use of the whole interleaving history. Individual
properties of the threads to be interleaved that depend on the actions performed
by them can be taken into account by making use of the control state. By doing
so, interleaving strategies are obtained which, to a certain extent, can be affected
by the threads to be interleaved.
Henceforth, we will write prBTAnt for prBTA extended with the forking
postconditional composition operator. The projective limit model of prBTAnt is
constructed like the projective limit model of prBTA. An outline of the projective
limit model of prBTAnt is given in Appendix A.3.
The following theorem concerns the question whether the operators added
to prBTAnt are well axiomatized by the equations given in Table 9 in the sense
18

that these equations allow the projective limit model of prBTAnt to be expanded
to a projective limit model of prTAsi .
Theorem 2. The operators added to prBTAnt are well axiomatized, i.e.:
(a) for all closed prTAsi terms t, there exists a closed prBTAnt term t′ such that
t = t′ is derivable from the axioms of prTAsi ;
(b) for all closed prBTAnt terms t and t′ , t = t′ is derivable from the axioms of
prBTAnt iff t = t′ is derivable from the axioms of prTAsi ;
(c) for all m, i ∈ N1 with i ≤ m, h ∈ H, s ∈ S, closed prTAsi terms t1 ,
m
. . . , tm and n ∈ N, πn (km
h,s (t1 , . . . , tm )) = πn (kh,s (πn (t1 ), . . . , πn (tm ))) and
m,i
m,i
πn (⌋⌊h,s (t1 , . . . , tm )) = πn (⌋⌊h,s (πn (t1 ), . . . , πn (tm ))) are derivable from the
axioms of prTAsi , the axioms for the operators πn introduced in Theorem 1,
and the following axiom:
πn+1 (x E nt(z) D y) = πn+1 (x) E nt(πn+1 (z)) D πn+1 (y) ,
where n stands for an arbitrary natural number from N;
(d) for all closed prTAsi terms t and n ∈ N, πn (SD (t)) = πn (SD (πn (t))) is derivable from the axioms of prTAsi , the axioms for the operators πn introduced
in Theorem 1, and the axiom introduced in part (c).
Proof. Part (a) is straightforwardly proved by induction on the structure of t,
and then in the case where t is of the form ⌋⌊n,i
h,s (t1 , . . . , tn ) by induction on the
sum of the lengths of t1 , . . . , tn and case distinction on the structure of ti and in
the case where t is of the form SD (t1 ) by induction on the structure of t1 . The
n,i
proof of the case where t is of the form ⌋⌊h,s (t1 , . . . , tn ) reveals that occurrences
of the forking postconditional composition operator get eliminated if t is of that
form.
In the case of part (b), the implication from left to right follows immediately
from the fact that the axioms of prBTAnt are included in the axioms of prTAsi .
The implication from right to left is not difficult to see either. From the axioms
of prTAsi that are not axioms of prBTAnt , only axioms prSI2, prSI4, DT1, and
DT2 may be applicable to a closed prBTAnt term t. If one of them is applicable,
then the application yields an equation t = t′ in which t′ is not a closed prBTAnt
term. Moreover, only the axiom whose application yielded t = t′ is applicable
to t′ , but now in the opposite direction. Hence, applications of axioms of prTAsi
that are not axioms of prBTAnt do not yield additional equations.
By part (a), it is sufficient to prove part (c) for all closed prBTAnt terms
t1 , . . . , tm . The derivability of the second equation is straightforwardly proved
by induction on the sum of the lengths of t1 , . . . , tn and case distinction on the
structure of ti , and in each case by case distinction between n = 0 and n > 0.
The derivability of the first equation now follows immediately using the axioms
of the operators πn . In the proofs, we repeatedly need the easy to prove fact
that, for all closed prBTAnt terms t and n ∈ N, πn (t) = πn (πn (t)) is derivable.
By part (a), it is sufficient to prove part (d) for all closed prBTAnt terms t.
Part (d) is easily proved by induction on the structure of t, and in each case by
19

case distinction between n = 0 and n > 0. In the proof, we need again the fact
mentioned at the end of the proof outline of part (c).
⊓
⊔
By Theorem 2, we know that the projective limit model of prBTAnt can be
expanded to a projective limit model of prTAsi . An outline of this expansion is
given in Appendix A.3.

7

Concluding Remarks

We have added probabilistic features to BTA and its extensions with threadservice interaction and strategic interleaving. Thus, we have paved the way for
rigorous investigation of issues related to probabilistic computation thinking in
terms of instruction sequences and rigorous investigation of probabilistic interleaving strategies. As an example of the use of prTAtsi , the probabilistic version
of the extension of BTA with thread-service interaction, we have added the most
basic kind of probabilistic instructions proposed in [12] to a program notation
rooted in PGA and have given a formal definition of the behaviours produced by
the instruction sequences from the resulting program notation under excution
with the help of prTAtsi .
We enumerate neither the numerous issues relating to probabilistic computation in areas such as computability and complexity of computational problems, efficiency of algorithms, and verification of programs that could be investigated thinking in terms of instruction sequences nor the numerous probabilistic
scheduling algorithms that could be investigated in prTAsi , the probabilistic
generalization of the extensions of BTA with strategic interleaving.
However, we mention interesting options for future work that are of a different kind: (a) clarifying analyses of relevant probabilistic algorithms, such as
the Miller-Rabin probabilistic primality test [28], using probabilistic instruction
sequences or non-probabilistic instruction sequences and probabilistic services
and (b) explanations of relevant quantum algorithms, such as Shor’s integer factorization algorithm [32], by first giving a clarifying analysis using probabilistic
instruction sequences or non-probabilistic instruction sequences and probabilistic services and then showing how certain services involved in principle can be
realized very efficiently with quantum computing.
Moreover, we believe that the development of program notations for probabilistic computation is a useful preparation for the development of program
notations for quantum computation later on. The development of program notations for quantum computation that have their origins in instruction sequences
could constitute a valuable complement to other developments with respect to
quantum computation, which for the greater part boil down to mere adaptation
of earlier developments with respect to classical computation to the potentialities
of quantum physics (see e.g. [19]).
In fact, prBTA is a process algebra tailored to the behaviours produced by
probabilistic instruction sequences under execution. Because prBTA offers probabilistic choices of the generative variety (see [20]) and no non-deterministic

20

choices, it is most closely related to the probabilistic process algebra prBPA
presented in [2]. To our knowledge, thread-service interaction and strategic interleaving as found in prTAtsi and prTAsi are mechanisms for interaction and
concurrency that are quite different from those found in any theory or model of
processes. This leaves almost nothing to be said about related work.
The very limited extent of related work is due to two conscious choices: (a) the
limitation of the scope to behaviours produced by programs under execution and
(b) the limitation of the scope to the form of interleaving concurrency that is
relevant to the behaviours of multi-threaded programs under execution. However,
something unexpected remains to be mentioned as related work, to wit the work
on security of multi-threaded programs presented in [30]. Probabilistic strategic
interleaving as found in prTAsi is strongly inspired by the scheduler-dependent
semantics of a simple programming language with support for multi-threading
that we found in that paper.
It is noteworthy to mention something about the interpretation of prBTA,
prTAtsi , and prTAsi in a probabilistic version of a general process algebra such as
ACP, CCS or CSP. It is crucial that probabilistic choice of the generative variety,
non-deterministic choice, asynchronous parallel composition, abstraction from
internal actions, and recursion are covered by the process algebra used for the
purpose of interpretation. General process algebras that cover all this are rare. To
our knowledge, pACPτ [1] is the only one that has been elaborated in sufficient
depth. However, interpretation of prBTA, prTAtsi , and prTAsi in pACPτ seems
impossible to us. The presence of asynchronous parallel composition based on
arbitrary interleaving in pACPτ precludes the proper form of abstraction from
internal actions for interpretation of prBTA, prTAtsi , and prTAsi .
Acknowledgements
We thank two anonymous referees for carefully reading a preliminary version of
this paper and for suggesting improvements of the presentation of the paper.

A

Projective Limit Models

In this appendix, we outline the construction of projective limit models for
prBTA, prTAtsi , and prTAsi . In these model, which covers finite and infinite
threads, threads are represented by infinite sequences of finite approximations.
Guarded recursive specifications have unique solutions in these models. We denote the interpretations of constants and operators in the models by the constants and operators themselves.
A.1

Projective Limit Model of prBTA

We will write I(prBTA) for the initial model of prBTA and T (prBTA) for the
carrier of I(prBTA). T (prBTA) consists of the equivalence classes of closed

21

prBTA terms with respect to derivable equality. In other words, modulo derivable equality, T (prBTA) is the set of all closed prBTA terms. Henceforth, we
will identify closed prBTA terms with their equivalence class where elements of
T (prBTA) are concerned.
Each element of T (prBTA) represents a finite thread, i.e. a thread with a
finite upper bound to the number of actions that it can perform. Below, we will
construct a model that covers infinite threads as well. In preparation for that, we
define for all n a function that cuts off threads from T (prBTA) after n actions
have been performed.
For each n ∈ N, we define the projection function πn : T (prBTA) →
T (prBTA), inductively as follows:
π0 (t) = D ,
πn+1 (S) = S ,

πn+1 (t E a D t′ ) = πn (t) E a D πn (t′ ) ,

πn+1 (D) = D ,

πn+1 (t +π t′ ) = πn+1 (t) +π πn+1 (t′ ) .

For t ∈ T (prBTA), πn (t) is called the nth projection of t. It can be thought of
as an approximation of t. If πn (t) 6= t, then πn+1 (t) can be thought of as the
closest better approximation of t. If πn (t) = t, then πn+1 (t) = t as well. For all
n ∈ N, we will write T n (prBTA) for {πn (t) | t ∈ T (prBTA)}. Obviously, the
projection functions defined above satisfy the axioms for the projection operators
introduced in Theorem 1.
In the projective limit model, which covers both finite and infinite threads,
threads are represented by projective sequences, i.e. infinite sequences (tn )n∈N
of elements of T (prBTA) such that tn ∈ T n (prBTA) and tn = πn (tn+1 ) for all
n ∈ N. In other words, a projective sequence is a sequence of which successive
components are successive projections of the same thread. The idea is that any
infinite thread is fully characterized by the infinite sequence of all its finite
approximations. We will write T ∞ (prBTA) for the set of all projective sequences
over T (prBTA), i.e. the set
{(tn )n∈N |

V

n∈N (tn

∈ T n (prBTA) ∧ tn = πn (tn+1 ))} .

The projective limit model I ∞ (prBTA) of prBTA consists of the following:
– the set T ∞ (prBTA), the carrier of the projective limit model;
– an element of T ∞ (prBTA) for each constant of prBTA;
– an operation on T ∞ (prBTA) for each operator of prBTA;
where those elements of T ∞ (prBTA) and operations on T ∞ (prBTA) are defined
as follows:
S
= (πn (S))n∈N ,
= (πn (D))n∈N ,

D
(tn )n∈N E a D

(t′n )n∈N

(tn )n∈N +π (t′n )n∈N

= (πn (tn E a D t′n ))n∈N ,
= (πn (tn +π t′n ))n∈N .
22

It is straightforward to check that the constants are elements of T ∞ (prBTA)
and the operations always yield elements of T ∞ (prBTA). It follows immediately
from the construction of the projective limit model of prBTA that the axiom
of prBTA forms a complete axiomatization of this model for equations between
closed terms.
A.2

Projective Limit Model of prTAtsi

We will write I(SFA) for the free SFA-extension of S and I(prTAtsi ) for the
free prTAtsi -extension of S.
From the fact that the signatures of I ∞ (prBTA) and I(SFA) are disjoint,
it follows, by the amalgamation result about expansions presented as Theorem 6.1.1 in [25] (adapted to the many-sorted case), that there exists a model of
prBTA combined with SFA such that the restriction to the signature of prBTA
is I ∞ (prBTA) and the restriction to the signature of SFA is I(SFA).
Let I ∞ (prBTA+SFA) be the model of prBTA combined with SFA referred to above. Then the projective limit model I ∞ (prTAtsi ) of prTAtsi is
I ∞ (prBTA+SFA) expanded with the operations defined by
(tn )n∈N / S = (πn (tn / S))n∈N ,
τtau ((tn )n∈N ) = (limk→∞ πn (τtau (tk )))n∈N
as interpretations of the additional operators of prTAtsi . On the right-hand side
of these equations, the symbols / and τtau denote the interpretation of the operators / and τtau in I(prTAtsi ). In the second equation, the limit is the limit
with respect to the discrete topology on T (prBTA).
It is straightforward to check that the operations with which I ∞ (prBTA)
is expanded always yield elements of T ∞ (prBTA). It follows immediately from
the construction of I ∞ (prTAtsi ) and Theorem 1 that I ∞ (prTAtsi ) is really a
projective limit model of prTAtsi .
A.3

Projective Limit Model of prTAsi

We will write I(prBTAnt ) for the initial model of prBTAnt and T (prBTAnt )
for the carrier of I(prBTAnt ). Moreover, we will write I(prTAsi ) for the initial
model of prTAsi .
With the projection functions πn extended from T (prBTA) to T (prBTAnt )
such that
πn+1 (t E nt(t′′ ) D t′ ) = πn+1 (t) E nt(πn+1 (t′′ )) D πn+1 (t′ ) ,
the projective limit model I ∞ (prBTAnt ) of prBTAnt is constructed from
I(prBTAnt ) like the projective limit model I ∞ (prBTA) of prBTA is constructed
from I(prBTA). The interpretation of the additional operator is the operation
on T ∞ (prBTAnt ) defined as follows:
(t1 n )n∈N E nt((t2 n )n∈N ) D (t3 n )n∈N = (πn (t1 n E nt(t2 n ) D t3 n ))n∈N .
23

The projective limit model I ∞ (prTAsi ) of prTAsi is I ∞ (prBTAnt ) expanded
with the operations defined by
knh,s ((t1 n )n∈N , . . . , (tm n )n∈N ) = (πn (knh,s (t1 n , . . . , tm n )))n∈N ,
n,i

n,i

⌋⌊h,s ((t1 n )n∈N , . . . , (tm n )n∈N ) = (πn (⌋⌊h,s (t1 n , . . . , tm n )))n∈N ,
SD ((tn )n∈N )

= (πn (SD (tn )))n∈N

as interpretations of the additional operators of prTAsi . On the right-hand side
n,i
of these equations, the symbols E nt( ) D, knh,s , ⌋⌊h,s , and SD denote the intern,i

pretation of the operators E nt( ) D, knh,s , ⌋⌊h,s , and SD in I(prTAsi ).
It is straightforward to check that the operations with which I ∞ (prBTAnt ) is
expanded always yield elements of T ∞ (prBTAnt ). It follows immediately from
the construction of I ∞ (prTAsi ) and Theorem 2 that I ∞ (prTAsi ) is really a
projective limit model of prTAsi .

References
1. Andova, S., Georgievska, S.: On compositionality, efficiency, and applicability of
abstraction in probabilistic systems. In: Nielsen, M., et al. (eds.) SOFSEM 2009.
Lecture Notes in Computer Science, vol. 5404, pp. 67–78. Springer-Verlag (2009)
2. Baeten, J.C.M., Bergstra, J.A., Smolka, S.A.: Axiomatizing probabilistic processes:
ACP with generative probabilities. Information and Computation 121(2), 234–255
(1995)
3. Baeten, J.C.M., Weijland, W.P.: Process Algebra, Cambridge Tracts in Theoretical
Computer Science, vol. 18. Cambridge University Press, Cambridge (1990)
4. Bergstra, J.A., Bethke, I., Ponse, A.: Cancellation meadows: A generic basis theorem and some applications. Computer Journal 56(1), 3–14 (2013)
5. Bergstra, J.A., Hirshfeld, Y., Tucker, J.V.: Meadows and the equational specification of division. Theoretical Computer Science 410(12–13), 1261–1271 (2009)
6. Bergstra, J.A., Loots, M.E.: Program algebra for sequential code. Journal of Logic
and Algebraic Programming 51(2), 125–156 (2002)
7. Bergstra, J.A., Middelburg, C.A.: Thread algebra with multi-level strategies. Fundamenta Informaticae 71(2–3), 153–182 (2006)
8. Bergstra, J.A., Middelburg, C.A.: Thread algebra for strategic interleaving. Formal
Aspects of Computing 19(4), 445–474 (2007)
9. Bergstra, J.A., Middelburg, C.A.: A thread algebra with multi-level strategic interleaving. Theory of Computing Systems 41(1), 3–32 (2007)
10. Bergstra, J.A., Middelburg, C.A.: Distributed strategic interleaving with load balancing. Future Generation Computer Systems 24(6), 530–548 (2008)
11. Bergstra, J.A., Middelburg, C.A.: Program algebra with a jump-shift instruction.
Journal of Applied Logic 6(4), 553–563 (2008)
12. Bergstra, J.A., Middelburg, C.A.: Instruction sequence notations with probabilistic
instructions. arXiv:0906.3083v1 [] (June 2009)
13. Bergstra, J.A., Middelburg, C.A.: A thread calculus with molecular dynamics.
Information and Computation 208(7), 817–844 (2010)
14. Bergstra, J.A., Middelburg, C.A.: Instruction sequence processing operators. Acta
Informatica 49(3), 139–172 (2012)

24

15. Bergstra, J.A., Middelburg, C.A.: Instruction Sequences for Computer Science,
Atlantis Studies in Computing, vol. 2. Atlantis Press, Amsterdam (2012)
16. Bergstra, J.A., Ponse, A.: Combining programs and state machines. Journal of
Logic and Algebraic Programming 51(2), 175–192 (2002)
17. Bergstra, J.A., Ponse, A.: Signed meadow valued probability mass functions.
arXiv:1307.5173v1 [math.LO] (July 2013)
18. Bergstra, J.A., Tucker, J.V.: The rational numbers as an abstract data type. Journal of the ACM 54(2), Article 7 (2007)
19. Gay, S.J.: Quantum programming languages: Survey and bibliography. Mathematical Structures in Computer Science 16(4), 581–600 (2006)
20. van Glabbeek, R.J., Smolka, S.A., Steffen, B.: Reactive, generative and stratified models of probabilistic processes. Information and Computation 121(1), 59–80
(1995)
21. Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification.
Addison-Wesley, Reading, MA, second edn. (2000)
22. He Jifeng, Seidel, K., McIver, A.K.: Probabilistic models for the guarded command
language. Science of Computer Programming 28(2–3), 171–192 (1997)
23. Hejlsberg, A., Wiltamuth, S., Golde, P.: C# Language Specification. AddisonWesley, Reading, MA (2003)
24. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood
Cliffs (1985)
25. Hodges, W.A.: Model Theory, Encyclopedia of Mathematics and Its Applications,
vol. 42. Cambridge University Press, Cambridge (1993)
26. Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. Information and
Computation 88(1), 60–87 (1990)
27. Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs
(1989)
28. Rabin, M.O.: Probabilistic algorithms. In: Traub, J.F. (ed.) Algorithms and Complexity: New Directions and Recent Results, pp. 21–39. Academic Press, New York
(1976)
29. Rabin, M.O.: Probabilistic algorithm for testing primality. Journal of Number Theory 12(1), 128–138 (1980)
30. Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs.
In: Computer Security Foundations Workshop 2000. pp. 200–214. IEEE Computer
Society Press (2000)
31. Sannella, D., Tarlecki, A.: Algebraic preliminaries. In: Astesiano, E., Kreowski,
H.J., Krieg-Brückner, B. (eds.) Algebraic Foundations of Systems Specification,
pp. 13–30. Springer-Verlag, Berlin (1999)
32. Shor, P.W.: Algorithms for quantum computation: Discrete logarithms and factoring. In: FOCS ’94. pp. 124–134. IEEE Computer Society Press (1994)
33. Waldspurger, C.A., Weihl, W.E.: Lottery scheduling: Flexible proportional-share
resource management. In: OSDI ’94. pp. 1–12. USENIX Association (1994)
34. Wirsing, M.: Algebraic specification. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 675–788. Elsevier, Amsterdam (1990)

25

