Information Technology Reference
In-Depth Information
and in particular bisimilarity corresponds to a pseudometric that is the greatest
fixed point of the monotone function.
3. As to the algorithmic characterisation, we will see that a partition refinement al-
gorithm can be used to check whether two states are bisimilar. We also propose an
“on-the-fly” algorithm that checks whether two states are related by probabilistic
bisimilarity. The schema of the algorithm is to approximate probabilistic bisimi-
larity by iteratively accumulating information about state pairs ( s , t ) where s and
t are not bisimilar. In each iteration we dynamically construct a relation
as an
approximant. Then we verify that every transition from one state can be matched
by a transition from the other state, and that their resulting distributions are related
by the lifted relation
R
. The latter involves solving the maximum flow problem
of an appropriately constructed network, by taking advantage of the close rela-
tionship between our lifting operation and the above mentioned maximum flow
problem.
R
3.2
Probabilistic Labelled Transition Systems
There are various ways of generalising the usual (nonprobabilistic) LTSs to a
probabilistic setting. Here we choose one that is widely used in the literature.
Definition 3.1
A probabilistic labelled transition system (pLTS) is defined as a
triple
S , L ,
, where
1. S is a set of states.
2. L is a set of transition actions.
3. Relation
is a subset of S
×
L
× D
( S ).
A nonprobabilistic LTS may be viewed as a degenerate pLTS — one in which
only point distributions are used. As with LTSs, we write s
ʱ
−ₒ
ʔ in place of
ʱ
−ₒ
ʱ
−ₒ
( s , ʱ , ʔ )
∈ₒ
. If there exists some ʔ with s
ʔ , then the predicate s
holds.
ʱ
−ₒ
Similarly, s
holds if there is some ʱ with s
. A pLTS is finitely branching if
ʱ
−ₒ
the set
{
ʱ , ʔ
L
× D
( S )
|
s
ʔ
}
is finite for all states s ; if moreover S is
finite, then the pLTS is said to be finitary .
Convention All the pLTSs considered in this topic are assumed to be finitary, unless
otherwise stated.
In order to visualise pLTSs, we often draw them as directed graphs. Given that in
a pLTS transitions go from states to distributions, we need to introduce additional
edges to connect distributions back to states, thereby obtaining a bipartite graph.
States are therefore represented by nodes of the form
and distributions by nodes of
ʱ
−ₒ
the form
. For any state s and distribution ʔ with s
ʔ we draw an edge from s
to ʔ , labelled with ʱ . Consequently, the edges leaving a
-node are all labelled with
actions from L . For any distribution ʔ and state s in
, the support of ʔ , we draw
an edge from ʔ to s , labelled with ʔ ( s ). Consequently, the edges leaving a
ʔ
-node
Search WWH ::




Custom Search