Information Technology Reference
In-Depth Information
there is no agreement on which is the best equivalence relation; in formal verifica-
tion different equivalences might be suitable for different applications. Sometimes
an equivalence is induced by a preorder relation, by taking the intersection of the
preorder with its inverse relation, instead of being directly defined.
Among the various equivalences, bisimilarity [ 2 , 15 ] is one of the most impor-
tant ones as it admits beautiful characterisations in terms of fixed points, modal
logics, coalgebras, pseudometrics, games, decision algorithms, etc. In this topic
we will characterise bisimilarity for probabilistic processes from metric, logical and
algorithmic perspectives.
Preorders can be used to formalise a “better than” relation between programs
or processes, one that has its origins in the original work assigning meanings to
programs and associating a logic with those meanings [ 12 , 13 ]. Usually that relation
is expressed in two different ways: either to provide a witness for the relation or to
provide a testing context to make obvious that one program is actually not better than
another.
Two important kinds of preorders are testing preorders [ 16 , 17 ] and simulation
preorders . They give rise to testing semantics and simulation semantics , respectively.
In a testing semantics, two processes can be compared by experimenting with a class
of tests. Process P is deemed “better” than process Q if the former passes every test
that the latter can pass. In contrast, to show that P is not “better” than Q it suffices
to find a test that Q can pass but P cannot. In a simulation semantics, process P can
simulate Q if Q performs an action and evolves into Q then P is able to exhibit
the same action and evolve into P such that P can simulate Q in the next round
of the simulation game. Simulation is coinductively defined and comes along with a
proof principle called coinduction : to show that two processes are related it suffices
to exhibit a simulation relation containing a pair consisting of the two processes.
In the nonprobabilistic setting, simulation semantics is in general finer than testing
semantics in that it can distinguish more processes. However, in this topic we will
see that for a large class of probabilistic processes, the gap between simulation and
testing semantics disappears. Therefore, in this case we have a semantics where both
negative and positive results can easily be proved: to show that two processes are not
related in the semantics we just give a witness test, while to show that two processes
are related we construct a relation and argue that it is a simulation relation.
1.2
Synopsis
The remainder of the topic is organised as follows. Chapter 2 collects some funda-
mental concepts and theorems in a few mathematical subjects such as lattice theory,
topology and linear programming. They are briefly reviewed and meant to be used
as references for later chapters. Most of the theorems are classic results, and thus
are stated without proofs as they can be easily found in many standard textbooks in
mathematics. It is not necessary to go through the whole chapter; readers can refer
to relevant parts of this chapter when it is mentioned elsewhere in the topic.
Search WWH ::




Custom Search