**BRICS** **R** **S-01-8** **F** **re** **ndrup** **&** **J** **ensen:** **Checking** **for** **O** **p** **en** **Bisimilarity** **in** **the** **π** **-Calculus**

**π**

## BRICS

**Basic Research in Computer Science**

**Checking for Open Bisimilarity in** **the** **π** ^{-Calculus}

**π**

^{-Calculus}

**Ulrik Frendrup**

**Jesper Nyholm Jensen**

**BRICS Report Series** **RS-01-8**

**Copyright c** **2001,** **Ulrik Frendrup & Jesper Nyholm Jensen.**

**BRICS, Department of Computer Science** **University of Aarhus. All rights reserved.**

**Reproduction of all or part of this work** **is permitted for educational or research use** **on condition that this copyright notice is** **included in any copy.**

**See back inner page for a list of recent BRICS Report Series publications.**

**Copies may be obtained by contacting:**

**BRICS**

**Department of Computer Science** **University of Aarhus**

**Ny Munkegade, building 540** **DK–8000 Aarhus C**

**Denmark**

**Telephone: +45 8942 3360** **Telefax:** **+45 8942 3255** **Internet:** **BRICS@brics.dk**

**BRICS publications are in general accessible through the World Wide** **Web and anonymous FTP through these URLs:**

### http://www.brics.dk ftp://ftp.brics.dk

**This document in subdirectory** RS/01/8/

Checking for Open Bisimilarity in the

*π*

^{-Calculus}

BRICS 1

UlrikFrendrup&JesperNyholm Jensen

AalborgUniversity,DepartmentofComputerScience

FredrikBajersVej 7E

9220AalborgØ,Denmark

Email: ulrikf@cs.auc.dk,nyholm@gaztricjuice.dk

Abstract

This paper deals with algorithmic checking of open bisimilarity in the

*π*

^{-calculus.}

^{Most}

bisimulationcheckingalgorithmsarebasedonthepartitionrenementapproach. Unfortu-

nately thedenition ofopenbisimulationdoesnotpermit usto useapartition renement

approachforopenbisimulationcheckingdirectly, butin thepaperA PartitionRenement

Algorithmforthe

*π*

^{-Calculus}

^{Marco}

^{Pistore}

^{and}

^{Davide}

^{Sangiogi}

^{present}

^{an}

^{iterative}

^{method}

that makes itpossible to check for open bisimilarity using partition renement. Wehave

implemented the algorithm presented by Marco Pistore and Davide Sangiorgi. Further-

more, we haveoptimized this algorithm and implemented this optimized algorithm. The

time-complexityofthisalgorithmisthesameasthetime-complexityfortherstalgorithm,

but performance tests have shown that in many casesthe running time of the optimized

algorithmisshorterthantherunningtimeof therstalgorithm.

Ourimplementationoftheoptimizedopenbisimulationcheckeralgorithmandauserinter-

face havebeenintegrated in asystemcalled theOBC Workbench.The source code and a

manualforitisavailablefrom http://www.cs.auc.dk/research/FS/ny/PR-pi/.

1

BasicResearchinComputerScience(www.brics.dk),fundedbytheDanishNationalResearchFounda-

tion

1 Introduction 4

2 Checkingfor Bisimilarity UsingPartition Renement 5

2.1 TheGeneralizedPartitionRenementProblem . . . 5

2.2 BisimulationChecking . . . 6

3 The

*π*

^{-Calculus}

^{8}3.1 Syntax . . . 8

3.2 Semantics . . . 10

3.3 Bisimulation. . . 10

4 AlgorithmforChecking Open Bisimilarityin the

*π*

^{-Calculus}

^{13}4.1 Syntax . . . 13

4.2 Semantics . . . 14

4.3 OpenBisimulation . . . 16

4.4 ConstrainedProcesses . . . 17

4.5 Non-RedundantTransitions . . . 19

4.6 ActiveNames . . . 20

4.7 TheIterativeMethod . . . 22

4.8 TheAlgorithm . . . 23

4.9 Examples . . . 25

5 Implementationof Open BisimulationChecker 30 5.1 DataTypes . . . 30

5.2 Finding Transitions. . . 33

5.4 Step1-ConstructionoftheStateGraphs . . . 36

5.5 Step2-Initializing Partition

*W*

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{38}

5.6 Step3-StabilizingPartition

*W*

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{.}

^{39}

5.7 Step4-Result . . . 44

5.8 MainFunction . . . 44

6 Optimization 45 6.1 ReducingtheSizesoftheStateGraphs . . . 45

6.2 OptimizingtheComputationofNon-RedundantTransitions. . . 48

6.3 OptimizingtheComputationofActiveNames. . . 48

6.4 OptimizingtheComputationoftheNormalizedTransitions . . . 49

6.5 AFasterPartitionRenementAlgorithm . . . 50

6.6 Heuristics . . . 51

6.7 RemarksontheOptimizedAlgorithm . . . 51

7 Conclusion 52 A The Optimized Algorithm 55 B PerformanceTests 60 B.1

*π*

^{-Processes}

^{Used}

^{in}PerformanceTests . . . 60

B.2 ResultsofPerformanceTests . . . 61

Introduction

This paperdealswithalgorithmiccheckingofopenbisimilarityin the

*π*

^{-calculus.}

^{We}

^{have}

implementedanalgorithmforopenbisimulationcheckinginthe

*π*

^{-calculus.}

^{Most}

^{algorithms}

forbisimulationcheckingarebasedonpartitionrenement,butthedenitionofopenbisim-

ulation makes itdicult to use this strategyfor an openbisimulationchecking algorithm

directly sincethe statespaces of the processesbeingchecked for open bisimilarity cannot

beconstructedseparately. Wehaveimplementedtheopenbisimulationcheckingalgorithm

presentedin [10]. This algorithm was developed byintroducing the notionof constrained

processes,deningactivenamesbisimulationonconstrainedprocesses,showingthatthereis

ausefulconnectionbetweenopenbisimilarityandactivenamesbisimilarity,anddeveloping

aniterativemethodforcheckingactivenamesbisimilarity.

Wehaveoptimized thealgorithm foropenbisimulationchecking,implementedthis al-

gorithm, and carriedout someperformancetests of therst and theoptimized versionof

the implementation. Finally, the implementation of the optimized algorithm and a user

interfacehavebeenintegratedinasystemcalled theOBCWorkbench.

Thispapercontainssevenchaptersandtwoappendicesandisorganizedasfollows. Chap-

ter 2describes thegeneralized partition renementproblem and shows how an algorithm

for solvingthis problemcan beusedfor checkingbisimilarity. Inchapter 3wepresentthe

syntaxandsemanticsofasubsetofthe

*π*

^{-calculus}

^{and}

^{dene}

^{some}traditionalbisimilarities between

*π*

-processes. In chapter 4 we present another notion of bisimilarity called open
bisimilaritydened by[10]. Chapter 4alsocontainssomeresultsfrom[10]thatshowsthat
openbisimilaritycan be checked algorithmically. Chapter 5containsadescription of our

rst implementation of the open bisimulationcheckingalgorithm and chapter 6 describes

howthe algorithm is optimizedwith respect to running time. Weconclude onthe imple-

mentation in chapter 7. Pseudo code for the optimized implementation can be found in

appendixA. Resultsofperformancetestsoftherstandtheoptimizedimplementationand

acomparisonofthesecanbefoundinappendixB.

Checking for Bisimilarity Using

Partition Renement

Thealgorithmforopenbisimulationcheckinginthe

*π*

^{-calculus}

^{developed}

^{by}

^{[10]}

^{is}

^{as}

^{many}

other bisimulationequivalence checkingalgorithms based on partition renement. Inthis

chapterwedescribethegeneralizedproblemofpartitionrenement. Furthermore,weshow

howthis canbeusedforbisimulationchecking.

2.1 The Generalized Partition Renement Problem

Beforewecanpresentthegeneralized partition renement problem weneedtodene

thenotionsof partitions andblocks.

Denition 1 (Partitionsandblocks)

Let

*U*

^{be}

^{a}

^{set.}

^{A}

^{partition}

*W*

^{of}

*U*

^{is}

^{a}

^{nite}

^{set}

^{of}

^{pairwise}

^{disjoint}

^{subsets}

*B* _{1} *, . . . B* *n*

^{of}

*U*

^{where}

### S

*i* *∈{1* *,...,n* *}* *B* *i* = *U*

^{.}

^{The}

^{sets}

*B* *i*

^{of}

*W*

^{are}

^{called}

^{blocks.}

Denition 2 (GeneralizedPartitionRenementProblem)

Givenaset

*U*

^{,}

^{a}

^{partition}

*W* = *{B* 1 *, . . . B* *n* *}*

^{of}

*U*

^{,}

^{and}

*k*

^{functions}

*f* *l* : *U* *→ P* (U )

^{,}

### 1 *≤* *l* *≤* *k*

^{,}

wewanttorene

*W*

^{into}

^{a}

^{new}

^{partition}

*W* ^{0}

^{0}

^{of}

*U*

^{,}

^{where}

*W* ^{0} = *{C* 1 *, . . . , C* *m* *}*

^{0}

^{is}

^{the}

^{coarsest}

set (theset withfewestblocks)satisfying

(i) foreach

*i* *∈ {* 1, . . . , m}

^{there}

^{exists}

^{a}

*j* *∈ {* 1, . . . , n}

^{such}

^{that}

*C* *i* *⊆* *B* *j*

^{and}

(ii) forany

*a, b* *∈* *C* *i*

^{,}

^{any}

^{block}

*C* *j*

^{,}

### 1 *≤* *i, j* *≤* *m*

^{,}

^{and}

^{any}

^{function}

*f* *l*

^{,}

### 1 *≤* *l* *≤* *k*

^{it}

^{holds}

that

*f* *l* (a) *∩* *C* *j* *6* = *∅*

^{if}

^{and}

^{only}

^{if}

*f* *l* (b) *∩* *C* *j* *6* = *∅*

^{.}

Thenewpartition

*W* ^{0}

^{0}

^{always}

^{exists[3]}

^{and}

^{is}

^{the}

^{unique}

^{greatest}

^{xed}

^{point}

^{of}

^{the}

^{function}

*ψ* _{W}

_{W}

^{that}

^{maps}

^{partitions}

^{of}

*U*

^{to}

^{partitions}

^{of}

*U*

^{and}

^{is}

^{dened}

^{by}

*C* *∈* *ψ* _{W} ( *W* ^{0} )

_{W}

^{0}

^{if}

^{and}

^{only}

^{if}

(i)

*∃B* *∈ W.(C* *⊆* *B)*

^{and}

(ii) forany

*a, b* *∈* *C*

^{,}

^{any}

^{block}

*C* ^{0} *∈ W* ^{0}

^{0}

^{0}

^{,}

^{and}

^{any}

^{function}

*f* *l*

^{,}

### 1 *≤* *l* *≤* *k*

^{it}

^{holds}

^{that}

*f* *l* (a) *∩* *C* ^{0} *6* = *∅*

^{0}

^{if}

^{and}

^{only}

^{if}

*f* *l* (b) *∩* *C* ^{0} *6* = *∅*

^{0}

^{.}

The partition

*W* ^{0}

^{0}

^{induces}

^{an}equivalence

*W* _{∼} ^{0}

_{∼}

^{0}

^{dened}

^{by}

*W* _{∼} ^{0} ^{def} = *{* (a, b) *| ∃B* *∈ W.(a, b* *∈* *B)* *}*

_{∼}

^{0}

^{def}

^{.}

^{So}

^{the}generalizedpartitionrenementproblemconsistsofcomputingtheequivalence classesof

*U*

^{for}

^{an}equivalencedened asagreatestxedpoint.

Insection5.3wewillpresentanalgorithmtosolvethepartitionrenementproblemfor

a nite set

*U*

^{and}

*k* = 1

^{.}

^{This}

^{can}

^{be}

^{used}

^{to}

^{solve}

^{the}generalized partition renement problem in an iterative process where the renement algorithm is applied once for each

function ineachiterationuntilthepartitionstabilizes.

Inthefollowingsection weshowhowapartition renementalgorithm canbeused for

bisimulationchecking.

2.2 Bisimulation Checking

Let

*P*

^{be}

^{a}

^{set}

^{of}

^{states}

^{and}

*A* *ct*

^{a}

^{set}

^{of}

^{labels.}

^{We}

^{let}

*P*

^{and}

*Q*

^{range}

^{over}

*P*

^{and}

*α*

^{over}

*Act*

^{.}

^{F}

^{or}

^{a}

^{given}

^{labeled}

^{transition}

^{system}

^{(}

*P*

^{,}

*Act*

^{,}

*−→*

^{)}

^{we}

^{dene}bisimulationasfollows.

Denition 3 (Bisimulation)

Arelation

*R ⊆ P × P*

^{is}

^{a}bisimulationif

### (P, Q) *∈ R*

^{implies,}

(i) if

*P* *−→* ^{α} *P* ^{0}

^{α}

^{0}

^{then}

^{for}

^{some}

*Q* ^{0} *∈ P*

^{0}

^{,}

*Q* *−→* ^{α} *Q* ^{0}

^{α}

^{0}

^{and}

### (P ^{0} *, Q* ^{0} ) *∈ R*

^{0}

^{0}

^{,}

^{and}

(ii) if

*Q* *−→* ^{α} *Q* ^{0}

^{α}

^{0}

^{then}

^{for}

^{some}

*P* ^{0} *∈ P*

^{0}

^{,}

*P* *−→* ^{α} *P* ^{0}

^{α}

^{0}

^{and}

### (P ^{0} *, Q* ^{0} ) *∈ R*

^{0}

^{0}

^{.}

We will let

*∼*

^{denote}

^{the}

^{greatest}bisimulation and say that

*P*

^{and}

*Q*

^{are}

^{equivalent}

^{or}

bisimilar if

*P* *∼* *Q*

^{.}

^{We}

^{will}

^{use}

^{the}

^{shorthand}

^{notation}

*P* *−→* ^{s} *P* ^{0}

^{s}

^{0}

^{if}

*s* ^{def} = *a* _{1} *a* _{2} *· · ·* *a* *n*

^{def}

^{,}

*a* *i* *∈ A* *ct*

^{and}

^{there}

^{exists}

^{a}

^{sequence}

^{of}

^{states}

*P* _{1} *, P* _{2} *, . . . , P* *n* *∈ P*

^{such}

^{that}

*P* *−→* ^{a} ^{1} *P* _{1} *−→* ^{a} ^{2}

^{a}

^{a}

*· · ·* *−→* ^{a} ^{n} *P* *n*

^{a}

^{n}

^{and}

*P* ^{0} = *P* *n*

^{0}

^{.}

^{F}urthermore,wedene thelabelscontainedin astateasn

### (P ) = *{α* *∈ Act* *| ∃s* _{1} *, s* _{2} *∈ Act* ^{∗} *.(* *∃P* ^{0} *∈ P.P* ^{s} *−→* ^{1} ^{αs} ^{2} *P* ^{0} ) *}*

^{∗}

^{0}

^{s}

^{αs}

^{0}

^{.}

Nowweshowhowapartitionrenementalgorithmcanbeusedforbisimulationchecking.

Ifrene

### (U, *W, f* _{1} *, . . . , f* *k* )

^{is}

^{a}

^{function}

^{which}

^{returns}

^{a}

^{solution}

^{of}

^{the}generalizedpartition renement problem for the instance

*U,* *W, f* 1 *, . . . , f* *k*

^{then}

^{it}

^{can}

^{be}

^{used}

^{for}

^{checking}

^{for}

bisimilaritybetweenthestates

*P*

^{and}

*Q*

^{as}

^{follows.}

^{Let}

*S* *P*

^{denote}

^{the}

^{state}

^{space}

^{of}

*P*

^{,}

^{i.e.}

*S* *P* = *{P* ^{0} *| ∃s* *∈ Act* ^{∗} *.P* *−→* ^{s} *P* ^{0} *}*

^{0}

^{∗}

^{s}

^{0}

^{.}

^{Let}

*U*

^{be}

^{the}

^{set}

*S* *P* *∪* *S* *Q*

^{and}

*W*

^{the}

^{parti-}

tion of

*U*

^{containing}

^{only}

^{one}

^{block}

^{which}

^{is}

^{the}

^{set}

*U*

^{.}Furthermore, let the functions

*f* *α* : *U* *→ P* (U )

^{,}

*α* *∈*

^{n}

### (P ) *∪*

^{n}

### (Q)

^{be}

^{dened}

^{as}

*f* *α* (R) = *{R* ^{0} *∈* *U* *|* *R* *−→* ^{α} *R* ^{0} *}*

^{0}

^{α}

^{0}

^{.}

*P*

^{and}

*Q*

are bisimilarifandonlyiftheyarein thesameblockoftherened partition

*W* ^{0}

^{0}

^{returned}

from rene

### (U, *W* *,* *{* *f* *α* *}* _{(} *α* *∈*

^{n}

### ( *P* )∪

^{n}

### ( *Q* )) )

^{.}

^{This}

^{is}

^{true}

^{since}

*∼*

^{gives}

^{rise}

^{to}

^{a}

^{partition}

*W* ^{00}

^{00}

^{of}

*U*

^{where}

^{the}

^{blocks}

^{are}

^{the}equivalenceclassesof

*∼ ∩* (U *×* *U* )

^{.}

*W* ^{00}

^{00}

^{is}

^{clearly}

^{a}

^{xed}

^{point}

of

*ψ* _{W}

_{W}

^{.}

^{If}

*W* ^{00}

^{00}

^{is}

^{not}

^{the}

^{same}

^{as}

*W* ^{0}

^{0}

^{,}

^{i.e.}

^{the}

^{greatest}

^{xed}

^{point}

^{of}

*ψ* _{W}

_{W}

^{,}

^{there}

^{exists}

^{a}

bisimulation

*∼ ∪W* _{∼} ^{0}

_{∼}

^{0}

^{larger}

^{than}

*∼*

^{,}

^{which}

^{is}

^{a}contradiction.

The

*π*

^{-Calculus}

In this chapter we presentthe notionof late andearly bisimulationfor asubsetof the

*π*

^{-}

calculus and describe some of the problems associated with algorithmic checking for late

andearlybisimilarity. First,wegivethesyntaxandsemanticsofasubsetofthe

*π*

^{-calculus.}

3.1 Syntax

Webeginbygivingthesyntaxforasubsetofthe

*π*

^{-calculus.}

^{The}

^{syntactic}

^{categories}

^{for}

^{the}

*π*

^{-calculus}

^{are:}

^{an}

^{innite}

^{set}

^{of}

^{names,}

*N*

^{,}

^{a}

^{set}

^{of}

^{actions,}

*Act*

^{,}

^{an}

^{innite}

^{set}

^{of}

^{process}

identiers,

*K*

^{,}

^{and}

^{a}

^{set}

^{of}

*π*

^{-processes}

^{,}

*Pr*

^{.}

^{We}

^{will}

^{denote}

^{elements}

^{of}

*N*

^{by}

*a, b*

^{,}

*c*

^{,}

*d*

^{,}

*e*

^{,}

*v*

^{,}

*x*

^{,}

^{and}

*y*

^{,}

^{elements}

^{of}

*Act*

^{by}

*α*

^{and}

*β*

^{,}

^{elements}

^{of}

*K*

^{by}

*K*

^{,}

^{and}

^{elements}

^{of}

*Pr*

by

*P*

^{and}

*Q*

^{.}

^{The}

^{set}

^{of}

^{processes}

^{can}

^{be}constructedwith theconstructorsfor inaction, prex,matching, nondeterministic choice,parallel composition, restriction, and

recursion,andanactioncanbeasilentaction,input,free output,orboundoutput.

Thegrammarfor

*Act*

^{and}

*Pr*

^{is}

^{presented}

^{below.}

*α* ::= *τ* *|* *a(b)* *|* ¯ *ab* *|* ¯ *a(b)*

*P* ::= **0** *|* *α.P* *|* [a = *b]P* *|* *P* + *P* *|* *P* *|* *P* *|* (ν a)P *|* *K* *h* ˜ *a* *i*

Each process identier

*K*

^{has}

^{an}

^{associated}

^{arity}

^{and}

^{a}

^{denition}

^{of}

^{the}

^{form}

*K* ^{def} = (˜ *b)P*

^{def}

^{,}

where

### ˜ *b*

^{are}

^{the}

^{free}

^{names}

^{of}

*P*

^{(see}

^{denition}

^{4).}

^{For}

^{the}

^{process}

*K* *h* ˜ *a* *i*

^{the}

^{tuple}

*a* ˜

^{must}

havethesamelengthas

### ˜ *b*

^{.}

^{The}

^{free,}

^{bound}

^{,}

^{extruded,}

^{object,}

^{and}

^{subject}

^{names}

^{of}

^{an}

action

*α*

^{,}

^{written}

^{fn}

### (α)

^{,}

^{bn}

### (α)

^{,}

^{en}

### (α)

^{,}

^{ob}

### (α)

^{,}

^{and}

^{sub}

### (α)

^{,}respectively,aredenedasfollows.

*α*

^{fn}

### (α)

^{bn}

### (α)

^{en}

### (α)

^{ob}

### (α)

^{sub}

### (α)

*τ* *∅* *∅* *∅* *∅* *∅*

*a(b)* *{a}* *{b}* *∅* *{a}* *{b}*

### ¯ *ab* *{a, b}* *∅* *∅* *{a}* *{b}*

### ¯

*a(b)* *{a}* *{b}* *{b}* *{a}* *{b}*

The names of an action

*α*

^{are}

^{the}

^{free}

^{names}

^{and}

^{the}

^{bound}

^{names}

^{of}

*α*

^{,}

^{i.e.}

^{n}

### (α) =

fn

### (α) *∪*

^{bn}

### (α)

^{.}

^{The}

^{free}

^{and}

^{bound}

^{names}

^{of}

^{a}

^{process}

^{are}

^{dened}

^{as}

^{follows.}

Denition 4 (FreeNames)

Aname

*a*

^{is}

^{free}

^{in}

^{the}

^{process}

*P*

^{,}

^{written}

*a* *∈*

^{fn}

### (P )

^{,}

^{if}

^{it}

^{belongs}

^{to}

^{the}

^{set}

^{free}

### (P )

^{,}

^{where}

thefunction free

### : *Pr* *→ P* ( *N* )

^{is}

^{dened}

^{by}

^{the}

^{following.}

free

### ( **0** ) = *∅*

free

### (α.P ) =

^{fn}

### (α) *∪* (

^{free}

### (P ) *\*

^{bn}

### (α))

free

### ([a = *b]P* ) = *{a, b} ∪*

^{free}

### (P)

free

### (P _{1} *|P* _{2} ) =

^{free}

### (P _{1} ) *∪*

^{free}

### (P _{2} )

free

### (P _{1} + *P* _{2} ) =

^{free}

### (P _{1} ) *∪*

^{free}

### (P _{2} )

free

### ((ν a)P) =

^{free}

### (P ) *\ {a}*

free

### (K *h* (a _{1} *, a* _{2} *, . . . , a* *n* ) *i* ) = *{* *a* _{1} *, a* _{2} *, . . . , a* *n* *}*

Denition 5 (BoundNames)

A name

*a*

^{is}

^{bound}

^{in}

^{the}

^{process}

*P*

^{,}

^{written}

*a* *∈*

^{bn}

### (P)

^{,}

^{if}

^{it}

^{belongs}

^{to}

^{the}

^{set}

^{bound}

### (P )

^{,}

where thefunction bound

### : *P* *r* *→ P* ( *N* )

^{is}

^{the}

^{least}

^{function}

^{that}

^{satises}

^{the}

^{following.}

bound

### ( **0** ) = *∅*

bound

### (α.P ) =

^{bn}

### (α) *∪*

^{bound}

### (P )

bound

### ([a = *b]P* ) =

^{bound}

### (P )

bound

### (P _{1} *|P* 2 ) =

^{bound}

### (P _{1} ) *∪*

^{bound}

### (P _{2} )

bound

### (P _{1} + *P* _{2} ) =

^{bound}

### (P _{1} ) *∪*

^{bound}

### (P _{2} )

bound

### ((ν a)P ) = *{* *a* *} ∪*

^{bound}

### (P )

bound

### (Kh (˜ *a)* *i* ) =

^{bound}

### (P )

^{where}

*K* ^{def} = (˜ *b)P*

^{def}

Thenames ofaprocess

*P*

^{,}

^{written}

^{n}

### (P )

^{,}

^{consists}

^{of}

^{the}

^{free}

^{names}

^{and}

^{the}

^{bound}

^{names}

of

*P*

^{,}

^{i.e.}

^{n}

### (P ) =

^{fn}

### (P ) *∪*

^{bn}

### (P )

^{.}

^{We}

^{sometimes}

^{write}

^{fn}

### (P _{1} *, P* _{2} *, . . . , P* *n* )

^{for}

^{fn}

### (P _{1} ) *∪*

^{fn}

### (P _{2} ) *∪*

*· · · ∪*

^{fn}

### (P *n* )

^{,}

^{and}

^{similarly}

^{for}

^{bound}

^{names}

^{and}

^{names.}

Weidentifyprocessesuptorenamingofboundnames. Renamingofaboundnameina

processiscalled

*α*

-conversion. Iftheprocesses*P*

^{and}

*Q*

^{can}

^{be}

^{identied}

^{up}

^{to}

^{renaming}

ofboundnamesthen

*P*

^{and}

*Q*

^{are}

*α*

-convertible,written *P* *≡* *α* *Q*

^{.}

Denition 6 (

*α*

-conversion)
*α*

-conversionof aname *a*

^{to}

^{a}

^{name}

*b*

^{in}

^{a}

*π*

^{-process}

*P*

^{,}

^{where}

*b /* *∈*

^{n}

### (P )

^{,}

^{is}

^{the}

^{result}

^{of}

renamingallbound occurrencesof

*a*

^{in}

*P*

^{to}

*b*

^{.}

Substitutions are denoted by

*σ*

^{and}

^{are}

^{functions}

^{that}

^{map}

^{names}

^{to}

^{names,}

^{e.g.}

*σ* ^{def} = *{y* _{1} */x* _{1} *y* _{2} */x* _{2} *· · ·* *y* *n* */x* *n* *}*

^{def}

^{denotes}

^{the}simultaneous substitution that maps every freeoccurrenceofthename

*x* *i*

^{to}

^{the}

^{name}

*y* *i*

^{for}

^{all}

*i* *∈ {* 1, 2, . . . , n}

^{.}

^{A}

^{name}

*a*

^{is}

^{neutral}

for asubstitution

*σ*

^{if}

^{for}

^{all}

*b* *∈ N*

^{,}

*σ(b) =* *a*

^{if}

^{and}

^{only}

^{if}

*b* = *a*

^{.}

^{A}

^{set}

^{of}

^{names,}

*V*

^{,}

is neutral for asubstitution

*σ*

^{if}

^{all}

^{the}

^{names}

^{of}

*V*

^{are}

^{neutral}

^{for}

*σ*

^{.}Application of a substitution

*σ*

^{to}

^{a}

^{process}

*P*

^{is}

^{written}

*P σ*

^{.}

^{If}

^{there}

^{exists}

^{some}

^{bound}

^{name}

*a*

^{in}

*P*

^{such}

thatthesubstitution

*σ*

^{maps}

^{some}

^{name}

^{to}

*a*

^{then}

*a*

^{is}

*α*

^{-converted}

^{to}

^{some}

*b*

^{that}

^{is}

^{neutral}

for

*σ*

^{.}

3.2 Semantics

Theoperationalsemanticsforthesubsetofthe

*π*

^{-calculus}

^{is}

^{given}

^{by}

^{the}

^{labeled}

^{transition}

system(

*P* *r*

^{,}

*Act*

^{,}

*→*

^{)}

^{where}

*→*

^{is}

^{the}

^{smallest}

^{relation}

^{closed}

^{under}

^{the}

^{rules}

^{in}

^{table}

^{3.1.}

^{The}

symmetricversionsofthe rulesSum,Par,Com,andClosehavebeenomitted. Transitions

havetheform

*P* *−→* ^{α} *P* ^{0}

^{α}

^{0}

^{.}

### [

^{Alpha}

### ] *P* ^{0} *−→* ^{α} *P* ^{00}

^{0}

^{α}

^{00}

*P* *−→* ^{α} *P* ^{00} *P* *≡* *α* *P* ^{0} [

^{α}

^{00}

^{0}

^{Pre}

### ]

*α.P* *−→* ^{α} *P*

^{α}

### [

^{Con}

### ] *P* *{* ˜ *a/* ˜ *b* *}* *−→* ^{α} *P* ^{0}

^{α}

^{0}

*K* *h* ˜ *a* *i* *−→* ^{α} *P* ^{0} *K* ^{def} = (˜ *b)P* [

^{α}

^{0}

^{def}

^{Sum}

### ] *P* *−→* ^{α} *P* ^{0} *P* + *Q* *−→* ^{α} *P* ^{0}

^{α}

^{0}

^{α}

^{0}

### [

^{Par}

### ] *P* *−→* ^{α} *P* ^{0}

^{α}

^{0}

*P* *|Q* *−→* ^{α} *P* ^{0} *|Q*

^{α}

^{0}

^{bn}

### (α) *∩*

^{fn}

### (Q) = *∅* [

^{Com}

### ] *P* *−→* ^{¯} ^{ay} *P* ^{0} *Q* *−→* ^{a} ^{(} ^{x} ^{)} *Q* ^{0} *P* *|Q* *−→* ^{τ} *P* ^{0} *|Q* ^{0} *{y/x}*

^{ay}

^{0}

^{a}

^{x}

^{0}

^{τ}

^{0}

^{0}

### [

^{Close}

### ] *P* ^{a} *−→* ^{¯} ^{(} ^{x} ^{)} *P* ^{0} *Q* *−→* ^{a} ^{(} ^{x} ^{)} *Q* ^{0}

^{a}

^{x}

^{0}

^{a}

^{x}

^{0}

*P* *|Q* *−→* ^{τ} (ν x)(P ^{0} *|Q* ^{0} ) [

^{τ}

^{0}

^{0}

^{Match}

### ] *P* *−→* ^{α} *P* ^{0} [a = *a]P* *−→* ^{α} *P* ^{0}

^{α}

^{0}

^{α}

^{0}

### [

^{Res}

### ] *P* *−→* ^{α} *P* ^{0}

^{α}

^{0}

### (ν b)P *−→* ^{α} (ν b)P ^{0} *b /* *∈*

^{α}

^{0}

^{n}

### (α) [

^{Open}

### ] *P* *−→* ^{¯} ^{ab} *P* ^{0} (ν b)P *−→* ^{¯} ^{a} ^{(} ^{b} ^{)} *P* ^{0}

^{ab}

^{0}

^{a}

^{b}

^{0}

*b* *6* = *a*

Table3.1: Operationalsemanticsforthe

*π*

^{-calculus.}

3.3 Bisimulation

In this section wedene the notionof late bisimulation and early bisimulation rst

introducedby[5].

A symmetricbinaryrelation

*R*

^{on}

^{processes}

^{is}

^{a}

^{late}bisimulationif

*P* *R* *Q*

^{and}

*P* *−→* ^{α} *P* ^{0}

^{α}

^{0}

where bn

### (α) *∩* (

^{fn}

### (P ) *∪*

^{fn}

### (Q)) = *∅*

^{implies}

(i) if

*α* = *a(x)*

^{then}

*∃Q* ^{0} *.(Q* *−→* ^{a} ^{(} ^{x} ^{)} *Q* ^{0} *∧ ∀y.(P* ^{0} *{y/x} R* *Q* ^{0} *{y/x}* ))

^{0}

^{a}

^{x}

^{0}

^{0}

^{0}

^{,}

^{and}

(ii) if

*α* *6* = *a(x)*

^{then}

*∃Q* ^{0} *.(Q* *−→* ^{α} *Q* ^{0} *∧* *P* ^{0} *R* *Q* ^{0} )

^{0}

^{α}

^{0}

^{0}

^{0}

^{.}

Fromthedenition oflatebisimulationthenotionof late bisimilarity isdened.

Denition 8 (LateBisimilarity)

Theprocesses

*P*

^{and}

*Q*

^{are}

^{late}

^{bisimilar,}

^{written}

*P* *∼* ˙ *Q*

^{,}

^{if}

^{there}

^{exists}

^{a}

^{late}bisimulation

*R*

^{such}

^{that}

*P* *R* *Q*

^{.}

Asanexampleoftwolatebisimilarprocessesconsider

*a(x).0* *|* ¯ *by.0*

^{and}

*a(x).* ¯ *by.0* +¯ *by.a(x).0*

^{.}

Itis easilyseenthat

*a(x).0* *|* ¯ *by.0* *∼* ˙ *a(x).* ¯ *by.0* + ¯ *by.a(x).0*

^{.}

It turns out that with the operational semantics dened it is hard to give anecient

algorithmforcheckinglatebisimilaritybetweenprocesses.Supposeweneedtocheckwhether

the processes

*P*

^{and}

*Q*

^{are}

^{late}

^{bisimilar.}

^{If}

*P*

^{has}

^{the}

^{transition}

*P* *−→* ^{a} ^{(} ^{x} ^{)} *P* ^{0}

^{a}

^{x}

^{0}

^{,}

^{that}

^{is}

*P*

^{can}

receivesomethingonthechannel

*a*

^{and}

^{become}

*P* ^{0}

^{0}

^{,}

^{we}

^{can}

^{only}

^{explore}transitionsfrom

*P* ^{0}

^{0}

byexaminingallthepossiblesubstitutionsof

*x*

^{in}

*P* ^{0}

^{0}

^{and}

^{there}

^{are}

^{innitely}

^{many}

^{of}

^{these.}

Similarproblemsariseforearly bisimilarity basedonthelatesemanticsgivenbythe

labeledtransition systemoftable3.1. Early bisimulation isdenedasfollows.

Denition 9 (EarlyBisimulation)

Asymmetricbinaryrelation

*R*

^{on}

^{processes}

^{is}

^{an}

^{early}bisimulationif

*P* *R* *Q*

^{and}

*P* *−→* ^{α} *P* ^{0}

^{α}

^{0}

where bn

### (α) *∩* (

^{fn}

### (P ) *∪*

^{fn}

### (Q)) = *∅*

^{implies}

(i) if

*α* = *a(x)*

^{then}

*∀y.(* *∃Q* ^{0} *.(Q* *−→* ^{a} ^{(} ^{x} ^{)} *Q* ^{0} *∧* *P* ^{0} *{y/x} R* *Q* ^{0} *{y/x}* ))

^{0}

^{a}

^{x}

^{0}

^{0}

^{0}

^{,}

^{and}

(ii) if

*α* *6* = *a(x)*

^{then}

*∃* *Q* ^{0} *.(Q* *−→* ^{α} *Q* ^{0} *∧* *P* ^{0} *R* *Q* ^{0} )

^{0}

^{α}

^{0}

^{0}

^{0}

^{.}

Fromthedenition ofearlybisimulationthenotionofearlybisimilarityisdened.

Denition 10 (Early Bisimilarity)

Theprocesses

*P*

^{and}

*Q*

^{are}

^{early}

^{bisimilar,}

^{written}

*P* *∼* ˙ *E* *Q*

^{,}

^{if}

^{there}

^{exists}

^{an}

^{early}

^{bisim-}

ulation

*R*

^{such}

^{that}

*P* *R* *Q*

^{.}

constructorinputprex.

Inthenextsectionanalternativeoperationalsemanticsandthedenitionofopenbisimi-

larityisgiven. Thesemakeitpossibletodevelopamoreecientbisimulationcheckingalgo-

rithm. Themainreasonsforusingthedenitionofopenbisimilarityinourimplementation

of abisimulation checkeris that openbisimilarityisacongruenceand thatabisimulation

checkingalgorithmfor lateorearly bisimulationcanbeextractedfrom theopenbisimula-

tioncheckingalgorithm[10]. Furthermore,thedenitionofopenbisimilaritywasalsoused

in theMobilityWorkbenchandwehope[7]maybenetfromourimplementation.

Algorithm for Checking Open

Bisimilarity in the

*π*

^{-Calculus}

In thischapter wepresent thenotionof openbisimulationfor the

*π*

^{-calculus}

^{and}

^{describe}

some of the problems associated with algorithmic checkingfor open bisimilarity. Finally,

we present some results from [10] that make algorithmic checking for open bisimilarity

possible. First,wepresentsomebasicnotionsneededforthesemanticsspecializedforopen

bisimulationandthedenitionofopenbisimulation. All lemmas,theorems,andcorollaries

presentedin thischapterareprovenin[10].

4.1 Syntax

We assumethesamesyntaxasin thepreviouschapter exceptfor thefact that weimpose

a strict ordering,

*<*

^{,}

^{on}

^{the}

^{set}

^{of}

^{names,}

*N*

^{,}

^{and}

^{that}

^{there}

^{exists}

^{a}

^{smallest}

^{name}

^{with}

respectto

*<*

^{.}Furthermore,weintroducethenotionsof conditionsanddistinctions.

Welet

*M*

^{denote}

^{the}

^{set}

^{of}

^{all}conditions. Conditionsare rangedoverby

*L*

^{,}

*M*

^{,}

^{and}

*N*

^{and}

^{are}

^{nite}conjunctionsofmatching, e.g.

### [a = *b][c* = *d]*

^{is}

^{the}

^{condition}

^{that}

^{equates}

*a*

^{with}

*b*

^{and}

*c*

^{with}

*d*

^{.}

^{The}

^{names}

^{of}

^{a}

^{condition}

*M*

^{,}

^{written}

^{n}

### (M )

^{,}

^{are}

^{the}

^{names}

^{that}

appearin

*M*

^{.}Compositionof twoconditions

*M*

^{and}

*N*

^{is}

^{written}

*M N*

^{.}

^{If}

^{every}

^{match}

^{of}

acondition,

*N*

^{,}

^{is}

^{implied}

^{by}

^{another}

^{condition,}

*M*

^{,}

^{we}

^{write}

*M* B *N*

^{.}

^{If}

^{it}

^{is}

^{also}

^{the}

^{case}

that noteverymatchofthecondition

*M*

^{is}

^{implied}

^{by}

*N*

^{we}

^{write}

*M* 6B *N*

^{.}

^{The}

^{trivially}

trueconditionisdenoted by

*∅*

^{.}

^{The}substitution

*σ* *M*

^{induced}

^{by}

^{a}

^{condition}

*M*

^{maps}

^{each}

elementofeachequivalenceclassof

*M*

^{to}

^{the}

^{smallest}

^{element}

^{of}

^{that}equivalenceclass,i.e.

*σ* *M* (a) =

^{min}

*{b* *|* *M* B [a = *b]* *}*

^{.}

^{To}

^{facilitate}

^{the}

^{evaluation}

^{of}

^{the}

^{expression}

*M* B *N*

^{,}

^{for}

someconditions

*M*

^{and}

*N*

^{,}

^{conditions}

^{are}transformedtoacanonical form.

Thecanonicalform ofacondition

*M*

^{is}

^{the}

^{condition}

*M* *c* = [a _{1} = *b* _{1} ][a _{2} = *b* _{2} ] *· · ·* [a *n* = *b* *n* ]

where

(i) forall

*a* *∈*

^{n}

### (M )

^{with}

*a* *6* = *σ* *M* (a)

^{it}

^{holds}

^{that}

### [a = *σ* *M* (a)] *∈* *M* *c*

^{,}

(ii)

*a* *i* *6* = *b* *i*

^{and}

^{either}

*b* *i* *< b* *i* +1

^{or}

*b* *i* = *b* *i* +1

^{and}

*a* *i* *< a* *i* +1

^{,}

^{and}

(iii)

*M . M* *c*

^{.}

The canonical form is dened in such a way that if

*M*

^{and}

*N*

^{are}

^{conditions}

^{such}

^{that}

*M* CB *N*

^{then}

*M* *c*

^{is}syntacticallyequalto

*N* *c*

^{,}

^{where}

*M* *c*

^{and}

*N* *c*

^{are}

^{the}

^{canonical}

^{forms}

of

*M*

^{and}

*N*

^{.}

Welet

*D* *is*

^{denote}

^{the}

^{set}

^{of}

^{all}distinctions. Distinctionsarenite binarysymmetric irreexiverelationson names

*N*

^{and}

^{are}

^{ranged}

^{over}

^{by}

*D*

^{and}

*E*

^{.}

^{If}

### (a, b) *∈* *D*

^{for}

^{some}

distinction

*D*

^{then}

^{the}

^{two}

^{names}

*a*

^{and}

*b*

^{must}

^{be}

^{distinct,}

^{i.e.}

*a* *6* = *b*

^{.}

^{The}

^{names}

^{of}

*D*

^{,}

writtenn

### (D)

^{,}

^{are}

^{the}

^{names}

^{that}

^{appear}

^{in}

*D*

^{.}

^{A}substitution

*σ*

^{respects}

*D*

^{if}

*σ(a)* *6* = *σ(b)*

for all

### (a, b) *∈* *D*

^{.}

^{Likewise,}

^{a}

^{condition}

*M*

^{respects}

^{the}distinction

*D*

^{if}

^{the}substitution,

*σ* *M*

^{,}

^{induced}

^{by}

*M*

^{respects}

*D*

^{.}

^{Let}

*F* *⊆ N*

^{then}

*D* *−* *F*

^{denotes}

^{the}distinction

*{* (a, b) *∈* *D* *|* *a, b /* *∈* *F* *}*

^{and}

*D* *∩* *F*

^{denotes}

^{the}distinction

*{* (a, b) *∈* *D* *|* *a, b* *∈* *F* *}*

^{.}

^{In}

^{the}

^{denition}

^{of}

^{a}

distinctionwewillnotalwaysgiveallsymmetricpairs,e.g. in

*D* ^{def} = *{* (a, b) *}*

^{def}

^{the}

^{pair}

### (b, a)

hasbeenleftout.

4.2 Semantics

Inthissectionwegiveasymbolicsemanticsspecializedforopenbisimulationforthesubset

of the

*π*

^{-calculus.}

^{A}

^{symbolic}

^{semantics}

^{is}

^{used}

^{to}

^{avoid}

^{the}

^{innite}

^{branching}

^{that}

^{could}

occur with a traditional semantics when exploring the transitions of processes containing

input prexes. To see why an innite branching can occur consider the process

*a(x).P*

with the transition

*a(x).P* *−→* ^{a} ^{(} ^{x} ^{)} *P*

^{a}

^{x}

^{.}

^{T}

^{o}

^{explore}

^{the}

^{further}transitions of

*P*

^{we}

^{have}

^{to}

explorethebehaviorof

*P* *{y/x}*

^{for}

^{innitely}

^{many}

*y*

^{s.}

^{The}

^{notion}

^{of}

^{symbolic}

^{semantics}

^{for}

the

*π*

^{-calculus}

^{was}

^{rst}

^{introduced}

^{by}

^{[1].}

^{The}operationalsemantics specialized for open bisimulationis givenby thesymboliclabeledtransition system(

*Pr*

^{,}

*M × Act*

^{,}

^{),}

^{where}

isthesmallestrelationclosedundertherulesintable4.1. Thesymmetricversionsofthe

rulesSum, Par,Com,andClose havebeenomitted. Transitionshavetheform

*P* ^{(} ^{M,α} ^{)} *P* ^{0}

^{M,α}

^{0}

^{,}

where

*M*

^{represents}

^{the}

^{minimal}

^{condition}

^{required}

^{for}

*P*

^{to}

^{perform}

^{the}

^{action}

*α*

^{.}

^{We}

^{let}

*µ*

^{range}

^{over}

*M × Act*

^{.}

### [

^{Alpha}

### ] *P* ^{0} ^{µ} *P* ^{00}

^{0}

^{µ}

^{00}

*P* ^{µ} *P* ^{00} *P* *≡* *α* *P* ^{0} [

^{µ}

^{00}

^{0}

^{Pre}

### ]

*α.P* ^{(∅} ^{,α} ^{)} *P* [

^{,α}

^{Con}

### ] *P{* ˜ *a/* ˜ *b}* ^{µ} *P* ^{0}

^{µ}

^{0}

*Kh* ˜ *ai* ^{µ} *P* ^{0} *K* ^{def} = (˜ *b)P*

^{µ}

^{0}

^{def}

### [

^{Sum}

### ] *P* ^{µ} *P* ^{0}

^{µ}

^{0}

*P* + *Q* ^{µ} *P* ^{0} [

^{µ}

^{0}

^{Par}

### ] *P* ^{µ} *P* ^{0}

^{µ}

^{0}

*P|Q* ^{µ} *P* ^{0} *|Q*

^{µ}

^{0}

^{bn}

### (µ) *∩*

^{fn}

### (Q) = *∅*

### [

^{Com}

### ] *P* ^{(} ^{M,} ^{¯} ^{ay} ^{)} *P* ^{0} *Q* ^{(} ^{N,b} ^{(} ^{x} ^{))} *Q* ^{0} *P* *|Q* ^{(} ^{L,τ} ^{)} *P* ^{0} *|Q* ^{0} *{y/x}*

^{M,}

^{ay}

^{0}

^{N,b}

^{x}

^{0}

^{L,τ}

^{0}

^{0}

where

*L* ^{def} = *M N[a* = *b]*

^{def}

### [

^{Close}

### ] *P* ^{(} ^{M,} ^{¯} ^{a} ^{(} ^{x} ^{))} *P* ^{0} *Q* ^{(} ^{N,b} ^{(} ^{x} ^{))} *Q* ^{0} *P* *|Q* ^{(} ^{L,τ} ^{)} (ν x)(P ^{0} *|Q* ^{0} )

^{M,}

^{a}

^{x}

^{0}

^{N,b}

^{x}

^{0}

^{L,τ}

^{0}

^{0}

where

*L* ^{def} = *M N* [a = *b]*

^{def}

### [

^{Match}

### ] *P* ^{(} ^{M,α} ^{)} *P* ^{0} [a = *b]P* ^{(} ^{N,α} ^{)} *P* ^{0}

^{M,α}

^{0}

^{N,α}

^{0}

where

*N* ^{def} = *M* [a = *b]*

^{def}

### [

^{Res}

### ] *P* ^{µ} *P* ^{0}

^{µ}

^{0}

### (ν b)P ^{µ} (ν b)P ^{0} *b /* *∈*

^{µ}

^{0}

^{n}

### (µ)

### [

^{Open}

### ] *P* ^{(} ^{M,} ^{¯} ^{ab} ^{)} *P* ^{0} (ν b)P ^{(} ^{M,} ^{¯} ^{a} ^{(} ^{b} ^{))} *P* ^{0}

^{M,}

^{ab}

^{0}

^{M,}

^{a}

^{b}

^{0}

*b /* *∈*

^{n}

### (M ) *∪ {a}*

Table4.1: Thespecializedoperationalsemanticsforthe

*π*

^{-calculus.}

From the transition system given by the rules in table 4.1 we dene another transition

system,

### ( *P* *r,* *M × A* *ct,* *−→* )

^{,}

^{such}

^{that}

^{the}

^{condition}

*M*

^{of}

^{a}

^{transition}

*P* ^{(} ^{M,α} *−→* ^{)} *P* ^{0}

^{M,α}

^{0}

^{is}

^{in}

canonical form and

*α*

^{and}

*P* ^{0}

^{0}

^{are}

^{closed}

^{under}

^{the}substitution

*σ* *M*

^{,}

^{i.e.}

*α* = *ασ* *M*

^{and}

*P* ^{0} = *P* ^{0} *σ* *M*

^{0}

^{0}

^{.}

^{The}

^{relation}

*−→*

^{is}

^{the}

^{smallest}

^{relation}

^{closed}

^{under}

^{the}

^{following}

^{rule.}

### [

^{Canon}

### ] *P* ^{(} ^{N,α} ^{)} *P* ^{0} *P* ^{(} ^{M,ασ} *−→* ^{M} ^{)} *P* ^{0} *σ* *M*

^{N,α}

^{0}

^{M,ασ}

^{M}

^{0}

bn

### (α) *∩*

^{fn}

### (P ) = *∅*

^{and}

*M*

^{is}

^{the}

^{canonical}

^{form}

^{of}

*N*

4.3 Open Bisimulation

In this section wegivethe denition of open bisimulation. Firstweneed to dene the

notionof distinction-indexed relation.

Denition 12 (Distinction-Indexed Relation)

Adistinction-indexedrelation

*R*

^{is}

^{a}

^{set}

*{R* *D* *}* *D*

^{of}

^{relations}

*R* *D*

^{over}

*π*

-processes,where*D*

rangesoveralldistinctionsin

*D* *is*

^{.}

Denition 13 (OpenBisimulation)

Adistinction-indexed relation

*R*

^{is}

^{an}

^{open}bisimulationif

*P* *R* *D* *Q*

^{implies}

(i) forall

*M*

^{,}

*α*

^{,}

^{and}

*P* ^{0}

^{0}

^{such}

^{that}

*P* ^{(} *−→* ^{M,α} ^{)} *P* ^{0}

^{M,α}

^{0}

^{,}

^{with}

^{bn}

### (α) *∩*

^{fn}

### (Q, D) = *∅*

^{and}

*M*

^{respects}

*D*

^{,}

^{there}

^{exist}

^{some}

*N*

^{,}

*β*

^{,}

^{and}

*Q* ^{0}

^{0}

^{such}

^{that}

*Q* ^{(} *−→* ^{N,β} ^{)} *Q* ^{0}

^{N,β}

^{0}

^{and}

*M* B *N*

^{,}

*α* = *βσ* *M*

^{,}

^{and}

*P* ^{0} *R* *D* ^{0} *Q* ^{0} *σ* *M*

^{0}

^{0}

^{0}

^{for}

*D* ^{0} ^{def} = (D *∪* (

^{0}

^{def}

^{en}

### (α) *×*

^{fn}

### (P, Q)))σ *M*

^{,}

^{and}

(ii) theconverse,withtheroleof

*P*

^{and}

*Q*

^{exchanged.}

Fromthedenition ofopenbisimulationwedenethenotionof open bisimilarity.

Denition 14 (Openbisimilarity)

Theprocesses

*P*

^{and}

*Q*

^{are}

^{open}

^{bisimilar}

^{with}

^{respect}

^{to}distinction

*D*

^{,}

^{written}

*P* *∼* *D* *Q*

^{,}

if

*P* *R* *D* *Q*

^{for}

^{some}

^{open}bisimulation

*R*

^{.}

Asitisseenindenition13thedistinction

*D* ^{0}

^{0}

^{is}

*D*

^{updated}

^{with}

^{the}

^{fact}

^{that}

^{the}

^{extruded}

namesof theaction

*α*

^{must}

^{be}

^{dierent}

^{from}

^{all}

^{free}

^{names}

^{in}

^{the}

^{processes}

*P*

^{and}

*Q*

^{and}

afterwardsupdated byapplying

*σ* *M*

^{to}

^{it.}

^{Since}

^{this}

^{kind}

^{of}

^{updating}

^{of}distinctionswill oftenbeused inthefollowing,wewilluseashorternotationdenedasfollows.

Let

*D*

^{be}

^{a}distinction,

*P* _{1} *, . . . , P* *n*

^{processes,}

*M*

^{a}

^{condition,}

^{and}

*α*

^{an}

^{action.}

^{Then}

^{we}

dene

*D* ^{M} _{(} _{P} _{1} _{,...,P} _{n} _{)} _{,α}

^{M}

_{P}

_{,...,P}

_{n}

_{,α}

^{as}

*D* ^{M} _{(} _{P} _{1} _{,...,P} _{n} _{)} _{,α} ^{def} = (D *∪* (

^{M}

_{P}

_{,...,P}

_{n}

_{,α}

^{def}

^{en}

### (α) *×*

^{fn}

### (P _{1} *, . . . , P* *n* )))σ *M*

With thisdenition

*D* ^{0}

^{0}

^{in}

^{denition}

^{13}

^{could}

^{be}

^{written}

^{as}

*D* _{(} ^{M} _{P,Q} _{)} _{,α}

^{M}

_{P,Q}

_{,α}

^{.}

Touse themethod described in chapter 2to check whether

*P* *∼* *D* *Q*

^{it}

^{is}

^{necessary}

^{to}

generate thestate spacesof

*P*

^{and}

*Q*

separately. This cannotbedone sincethe following
dependenciesbetween*P*

^{and}

*Q*

^{aect}

^{the}transitionsandthederivatives.

Dependency1 Thenameemittedby

*P*

^{may}

^{not}

^{occur}

^{free}

^{in}

*Q*

^{.}

Dependency2 Thesubstitution

*σ* *M*

^{determined}

^{by}

^{the}

^{condition}

*M*

^{in}

^{a}

^{transition}

^{of}

*P*

mustbeappliedto thederivativeof

*Q*

^{.}

Dependency3 There isaglobaldistinction,whichisupdatedusingthefreenamesfrom

bothprocesses.

To see a discussion of the problems the dierent dependencies introduce we refer to the

introductionof[10].

Inthefollowingthree sectionsalternativecharacterizationsof

*∼*

^{,}

^{proposed}

^{by}

^{[10],}

^{are}

given, which avoid the mentioned dependencies and make it possible to use a partition

renementstrategytocheckforopenbisimilarity.

4.4 Constrained Processes

To make the indexing distinctions of open bisimulation local to processes, and thereby

avoidingdependency3describedintheprevioussection,[10]introducedthenotionof con-

strained processes, dened a bisimilarity on these, and showed that there is a useful

connectionbetweenconstrainedprocessbisimilarityand

*π*

^{-process}

^{open}bisimilarity.

Denition 16 (ConstrainedProcess)

A constrainedprocess isapair

*hP, Di*

^{,}

^{where}

*P*

^{is}

^{a}

*π*

^{-process}

^{and}

*D*

^{is}

^{a}distinction such

that n

### (D) *⊆*

^{fn}

### (P )

^{.}

Welet

*CP*

^{denote}

^{the}

^{set}

^{of}

^{all}constrainedprocesses.

*CP*

^{is}

^{ranged}

^{over}

^{by}

*A*

^{and}

*B*

^{.}

Denition 17 (Free andBoundNamesofConstrainedProcesses)

Let

*A* ^{def} = *h* *P, D* *i ∈ CP*

^{def}

^{.}

^{Then}

^{the}

^{free}

^{names}

^{of}

*A*

^{,}

^{written}

^{fn}

### (A)

^{,}

^{are}

^{dened}

^{as}

fn

### (A) =

^{fn}

### (P )

^{and}

^{the}

^{bound}

^{names}

^{of}

*A*

^{,}

^{written}

^{bn}

### (A)

^{,}

^{are}

^{dened}

^{as}

^{bn}

### (A) =

^{bn}

### (P )

^{.}

Application of a substitution

*σ*

^{to}

^{a}constrained process

*A* ^{def} = *hP, Di*

^{def}

^{is}

^{written}

*Aσ*

^{and}

abbreviates

*hP σ, Dσi*

^{.}

Thetransitionsof aconstrainedprocess

*hP, Di*

^{are}

^{dened}

^{from}

^{those}

^{of}

^{the}

*π*

^{-process}

*P*

^{as}

*P* ^{(} *−→* ^{M,α} ^{)} *P* ^{0}

^{M,α}

^{0}

*hP, Di* ^{(} *−→ hP* ^{M,α} ^{)} ^{0} *, D* ^{M} _{P,α} *∩*

^{M,α}

^{0}

^{M}

_{P,α}

^{fn}

### (P ^{0} ) *i* *M*

^{0}

^{respects}

*D*

Asitisseen

*hP, Di*

^{can}

^{make}

^{the}

^{same}transitionsas

*P*

^{except}

^{those}

^{where}

^{the}

^{condition}

*M*

^{of}

^{the}

^{transition}

^{conicts}

^{with}

^{the}distinction

*D*

^{.}

For two constrained processesto bebisimilar they must fulll two requirements. The

rst oneis that they are compatible, e.i. their distinctions must agree on the common

names.

Denition 18 (Compatibility)

The constrained processes

*hP, Di*

^{and}

*hQ, Ei*

^{are}compatible, written

*hP, Di ⇓ hQ, Ei*

^{,}

^{if}

*D* *∩*

^{fn}

### (Q) = *E* *∩*

^{fn}

### (P )

^{.}

^{A}

^{relation}

*E*

^{on}constrained processesis compatible if

*A* *⇓* *B*

^{for}

eachpair

### (A, B) *∈ E*

^{.}

Thesecondrequirementfortwoconstrainedprocesses

*A*

^{and}

*B*

^{to}

^{be}

^{bisimilar}

^{is}

^{that}

### (A, B)

iscontainedin a

*_*

-bisimulation.
Denition 19 (

*_*

-bisimulation)
Arelation

*E*

^{on}constrainedprocessesisa

*_*

-bisimulationif*hP, Di E hQ, Ei*

^{implies}

(i) for all

*M*

^{,}

*α*

^{,}

^{and}

*h* *P* ^{0} *, D* ^{0} *i*

^{0}

^{0}

^{such}

^{that}

*h* *P, D* *i* ^{(} *−→ h* ^{M,α} ^{)} *P* ^{0} *, D* ^{0} *i*

^{M,α}

^{0}

^{0}

^{,}

^{with}

^{bn}

### (α) *∩*

^{fn}

### (Q) = *∅*

^{,}

thereexistsome

*N*

^{,}

*β*

^{,}

^{and}

*hQ* ^{0} *, E* ^{0} *i*

^{0}

^{0}

^{such}

^{that}

*hQ, Ei* ^{(} *−→ hQ* ^{N,β} ^{)} ^{0} *, E* ^{0} *i*

^{N,β}

^{0}

^{0}

^{and}

*M . N*

^{,}

*α* = *βσ* *M*

^{,}

^{and}

*h* *P* ^{0} *, D* ^{0} *iEh* *Q* ^{0} *σ* *M* *,* (D *∪* *E)* ^{M} _{(} _{P,Q} _{)} _{,α} *∩*

^{0}

^{0}

^{0}

^{M}

_{P,Q}

_{,α}

^{fn}

### (Q ^{0} *σ* *M* ) *i*

^{0}

^{,}

^{and}

(ii) theconverse,withtheroleof

*hP, Di*

^{and}

*hQ, Ei*

^{exchanged.}

Fromthedenitionofconstrainedbisimulationwedenethenotionofconstrainedbisim-

ilarity.

Denition 20 (ConstrainedBisimilarity)

Theconstrainedprocesses

*A*

^{and}

*B*

^{are}constrainedbisimilar,written

*A _ B*

^{,}

^{if}

*A* *⇓* *B*

^{and}

there existsa

*_*

-bisimulation*E*

^{such}

^{that}

*A* *E* *B*

^{.}

The followingtheorem shows the connection between

*π*

^{-process}

^{open}bisimilarity,

*∼*

^{,}

^{and}

constrainedbisimilarity,

*_*

^{.}

Theorem1 (Characterizationof

*∼*

^{in}

^{terms}

^{of}

*_*

^{)}

*P* *∼* *D* *Q*

^{if}

^{and}

^{only}

^{if}

*hP, D* *∩*

^{fn}

### (P ) *i* *_* *hQ, D* *∩*

^{fn}

### (Q) *i*

4.5 Non-Redundant Transitions

Asitisseenfromthedenitionof

*_*

-bisimulation,itsuersfromsomeofthesameproblems
asthe denition of open bisimulationwith respect to constructing analgorithm based on
partition renement. A name emitted by

*hP, Di*

^{may}

^{not}

^{occur}

^{free}

^{in}

*hQ, Ei*

^{and}

^{the}

substitution

*σ* *M*

^{determined}

^{by}

^{the}

^{condition}

*M*

^{in}

^{a}

^{transition}

^{of}

*hP, Di*

^{must}

^{be}

^{applied}

tothederivativeof

*hQ, Ei*

^{.}

^{To}

^{remove}

^{the}

^{latter}

^{of}

^{these}

^{problems,}

^{dependency}

^{2}

^{described}

in section4.3,[10]introducedthenotionof non-redundant transitions ofaconstrained

process.

Intuitively a transition

*A* ^{(} ^{M,α} *−→* ^{)} *A* ^{0}

^{M,α}

^{0}

^{is}non-redundant if there does not exist another transition

*A* ^{(} *−→* ^{N,β} ^{)} *A* ^{00}

^{N,β}

^{00}

^{where}

*M*

^{implies}

*N*

^{,}

*α* = *βσ* *M*

^{,}

^{and}

*A* ^{0}

^{0}

^{and}

*A* ^{00}

^{00}

^{are}

^{bisimilar.}

Denition 21 (Non-RedundantTransitions)

Let

*D*

^{be}

^{a}

^{relation}

^{on}constrainedprocesses. Atransition

*h* *P, D* *i* ^{(} *−→ h* ^{M,α} ^{)} *P* ^{0} *, D* ^{0} *i*

^{M,α}

^{0}

^{0}

^{is}

^{redundant}

for

*D*

^{if}

^{there}

^{exists}

^{a}

^{transition}

*hP, Di* ^{(} *−→ hP* ^{N,β} ^{)} ^{00} *, D* ^{00} *i*

^{N,β}

^{00}

^{00}

^{such}

^{that}

(i)

*M* 6B *N*

^{,}

(ii)

*α* = *βσ* *M*

^{,}

^{and}

(iii)

*hP* ^{0} *, D* ^{0} *i D hP* ^{00} *σ* *M* *, D* ^{M} _{P,α} *∩*

^{0}

^{0}

^{00}

^{M}

_{P,α}

^{fn}

### (P ^{00} *σ* *M* ) *i*

^{00}

^{.}

A transition

*A* ^{(} ^{M,α} *−→* ^{)} *A* ^{0}

^{M,α}

^{0}

^{is}non-redundant for

*D*

^{,}

^{written}

*A* ^{(} ^{M,α} *−→* ^{)} *A* ^{0} *∈*

^{M,α}

^{0}

^{nr}

### ( *D* )

^{,}

^{if}

^{it}

^{is}

^{not}

redundantfor

*D*

^{.}

Computing the non-redundant transitions of a process is as dicult as checking for

bisimilarity[10].

The following lemma showsthat when we havetwo bisimilarconstrained processes

*A*

and

*B*

^{then,}

^{if}

*A*

^{has}

^{a}non-redundant transition,

*B*

^{can}

^{match}

^{it}

^{with}

^{a}non-redundant transitionwiththesameconditionandaction.

Lemma1

If

*A _ B*

^{and}

*A* ^{(} *−→* ^{M,α} ^{)} *A* ^{0} *∈*

^{M,α}

^{0}

^{nr}

### (_)

^{with}

^{bn}

### (α) *∩*

^{fn}

### (B) = *∅*

^{then}

^{there}

^{exists}

^{a}

*B* ^{0}

^{0}

^{such}

^{that}

*B* ^{(} ^{M,α} *−→* ^{)} *B* ^{0} *∈*

^{M,α}

^{0}

^{nr}

### (_)

^{and}

*A* ^{0} *_ B* ^{0}

^{0}

^{0}

^{.}

Thisisstatedin thefollowinglemma.

Lemma2

If

*D ⊆ E*

^{then}

^{nr}

### ( *E* ) *⊆*

^{nr}

### ( *D* )

^{.}

4.6 Active Names

Toavoiddependency1describedin section 4.3, the choice ofbound names of theactions

of matching transitions for bisimilar constrained processes should be made local to the

processes. Since thefree names of two bisimilarconstrained processes arenot necessarily

thesame,thechoicecannotbebasedonthese. [10]hasshownthatthechoicecanbebased

onactive names sincethese arethesameforbisimilarconstrainedprocesses. Intuitively

the activenamesofaconstrained processarethesubset ofthefreenameswhichinuence

thebehavioroftheprocess.

Denition 22 (ActiveNames)

Let

*D*

^{be}

^{a}

^{relation}

^{on}constrained processes and let an

*D*

^{be}

^{the}

^{least}

^{xed}

^{point}

^{of}

^{the}

function

*ψ* : ( *CP → P* ( *N* )) *→* ( *CP → P* ( *N* ))

^{dened}

^{as}

*ψ(f* )(A) = [

*{* *M,α,A* ^{0} *|* *A* ^{(M,α)} *−→* *A* ^{0} *∈*

^{0}

^{0}

^{nr}

### (D)}

fn

### (M, α) *∪* (f (A ^{0} ) *\*

^{0}

^{bn}

### (α))

Thename

*n*

^{is}

^{active}

^{in}

*A*

^{with}

^{respect}

^{to}

*D*

^{if}

*n* *∈*

^{an}

*D* (A)

^{and}

^{otherwise}

*n*

^{is}

^{inactive}

^{in}

*A*

withrespectto

*D*

^{.}

Computingtheactivenamesofaprocessisasdicultascheckingforbisimilarity[10].

An activename in aconstrained process with respect to arelation is also active with

respecttoasubsetofthisrelation. Thisisstatedinthefollowinglemma.

Lemma3

If

*D ⊆ E*

^{then}

^{an}

_{E} *⊆*

_{E}

^{an}

_{D}

_{D}

^{.}

The following lemma shows that twobisimilarconstrained processeshave thesameset of

activenameswithrespectto

*_*

^{.}

Lemma4

If

*A _ B*

^{then}

^{an}

*_* (A) =

^{an}

*_* (B)

^{.}

This lemmaimplies thatiffor each transition

*A* ^{(} ^{M,α} *−→* ^{)} *A* ^{0}

^{M,α}

^{0}

^{the}

^{possibly}

^{bound}

^{name}

^{in}

*α*

^{is}

converted to the least not active name of

*A*

^{then}

^{the}

^{actions}

^{on}

^{matching}transitions are equal.

Non-redundanttransitionswiththeiractionsconvertedasdescribedarecallednormal-

ized transitions.