## Modal Logics for Mobile Processes

**Robin Milner, Joachim Parrow and David Walker**
*Abstract:* In process algebras, bisimulation equivalence
is typically defined directly in terms of the operational rules of
action; it also has an alternative characterisation in terms of a
simple modal logic (sometimes called *Hennessy-Milner logic*.
This paper first defines two forms of bisimulation equivalence for
the pi-calculus, a process algebra which allows dynamic
reconfiguration among processes; it then explores a family of
logics with different modal operators. It is proven that two of
these logics characterise the two bisimulation equivalences. Also,
the relative expressive power of all the logics is exhibited as a
lattice.

This report appeared in *Theoretical Computer Science*
**114** (1993) pp.149--171.

*LFCS report ECS-LFCS-91-136*

Previous |

Index |

Next