Paolo Baldan (1) -
Andrea Bracciali (2) -
Roberto Bruni (2)
(1) Dipartimento di Informatica, Università Ca' Foscari di Venezia, Italia. (2) Dipartimento di Informatica, Università di Pisa, Italia.
Abstract:
Behavioural equivalences on open systems are usually defined by
comparing system behaviour in all environments. Due to this
"universal" quantification over the possible hosting environments,
such equivalences are often difficult to check in a direct way.
Here, working in the setting of process calculi, we introduce a
hierarchy of behavioural equivalences for open systems, building on
a previously defined symbolic approach.
The hierarchy comprises both branching, bisimulation-based, and
non-branching, trace-based, equivalences.
Symbolic equivalences are amenable to effective analysis techniques
(e.g., the symbolic transition system is finitely branching under
mild assumptions), which result to be sound, but often not
complete due to redundant information.
Two kinds of redundancy, syntactic and semantic, are discussed and
and one class of symbolic equivalences is identified that deals
satisfactorily with syntactic redundant transitions, which are a
primary source of incompleteness.