MOVES Seminar, 13 Jan 2010, 10:00, Room 5056
Prof. Dr. Franck van Breugel (York University, Toronto)
Behavioural Pseudometrics
Abstract:
Concurrent systems are often modelled by means of labelled transition
systems. A labelled transition system is similar to a nondeterministic
finite automaton. In contrast to a finite automaton, the set of states
and the set of actions of a labelled transitions may be
infinite. Furthermore, a labelled transition system does usually not
have an initial state or final states.
A behavioural equivalence is an equivalence relation on the states of
a labelled transition system. Such a relation captures which states
behave the same. Many different behavioural equivalences have been
proposed. Bisimilarity is considered to be one of the key behavioural
equivalences for labelled transition systems.
To model concurrent systems in which quantitative data, such as
probabilities and time, play a crucial role, several variations on
labelled transition systems have been put forward. Notions of
behavioural equivalence like bisimilarity have been adapted to these
systems. However, such discrete Booleanvalued notions (states are
either behaviourally equivalent or they are not) sit uneasily with
systems featuring quantitative data. If some of this data change a
little bit --the data are often obtained experimentally and, hence,
are usually approximations-- states that used to be behaviourally
equivalent may not be anymore or vice versa. In conclusion,
behavioural equivalences are not robust.
To address this problem, pseudometrics that assign a distance, a real
number between 0 and 1, to each pair of states have been
proposed. Such a pseudometric yields a smooth and quantitative notion
of behavioural equivalence. The distance between states is used to
express the similarity of their behaviour. The smaller the distance,
the more alike the states behave. In particular, the distance between
states is zero if they are behaviourally indistinguishable.
In my talk, I will discuss behavioural pseudometrics and present
algorithms to approximate them. This talk is based on joint work with
Claudio Hermida, Michael Makkai, Mike Mislove, Joel Ouaknine, Steven
Shalit, Babita Sharma, James Worrell and Hongming Wu.
systems. A labelled transition system is similar to a nondeterministic
finite automaton. In contrast to a finite automaton, the set of states
and the set of actions of a labelled transitions may be
infinite. Furthermore, a labelled transition system does usually not
have an initial state or final states.
A behavioural equivalence is an equivalence relation on the states of
a labelled transition system. Such a relation captures which states
behave the same. Many different behavioural equivalences have been
proposed. Bisimilarity is considered to be one of the key behavioural
equivalences for labelled transition systems.
To model concurrent systems in which quantitative data, such as
probabilities and time, play a crucial role, several variations on
labelled transition systems have been put forward. Notions of
behavioural equivalence like bisimilarity have been adapted to these
systems. However, such discrete Booleanvalued notions (states are
either behaviourally equivalent or they are not) sit uneasily with
systems featuring quantitative data. If some of this data change a
little bit --the data are often obtained experimentally and, hence,
are usually approximations-- states that used to be behaviourally
equivalent may not be anymore or vice versa. In conclusion,
behavioural equivalences are not robust.
To address this problem, pseudometrics that assign a distance, a real
number between 0 and 1, to each pair of states have been
proposed. Such a pseudometric yields a smooth and quantitative notion
of behavioural equivalence. The distance between states is used to
express the similarity of their behaviour. The smaller the distance,
the more alike the states behave. In particular, the distance between
states is zero if they are behaviourally indistinguishable.
In my talk, I will discuss behavioural pseudometrics and present
algorithms to approximate them. This talk is based on joint work with
Claudio Hermida, Michael Makkai, Mike Mislove, Joel Ouaknine, Steven
Shalit, Babita Sharma, James Worrell and Hongming Wu.
