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

fixed-point operators to describe infinite behaviour. But for finite processes where
no infinite behaviour occurs, an adequate logic will also be expressive for those
processes.

3.6.1 An Adequate Logic

We extend the Hennessy-Milner logic by adding a probabilistic-choice modality to
express the behaviour of distributions.

Definition 3.8 L hm of modal formulae over L , ranged over by ˕ ,is

defined by the following grammar:

The class

=|

˕ 1 ∧ ˕ 2 |¬

|

˕ : ˕ a ˈ

=

ˈ : ˕ 1 p ↕ ˕ 2

where p [0, 1]. We call ˕ a state formula and ˈ a distribution formula . Note that

a distribution formula ˈ only appears as the continuation of a diamond modality

∈

ˈ . We sometimes use the finite conjunction i ∈ I ˕ i as syntactic sugar.
The satisfaction relation

a

|=ↆ S × L hm is defined by

• s |= for all s ∈ S .

• s |= ˕ 1 ∧ ˕ 2 if s |= ˕ i for i = 1, 2.

• s |= ¬ ˕ if it is not the case that s |= ˕ .

a
−ₒ ʔ and ʔ |= ˈ . • s |= a ˈ if for some ʔ ∈ D ( S ), s

• ʔ |= ˕ 1 p ↕ ˕ 2 if there are ʔ 1 , ʔ 2 ∈ D ( S ) with ʔ = p · ʔ 1 + (1 − p ) · ʔ 2 and for

˕ i .
With a slight abuse of notation, we write ʔ

each i = 1, 2, t ∈ ʔ i we have t |=

|= ˈ above to mean that ʔ satisfies the

distribution formula ˈ . For any ˕ ∈ L hm , the set of states that satisfies ˕ is denoted

by [[ ˕ ]], i.e. [[ ˕ ]] ={ s ∈ S | s |= ˕ } .

Example 3.1 Let ʔ be a distribution and ˕ be a state formula. We consider the
distribution formula

ˈ : = ˕ p ↕

where p = ʔ ([[ ˕ ]]). It is not difficult to see that ʔ |= ˈ holds. In the case p = 0 the

formula ˈ degenerates to . In the case p> 0 the distribution ʔ can be decomposed

as follows.

ʔ ( s )
p ·

ʔ ( s )
1

ʔ = ʔ ( s ) · s = p · s + (1 − p ) ·

p ·

s.

−

s ∈ S s ∈ [ | ˕ | ] s ∈ [ | ˕ | ]

So ʔ can be written as the linear combination of two distributions; the first one has
as support all the states that can satisfy ˕ . In general, for any ʘ

∈ D ( S )wehave

ʘ |= ˈ if and only if ʘ ([[ ˕ ]] ) ≥ p .