Wed 23 Jul
Symbolic Techniques for Value-passing Calculi
We describe the symbolic operational semantics for value-passing
calculi proposed by Hennessy and Lin. A feature of this approach
is a treatment of value-passing processes as first-order processes
proper rather than codifying them as pure processes.
The advantages of such a semantics are manifest when attempting
process verification. We show how the symbolic approach can be
applied to the problems of verifying bisimilarity using equational
reasoning, and model checking properties of value-passing processes.