数理解析研究所講究録996 巻 1997 年 96-97

96

Symbolic Bisimulations and Proof Systems for The-Calculus(Abstract)$*$$\pi$

Huimin$\mathrm{L}\mathrm{i}\mathrm{n}^{\uparrow}$

Laboratory for Computer Science
Institute of Software, Chinese Academy of Sciences

Axiomatisations for basic process algebras such as CCS, CSP, ACP, LOTOS..., arebased on equational logic. But purely equational reasoning is difficult for the -calculus
because here input prefixes introduce bound names, i.e. names which are local within thescope of the input prefixes and can be instantiated with arbitrary free names. Reflected in
the axiomatisations this amounts to require when an input prefix is introduced the input
name must not be used before, a concept difficult to be formulated in the frameworkof equational logic. The “symbolic” style proof system generalise equational logic by(where is a boolean condition on
using conditional equations of the form
names andare process terms) as judgements. For each construct in the calculus
there corresponds an introduction rule in the core proof system. For instance the rule
for input prefix is$\pi$$\phi\triangleright T=U$

$T,$$\phi$$U$

INPUT$\frac{\emptyset\triangleright\tau=U}{\phi\triangleright a(X).T=b(x).U}\phi\Rightarrow a=b$,$x\not\in n(\phi)$

Here represents the context condition for deriving $T=U$ , and the side condition
ensures the input name is fresh.
In [Lin94] it is shown that, together with the standard CCS axioms for strong bisimulation, this core proof system is sound and complete for late strong bisimulation inrecursion-free -calculus. By adding either an inference rule dealing with early input
or an axiom schemaproof systems for early bisimulation can be obtained. In
it is further shown that to extend these results to weak bisimulationequivalences all what needed is the three -laws.
For the -calculus with recursion the key inference rule is unique fixpoint induction.
It is syntactically identical to its pure-CCS counterpart, but work at the levelof abstractions:$\phi$$x$$\pi$$([\mathrm{H}\mathrm{L}96])$$([\mathrm{P}\mathrm{S}93])$$[\mathrm{L}\mathrm{i}\mathrm{n}95\mathrm{a}]$$([\mathrm{M}\mathrm{i}189])$$\tau$$\pi$$([\mathrm{M}\mathrm{i}184])$

UFI $\frac{F=G[F/X]}{F=\mu XG}$

$X$

guarded in$G$*Supported by research grants from the President Fund of Chinese Academy of Sciences and National
Natural Science Foundation of China.
author’s address: Institute of Software, Chinese Academy of Sciences,.Box 8718, Beijing
100080. Email: lhm@ox.ios.ac.cn.
$\uparrow \mathrm{T}\mathrm{h}\mathrm{e}$$\mathrm{P}.\mathrm{O}$97
ar name-closed abstractions. Extended with this rule, and thewhere both $F$ andrecursions, the core proof system is sound and comstandard rules forguarded
plete for strong bisimulation in finite-control -calculus where recursions. To achieve complet proof system for arbitrary recursions, the following
axiom can be adopted to reduce unguarded recursions to guarded ones:
$G$

$e$

$\mathrm{f}\mathrm{o}\mathrm{l}\mathrm{d}\mathrm{i}\mathrm{n}\mathrm{g}/\mathrm{u}\mathrm{n}\mathrm{f}\mathrm{o}\mathrm{l}\mathrm{d}\mathrm{i}\mathrm{n}\mathrm{g}$$\mathrm{a}r\mathrm{e}$

$\pi$

$e$

$([\mathrm{L}\mathrm{i}\mathrm{n}95\mathrm{b}])$

UNG fixX$( \vec{x})(\sum i\in I\emptyset i\nu\vec{X}_{i}’X(\vec{X}_{i})+T)=\mathrm{f}\mathrm{i}\mathrm{X}X(\vec{X})(\Sigma_{i\in I}\phi_{i}\nu\vec{x}_{i}’\tau[\vec{X}_{i}/\vec{x}]+^{\tau})$

where the summands in the recursion body satisfy certain saturation condition.
The proofs of the above mentioned completeness results rely on the notion of symbolic
bisimulation, first proposed in [HL95] for general message-passing process algebras. As
alternative characterisations of the standard definitions of bisimulations in the -calculus,
symbolic bisimulations overcome the infinity inherited in the standard definitions by
employing finite partitions over the name space, instead of instantiating input names
and name parameters of recursively defined processes. Another powerful technical device
upon which the completeness proofs heavily rely is the notion of maximally consistentname conditions.
Currently work is going on to extend the above results to weak bisimulation equiva-calculus.
lences in finite-cont$\pi$$r\mathrm{o}1\pi$References[HL95]

M. Hennessy and H. Lin. Symbolic bisimulations. Theoretical Computer Science, 138:353-389, 1995.

[HL96]

M. Hennessy and H. Lin. Proof systems for message-passing process algebras.
Formal Aspects of Computing, 8:408-427, 1996.

[Lin94]

H. Lin. Symbolic bisimulations and proof systems for the -calculus. Report
7/94, Computer Science, University of Sussex, 1994.
$\pi$[Lin95a] H. Lin. Complet e inference systems for weak bisimulation equivalences in the-calculus. In Proceedings of Sixth International Joint Conference on the Theory and Practice of Software Development, volume 915 of Lecture Notes in
Computer Science. Springer-Verlag, 1995.
$\pi$[Lin95b] H. Lin. Unique fixpoint induction for the -calculus. In Proceedings of Sixth
International Conference on Concurrency Theory, volume 962 of Lecture Notes
in Computer Science. Springer-Verlag, 1995.
$\pi$[Mi184]

R. Milner. A complete inference system for a class of regular behaviours. J.
Computer and System Science, 28:439-466, 1984.

[Mi189]R. Milner. Communication and Concurrency. Prentice-Hall, 1989.

[PS93]

J. Parrow and D. Sangiorgi. Algebraic theories for name-passing calculi. Report
ECS-LFCS-93-262, LFCS, University of Edinburgh, 1993.