Modal Logics for Mobile Processes

Robin Milner, Joachim Parrow, David Walker

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

In process algebras, bisimulation equivalence is typically defined directly in terms of the operational rules of action; it also has an alternative characterization in terms of a simple modal logic (sometimes called Hennessy-Milner logic). This paper first defines two forms of bisimulation equivalence for the π-calculus, a process algebra which allows dynamic reconfiguration among processes; it then explores a family of possible logics, with different modal operators. It is proven that two of these logics characterize the two bisimulation equivalences. Also, the relative expressive power of all the logics is exhibited as a lattice. The results are applicable to most value-passing process algebras.
Original languageEnglish
Pages (from-to)149-171
Number of pages23
JournalTheoretical Computer Science
Volume114
Issue number1
DOIs
Publication statusPublished - Jun 1993

Fingerprint

Dive into the research topics of 'Modal Logics for Mobile Processes'. Together they form a unique fingerprint.

Cite this