New for: D3
play a crucial role for the design by stepwise refinement and
system analysis. In particular, the weak equivalences
that abstract from internal computations are of great importance as they
are appropriate to compare systems on different levels of abstraction
(which is typically the case for an implementation and its specification).
This talks gives an overview of the several types of weak bisimulation
equivalences for probabilistic systems proposed in the literature
and presents a novel notion of weak bisimulation equivalence (called
``uniform bisimulation equivalence''). We discuss the use of these
equivalences as implementation relations via several criteria,
e.g. the soundness for establishing linear time properties, decidability
and compositionality.