Abstract:

Most of the traditional verification methods for process description languages rely on the fact that the underlying transition systems are finite branching. If processes are allowed to send and receive messages or values from an infinite data set then this is rarely the case. However if we work with ``symbolic transition systems'' as opposed to the usual concrete ones then many of the standard methods can still be applied. This talk will survey recent joint work with H. Lin and X. Liu on this symbolic approach to message-passing processes. This will include a theory of symbolic bisimulations, sound and complete proof systems for mesage-passing process calculi and a logical characterisation of bisimulation equivalence in terms of a first-order modal logic.