Probabilistic Bisimulation - Semantics of Probabilistic Processes: An Operational Approach - page 49

We shall consider (closed) equation systems of formulae of the form

E : X 1 = ˕ 1

.

X n = ˕ n

where X 1 , ... , X n are mutually distinct variables and ˕ 1 , ... , ˕ n are formulae hav-
ing at most X 1 , ... , X n as free variables. Here E can be viewed as a function
E : Var

ₒ L μ defined by E ( X i ) = ˕ i for i = 1, ... , n and E ( Y ) = Y for

other variables Y Var .

An environment ˁ is a solution of an equation system E if

∈

[[ ˕ i ]] ˁ .
The existence of solutions for an equation system can be seen from the following
arguments. The set Env , which includes all candidates for solutions, together with
the partial order

∀ i : ˁ ( X i ) =

≤ defined by

ˁ iff ˁ ( X ) ˁ ≤ ∀ X ∈ Var : ˁ ( X ) ↆ

E

: Env

ₒ Env given in the

forms a complete lattice. The equation function

ʻ -calculus notation by

E : = ʻˁ.ʻX. [ | E ( X ) | ] ˁ

is monotone. Thus, the Knaster-Tarski fixed-point theorem guarantees existence of
solutions, and the largest solution

ˁ E : = { ˁ | ˁ ≤ E ( ˁ ) }

3.6.2.2 Characteristic Equation Systems

As studied in [ 53 ], the behaviour of a process can be characterised by an equation sys-
tem of modal formulae. Below we show that this idea also applies in the probabilistic
setting.

Definition 3.9 Given a finitary pLTS, its characteristic equation system consists of
one equation for each state s 1 , ... , s n ∈

S .

E : X s 1 = ˕ s 1

.

X s n = ˕ s n

where

⊛
⊝

⊞ ⊛

⊝
a ∈ L

⊞

[ a ]

⊠ ∧ ⊠

˕ s : =

−ₒ ʔ a X ʔ

X ʔ (3.19)

a a