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.
Here, we introduce a hierarchy of behavioural equivalences for open
systems in the setting of process calculi, building on a symbolic
approach proposed in a previous paper. 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
correct, but often not complete due to redundant information. Two
kinds of redundancy, syntactic and semantic, are discussed and one
class of symbolic equivalences is identified that deals
satisfactorily with syntactic redundant transitions, which are a
primary source of incompleteness.