Change search
ReferencesLink to record
Permanent link

Direct link
A Proof System for the pi-calculus
Number of Authors: 2
1996 (English)Report (Refereed)
Abstract [en]

We study the problem of specifying and verifying properties of pi-calculus processes while relying on a bisimulation semantics. As our property specification language we use a version of the modal mu-calculus adapted to the pi-calculus. We show that the logical language is sufficiently expressive to characterize by means of a finite formula a process up to any approximation of the bisimulation relation. We consider the problem of checking that a process of the pi-calculus satisfies a specification expressed in this modal mu-calculus. We develop an algorithm which is sound in general, and complete for processes having a finite reachability property. Finally, we present a proof system which can be applied to prove non-recursive properties of arbitrary processes. We show that the system is complete on the non-recursive fragment of the logical language.

Place, publisher, year, edition, pages
Kista, Sweden: Swedish Institute of Computer Science , 1996, 9. , 28 p.
SICS Technical Report, ISSN 1100-3154 ; R96:03
Keyword [en]
Process Algebra, Temporal Logic, Mobile Processes, Compositional Verification, Model Checking
National Category
Computer and Information Science
URN: urn:nbn:se:ri:diva-14097OAI: diva2:1035381
Available from: 2016-10-13 Created: 2016-10-13

Open Access in DiVA

fulltext(2450 kB)1 downloads
File information
File name FULLTEXT01.pdfFile size 2450 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 1 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

ReferencesLink to record
Permanent link

Direct link