Checking for Open Bisimilarity in the π -Calculus

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

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

π

^{-CalculusMarcoPistoreandDavideSangiogipresentaniterativemethod}

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

π

^{-ProcessesUsedin}PerformanceTests . . . 60

B.2 ResultsofPerformanceTests . . . 61

Introduction

This paperdealswithalgorithmiccheckingofopenbisimilarityin the

π

^{-calculus. Wehave}

implementedanalgorithmforopenbisimulationcheckinginthe

π

^{-calculus. Mostalgorithms}

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

π

^{-calculusanddenesome}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

π

^{-calculusdevelopedby[10]isasmany}

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

^{beaset. Apartition}

W

^of

U

^{isaniteset ofpairwise disjointsubsets}

B ₁ , . . . B n

^of

U

^where

S

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

^{. Thesets}

B i

^of

W

^{arecalledblocks.}

Denition 2 (GeneralizedPartitionRenementProblem)

Givenaset

U

^,apartition

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

^of

U

^,and

k

^functions

f l : U → P (U )

^,

1 ≤ l ≤ k

^,

wewanttorene

W

^{intoanewpartition}

W ⁰

^of

U

^,where

W ⁰ = {C 1 , . . . , C m }

^{isthecoarsest}

set (theset withfewestblocks)satisfying

(i) foreach

i ∈ { 1, . . . , m}

^{there existsa}

j ∈ { 1, . . . , n}

^suchthat

C i ⊆ B j

^and

(ii) forany

a, b ∈ C i

^{, anyblock}

C j

^,

1 ≤ i, j ≤ m

^{,and anyfunction}

f l

^,

1 ≤ l ≤ k

^itholds

that

f l (a) ∩ C j 6 = ∅

^ifandonlyif

f l (b) ∩ C j 6 = ∅

^.

Thenewpartition

W ⁰

^{alwaysexists[3]andistheuniquegreatestxedpointofthefunction}

ψ _W

^{thatmapspartitionsof}

U

^{topartitionsof}

U

^{andisdened by}

C ∈ ψ _W ( W ⁰ )

^ifandonlyif

(i)

∃B ∈ W.(C ⊆ B)

^and

(ii) forany

a, b ∈ C

^,anyblock

C ⁰ ∈ W ⁰

^{,andanyfunction}

f l

^,

1 ≤ l ≤ k

^itholdsthat

f l (a) ∩ C ⁰ 6 = ∅

^ifandonlyif

f l (b) ∩ C ⁰ 6 = ∅

^.

The partition

W ⁰

^{induces an} equivalence

W _∼ ⁰

^{dened by}

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

^{. Sothe}generalizedpartitionrenementproblemconsistsofcomputingtheequivalence classesof

U

^foranequivalencedened asagreatestxedpoint.

Insection5.3wewillpresentanalgorithmtosolvethepartitionrenementproblemfor

a nite set

U

^and

k = 1

^{. This canbe used to solvethe} 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

^{beasetof statesand}

A ct

^{aset oflabels. Welet}

P

^and

Q

^rangeover

P

^and

α

^over

Act

^{. Foragivenlabeledtransitionsystem(}

P

^,

Act

^,

−→

^)wedenebisimulationasfollows.

Denition 3 (Bisimulation)

Arelation

R ⊆ P × P

^isabisimulationif

(P, Q) ∈ R

^implies,

(i) if

P −→ ^α P ⁰

^thenforsome

Q ⁰ ∈ P

^,

Q −→ ^α Q ⁰

^and

(P ⁰ , Q ⁰ ) ∈ R

^,and

(ii) if

Q −→ ^α Q ⁰

^thenforsome

P ⁰ ∈ P

^,

P −→ ^α P ⁰

^and

(P ⁰ , Q ⁰ ) ∈ R

^.

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 ⁰

^if

s ^def = a ₁ a ₂ · · · a n

^,

a i ∈ A ct

^{andthere exists asequence ofstates}

P ₁ , P ₂ , . . . , P n ∈ P

^{such that}

P −→ ^{a 1} P ₁ −→ ^{a 2}

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

^and

P ⁰ = P n

^{. F}urthermore,wedene thelabelscontainedin astateasn

(P ) = {α ∈ Act | ∃s ₁ , s ₂ ∈ Act ^∗ .( ∃P ⁰ ∈ P.P ^s −→ ^{1 αs 2} P ⁰ ) }

^.

Nowweshowhowapartitionrenementalgorithmcanbeusedforbisimulationchecking.

Ifrene

(U, W, f ₁ , . . . , f k )

^{isafunction which returnsasolutionofthe}generalizedpartition renement problem for the instance

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

^{then it canbe used for checking for}

bisimilaritybetweenthestates

P

^and

Q

^{asfollows. Let}

S P

^{denotethestatespaceof}

P

^,i.e.

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

^{. 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 )

^,

α ∈

ⁿ

(P ) ∪

ⁿ

(Q)

^{bedened as}

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

^.

P

^and

Q

are bisimilarifandonlyiftheyarein thesameblockoftherened partition

W ⁰

^returned

from rene

(U, W , { f α } ₍ α ∈

ⁿ

( P )∪

ⁿ

( Q )) )

^{. Thisis truesince}

∼

^{givesriseto apartition}

W ⁰⁰

^of

U

^{wheretheblocksarethe}equivalenceclassesof

∼ ∩ (U × U )

^.

W ⁰⁰

^{isclearlyaxed point}

of

ψ _W

^{. If}

W ⁰⁰

^{is notthe same as}

W ⁰

^{, i.e. the greatestxed point of}

ψ _W

^{, there exists a}

bisimulation

∼ ∪W _∼ ⁰

^largerthan

∼

^,whichisacontradiction.

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. Thesyntacticcategoriesforthe}

π

^{-calculusare: aninnitesetofnames,}

N

^{,asetofactions,}

Act

^{,aninnitesetofprocess}

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

^{. Theset of processescanbe}constructedwith theconstructorsfor inaction, prex,matching, nondeterministic choice,parallel composition, restriction, and

recursion,andanactioncanbeasilentaction,input,free output,orboundoutput.

Thegrammarfor

Act

^and

Pr

^{ispresentedbelow.}

α ::= τ | 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

^{hasan associatedarityandadenition of theform}

K ^def = (˜ b)P

^,

where

˜ b

^{arethe freenamesof}

P

^{(seedenition 4). Fortheprocess}

K h ˜ a i

^thetuple

a ˜

^must

havethesamelengthas

˜ b

^{. Thefree,bound,extruded,object,andsubject namesofan}

action

α

^,writtenfn

(α)

^,bn

(α)

^,en

(α)

^,ob

(α)

^,andsub

(α)

^,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 thefree names andthe bound names of}

α

^{, i.e. n}

(α) =

fn

(α) ∪

^bn

(α)

^{. Thefreeandboundnamesofaprocess aredened asfollows.}

Denition 4 (FreeNames)

Aname

a

^{isfreeintheprocess}

P

^,written

a ∈

^fn

(P )

^{,ifitbelongstothesetfree}

(P )

^,where

thefunction free

: Pr → P ( N )

^{isdened bythefollowing.}

free

( 0 ) = ∅

free

(α.P ) =

^fn

(α) ∪ (

^free

(P ) \

^bn

(α))

free

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

^free

(P)

free

(P ₁ |P ₂ ) =

^free

(P ₁ ) ∪

^free

(P ₂ )

free

(P ₁ + P ₂ ) =

^free

(P ₁ ) ∪

^free

(P ₂ )

free

((ν a)P) =

^free

(P ) \ {a}

free

(K h (a ₁ , a ₂ , . . . , a n ) i ) = { a ₁ , a ₂ , . . . , a n }

Denition 5 (BoundNames)

A name

a

^{isboundin theprocess}

P

^,written

a ∈

^bn

(P)

^{,ifitbelongsto thesetbound}

(P )

^,

where thefunction bound

: P r → P ( N )

^{istheleastfunctionthatsatises thefollowing.}

bound

( 0 ) = ∅

bound

(α.P ) =

^bn

(α) ∪

^bound

(P )

bound

([a = b]P ) =

^bound

(P )

bound

(P ₁ |P 2 ) =

^bound

(P ₁ ) ∪

^bound

(P ₂ )

bound

(P ₁ + P ₂ ) =

^bound

(P ₁ ) ∪

^bound

(P ₂ )

bound

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

^bound

(P )

bound

(Kh (˜ a) i ) =

^bound

(P )

^where

K ^def = (˜ b)P

Thenames ofaprocess

P

^,writtenn

(P )

^{,consistsofthefreenamesandtheboundnames}

of

P

^{,i.e. n}

(P ) =

^fn

(P ) ∪

^bn

(P )

^{. Wesometimeswritefn}

(P ₁ , P ₂ , . . . , P n )

^forfn

(P ₁ ) ∪

^fn

(P ₂ ) ∪

· · · ∪

^fn

(P n )

^{,andsimilarlyforbound namesandnames.}

Weidentifyprocessesuptorenamingofboundnames. Renamingofaboundnameina

processiscalled

α

-conversion. Iftheprocesses

P

^and

Q

^{canbeidentieduptorenaming}

ofboundnamesthen

P

^and

Q

^are

α

-convertible,written

P ≡ α Q

^.

Denition 6 (

α

-conversion)

α

-conversionof aname

a

^{to aname}

b

^{in a}

π

^-process

P

^{, where}

b / ∈

ⁿ

(P )

^{, is the result of}

renamingallbound occurrencesof

a

ⁱⁿ

P

^to

b

^.

Substitutions are denoted by

σ

^{and are functions that map names to names, e.g.}

σ ^def = {y ₁ /x ₁ y ₂ /x ₂ · · · y n /x n }

^{denotes the} simultaneous substitution that maps every freeoccurrenceofthename

x i

^tothename

y i

^forall

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

^{. Aname}

a

^isneutral

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 aprocess}

P

^iswritten

P σ

^{. If thereexists somebound name}

a

ⁱⁿ

P

^such

thatthesubstitution

σ

^{mapssomenameto}

a

^then

a

^is

α

^{-convertedtosome}

b

^{thatisneutral}

for

σ

^.

3.2 Semantics

Theoperationalsemanticsforthesubsetofthe

π

^{-calculusisgivenbythelabeledtransition}

system(

P r

^,

Act

^,

→

^)where

→

^{isthesmallestrelationclosedundertherulesintable3.1. The}

symmetricversionsofthe rulesSum,Par,Com,andClosehavebeenomitted. Transitions

havetheform

P −→ ^α P ⁰

^.

[

^Alpha

] P ⁰ −→ ^α P ⁰⁰

P −→ ^α P ⁰⁰ P ≡ α P ⁰ [

^Pre

]

α.P −→ ^α P

[

^Con

] P { ˜ a/ ˜ b } −→ ^α P ⁰

K h ˜ a i −→ ^α P ⁰ K ^def = (˜ b)P [

^Sum

] P −→ ^α P ⁰ P + Q −→ ^α P ⁰

[

^Par

] P −→ ^α P ⁰

P |Q −→ ^α P ⁰ |Q

^bn

(α) ∩

^fn

(Q) = ∅ [

^Com

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

[

^Close

] P ^a −→ ^{¯ ( x )} P ⁰ Q −→ ^{a ( x )} Q ⁰

P |Q −→ ^τ (ν x)(P ⁰ |Q ⁰ ) [

^Match

] P −→ ^α P ⁰ [a = a]P −→ ^α P ⁰

[

^Res

] P −→ ^α P ⁰

(ν b)P −→ ^α (ν b)P ⁰ b / ∈

ⁿ

(α) [

^Open

] P −→ ^{¯ ab} P ⁰ (ν b)P −→ ^{¯ a ( b )} P ⁰

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

^{onprocessesis alate} bisimulationif

P R Q

^and

P −→ ^α P ⁰

where bn

(α) ∩ (

^fn

(P ) ∪

^fn

(Q)) = ∅

^implies

(i) if

α = a(x)

^then

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

^,and

(ii) if

α 6 = a(x)

^then

∃Q ⁰ .(Q −→ ^α Q ⁰ ∧ P ⁰ R Q ⁰ )

^.

Fromthedenition oflatebisimulationthenotionof late bisimilarity isdened.

Denition 8 (LateBisimilarity)

Theprocesses

P

^and

Q

^{arelatebisimilar,written}

P ∼ ˙ Q

^{,ifthereexistsalate}bisimulation

R

^suchthat

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 latebisimilar. If}

P

^{hasthe transition}

P −→ ^{a ( x )} P ⁰

^{,that is}

P

^can

receivesomethingonthechannel

a

^andbecome

P ⁰

^{,wecanonlyexplore}transitionsfrom

P ⁰

byexaminingallthepossiblesubstitutionsof

x

ⁱⁿ

P ⁰

^{andthereareinnitelymanyofthese.}

Similarproblemsariseforearly bisimilarity basedonthelatesemanticsgivenbythe

labeledtransition systemoftable3.1. Early bisimulation isdenedasfollows.

Denition 9 (EarlyBisimulation)

Asymmetricbinaryrelation

R

^{onprocessesisanearly}bisimulationif

P R Q

^and

P −→ ^α P ⁰

where bn

(α) ∩ (

^fn

(P ) ∪

^fn

(Q)) = ∅

^implies

(i) if

α = a(x)

^then

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

^,and

(ii) if

α 6 = a(x)

^then

∃ Q ⁰ .(Q −→ ^α Q ⁰ ∧ P ⁰ R Q ⁰ )

^.

Fromthedenition ofearlybisimulationthenotionofearlybisimilarityisdened.

Denition 10 (Early Bisimilarity)

Theprocesses

P

^and

Q

^{areearlybisimilar,written}

P ∼ ˙ E Q

^{,ifthereexists anearlybisim-}

ulation

R

^suchthat

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

π

^{-calculusand 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 theset of names,}

N

^{, and that there exists a smallest name with}

respectto

<

^. Furthermore,weintroducethenotionsof conditionsanddistinctions.

Welet

M

^{denote theset ofall}conditions. Conditionsare rangedoverby

L

^,

M

^{, and}

N

^{andare nite}conjunctionsofmatching, e.g.

[a = b][c = d]

^{is theconditionthat equates}

a

^with

b

^and

c

^with

d

^{. Thenames of a condition}

M

^,writtenn

(M )

^{, arethenamesthat}

appearin

M

^. Compositionof twoconditions

M

^and

N

^{is written}

M N

^{. Ifeverymatch of}

acondition,

N

^{,isimpliedbyanothercondition,}

M

^,wewrite

M B N

^{. Ifitisalsothecase}

that noteverymatchofthecondition

M

^{isimplied by}

N

^wewrite

M 6B N

^{. Thetrivially}

trueconditionisdenoted by

∅

^{. The}substitution

σ M

^{inducedbyacondition}

M

^mapseach

elementofeachequivalenceclassof

M

^{tothesmallestelementofthat}equivalenceclass,i.e.

σ M (a) =

^min

{b | M B [a = b] }

^{. Tofacilitatetheevaluation oftheexpression}

M B N

^{, for}

someconditions

M

^and

N

^{,conditionsare}transformedtoacanonical form.

Thecanonicalform ofacondition

M

^{is thecondition}

M c = [a ₁ = b ₁ ][a ₂ = b ₂ ] · · · [a n = b n ]

where

(i) forall

a ∈

ⁿ

(M )

^with

a 6 = σ M (a)

^itholdsthat

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

^,

(ii)

a i 6 = b i

^andeither

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

^{arethecanonicalforms}

of

M

^and

N

^.

Welet

D is

^{denote thesetofall}distinctions. Distinctionsarenite binarysymmetric irreexiverelationson names

N

^{and are ranged overby}

D

^and

E

^{. If}

(a, b) ∈ D

^forsome

distinction

D

^{then thetwonames}

a

^and

b

^{must bedistinct, i.e.}

a 6 = b

^{. Thenames of}

D

^,

writtenn

(D)

^{,arethenamesthatappearin}

D

^{. A}substitution

σ

^respects

D

^if

σ(a) 6 = σ(b)

for all

(a, b) ∈ D

^{. Likewise, acondition}

M

^{respects the}distinction

D

^{if the}substitution,

σ M

^,inducedby

M

^respects

D

^{. Let}

F ⊆ N

^then

D − F

^denotesthedistinction

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

^and

D ∩ F

^{denotes the}distinction

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

^{. Inthe denition ofa}

distinctionwewillnotalwaysgiveallsymmetricpairs,e.g. in

D ^def = { (a, b) }

^thepair

(b, a)

hasbeenleftout.

4.2 Semantics

Inthissectionwegiveasymbolicsemanticsspecializedforopenbisimulationforthesubset

of the

π

^{-calculus. A symbolicsemantics isused to avoidthe innitebranching 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

^{. To explore the further} transitions of

P

^{we have to}

explorethebehaviorof

P {y/x}

^{forinnitelymany}

y

^{s. Thenotionofsymbolicsemanticsfor}

the

π

^{-calculuswasrst 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 ⁰

^,

where

M

^{representstheminimalconditionrequiredfor}

P

^{to perform theaction}

α

^{. Welet}

µ

^rangeover

M × Act

^.

[

^Alpha

] P ^{0 µ} P ⁰⁰

P ^µ P ⁰⁰ P ≡ α P ⁰ [

^Pre

]

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

^Con

] P{ ˜ a/ ˜ b} ^µ P ⁰

Kh ˜ ai ^µ P ⁰ K ^def = (˜ b)P

[

^Sum

] P ^µ P ⁰

P + Q ^µ P ⁰ [

^Par

] P ^µ P ⁰

P|Q ^µ P ⁰ |Q

^bn

(µ) ∩

^fn

(Q) = ∅

[

^Com

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

where

L ^def = M N[a = b]

[

^Close

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

where

L ^def = M N [a = b]

[

^Match

] P ^{( M,α )} P ⁰ [a = b]P ^{( N,α )} P ⁰

where

N ^def = M [a = b]

[

^Res

] P ^µ P ⁰

(ν b)P ^µ (ν b)P ⁰ b / ∈

ⁿ

(µ)

[

^Open

] P ^{( M, ¯ ab )} P ⁰ (ν b)P ^{( M, ¯ a ( b ))} P ⁰

b / ∈

ⁿ

(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 ⁰

^{is in}

canonical form and

α

^and

P ⁰

^{are closed under the} substitution

σ M

^{, i.e.}

α = ασ M

^and

P ⁰ = P ⁰ σ M

^{. Therelation}

−→

^{isthesmallestrelationclosedunder thefollowingrule.}

[

^Canon

] P ^{( N,α )} P ⁰ P ^{( M,ασ} −→ ^{M )} P ⁰ σ M

bn

(α) ∩

^fn

(P ) = ∅

^and

M

^{isthecanonicalform 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

^isaset

{R D } D

^ofrelations

R D

^over

π

-processes,where

D

rangesoveralldistinctionsin

D is

^.

Denition 13 (OpenBisimulation)

Adistinction-indexed relation

R

^isanopenbisimulationif

P R D Q

^implies

(i) forall

M

^,

α

^,and

P ⁰

^suchthat

P ⁽ −→ ^{M,α )} P ⁰

^,withbn

(α) ∩

^fn

(Q, D) = ∅

^and

M

^respects

D

^{, thereexistsome}

N

^,

β

^,and

Q ⁰

^suchthat

Q ⁽ −→ ^{N,β )} Q ⁰

^and

M B N

^,

α = βσ M

^,and

P ⁰ R D ⁰ Q ⁰ σ M

^for

D ^{0 def} = (D ∪ (

^en

(α) ×

^fn

(P, Q)))σ M

^,and

(ii) theconverse,withtheroleof

P

^and

Q

^exchanged.

Fromthedenition ofopenbisimulationwedenethenotionof open bisimilarity.

Denition 14 (Openbisimilarity)

Theprocesses

P

^and

Q

^{areopenbisimilarwithrespect to}distinction

D

^{, written}

P ∼ D Q

^,

if

P R D Q

^forsomeopenbisimulation

R

^.

Asitisseenindenition13thedistinction

D ⁰

^is

D

^{updatedwiththefactthattheextruded}

namesof theaction

α

^{mustbedierentfrom allfreenamesin theprocesses}

P

^and

Q

^and

afterwardsupdated byapplying

σ M

^{to it. Since this kind ofupdating of} distinctionswill oftenbeused inthefollowing,wewilluseashorternotationdenedasfollows.

Let

D

^{be a} distinction,

P ₁ , . . . , P n

^processes,

M

^{a condition, and}

α

^{an action. Then we}

dene

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

^as

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

^en

(α) ×

^fn

(P ₁ , . . . , P n )))σ M

With thisdenition

D ⁰

^{in denition13couldbewritten as}

D ₍ ^M _{P,Q ) ,α}

^.

Touse themethod described in chapter 2to check whether

P ∼ D Q

^{it is necessaryto}

generate thestate spacesof

P

^and

Q

separately. This cannotbedone sincethe following dependenciesbetween

P

^and

Q

^aectthetransitionsandthederivatives.

Dependency1 Thenameemittedby

P

^{maynotoccurfreein}

Q

^.

Dependency2 Thesubstitution

σ M

^{determinedbythecondition}

M

^{in atransition 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

∼

^{, proposedby [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

π

^-processopenbisimilarity.

Denition 16 (ConstrainedProcess)

A constrainedprocess isapair

hP, Di

^{, where}

P

^{is a}

π

^-processand

D

^{is a}distinction such

that n

(D) ⊆

^fn

(P )

^.

Welet

CP

^{denotethesetofall}constrainedprocesses.

CP

^{is rangedoverby}

A

^and

B

^.

Denition 17 (Free andBoundNamesofConstrainedProcesses)

Let

A ^def = h P, D i ∈ CP

^{. Then the free names of}

A

^{, written fn}

(A)

^{, are dened as}

fn

(A) =

^fn

(P )

^{andthebound namesof}

A

^,writtenbn

(A)

^{,aredenedasbn}

(A) =

^bn

(P )

^.

Application of a substitution

σ

^{to a} constrained process

A ^def = hP, Di

^{is written}

Aσ

^and

abbreviates

hP σ, Dσi

^.

Thetransitionsof aconstrainedprocess

hP, Di

^{aredened from those ofthe}

π

^-process

P

^as

P ⁽ −→ ^{M,α )} P ⁰

hP, Di ⁽ −→ hP ^{M,α ) 0} , D ^M _P,α ∩

^fn

(P ⁰ ) i M

^respects

D

Asitisseen

hP, Di

^{canmakethesame}transitionsas

P

^{exceptthosewherethecondition}

M

^{ofthetransitionconicts withthe}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

^onconstrained processesis compatible if

A ⇓ B

^for

eachpair

(A, B) ∈ E

^.

Thesecondrequirementfortwoconstrainedprocesses

A

^and

B

^{tobebisimilaristhat}

(A, B)

iscontainedin a

_

-bisimulation.

Denition 19 (

_

-bisimulation)

Arelation

E

^onconstrainedprocessesisa

_

-bisimulationif

hP, Di E hQ, Ei

^implies

(i) for all

M

^,

α

^{, and}

h P ⁰ , D ⁰ i

^{such that}

h P, D i ⁽ −→ h ^{M,α )} P ⁰ , D ⁰ i

^{, with bn}

(α) ∩

^fn

(Q) = ∅

^,

thereexistsome

N

^,

β

^,and

hQ ⁰ , E ⁰ i

^suchthat

hQ, Ei ⁽ −→ hQ ^{N,β ) 0} , E ⁰ i

^and

M . N

^,

α = βσ M

^,and

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

^fn

(Q ⁰ σ M ) i

^,and

(ii) theconverse,withtheroleof

hP, Di

^and

hQ, Ei

^exchanged.

Fromthedenitionofconstrainedbisimulationwedenethenotionofconstrainedbisim-

ilarity.

Denition 20 (ConstrainedBisimilarity)

Theconstrainedprocesses

A

^and

B

^areconstrainedbisimilar,written

A _ B

^,if

A ⇓ B

^and

there existsa

_

-bisimulation

E

^suchthat

A E B

^.

The followingtheorem shows the connection between

π

^{-process open} bisimilarity,

∼

^{, and}

constrainedbisimilarity,

_

^.

Theorem1 (Characterizationof

∼

^intermsof

_

⁾

P ∼ D Q

^ifandonlyif

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 thecondition}

M

^{in atransition of}

hP, Di

^{mustbeapplied}

tothederivativeof

hQ, Ei

^{. Toremovethelatteroftheseproblems,dependency2described}

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

process.

Intuitively a transition

A ^{( M,α} −→ ⁾ A ⁰

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

A ⁽ −→ ^{N,β )} A ⁰⁰

^where

M

^implies

N

^,

α = βσ M

^{, and}

A ⁰

^and

A ⁰⁰

^{arebisimilar.}

Denition 21 (Non-RedundantTransitions)

Let

D

^{bearelationon}constrainedprocesses. Atransition

h P, D i ⁽ −→ h ^{M,α )} P ⁰ , D ⁰ i

^isredundant

for

D

^{ifthereexistsatransition}

hP, Di ⁽ −→ hP ^{N,β ) 00} , D ⁰⁰ i

^suchthat

(i)

M 6B N

^,

(ii)

α = βσ M

^,and

(iii)

hP ⁰ , D ⁰ i D hP ⁰⁰ σ M , D ^M _P,α ∩

^fn

(P ⁰⁰ σ M ) i

^.

A transition

A ^{( M,α} −→ ⁾ A ⁰

^is non-redundant for

D

^{, written}

A ^{( M,α} −→ ⁾ A ⁰ ∈

^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

^{canmatch it with a} non-redundant transitionwiththesameconditionandaction.

Lemma1

If

A _ B

^and

A ⁽ −→ ^{M,α )} A ⁰ ∈

^nr

(_)

^withbn

(α) ∩

^fn

(B) = ∅

^{thenthereexistsa}

B ⁰

^suchthat

B ^{( M,α} −→ ⁾ B ⁰ ∈

^nr

(_)

^and

A ⁰ _ B ⁰

^.

Thisisstatedin thefollowinglemma.

Lemma2

If

D ⊆ E

^thennr

( 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 ))

^denedas

ψ(f )(A) = [

{ M,α,A ⁰ | A ^(M,α) −→ A ⁰ ∈

^nr

(D)}

fn

(M, α) ∪ (f (A ⁰ ) \

^bn

(α))

Thename

n

^isactivein

A

^{withrespectto}

D

^if

n ∈

^an

D (A)

^andotherwise

n

^isinactivein

A

withrespectto

D

^.

Computingtheactivenamesofaprocessisasdicultascheckingforbisimilarity[10].

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

respecttoasubsetofthisrelation. Thisisstatedinthefollowinglemma.

Lemma3

If

D ⊆ E

^thenan

_E ⊆

^an

_D

^.

The following lemma shows that twobisimilarconstrained processeshave thesameset of

activenameswithrespectto

_

^.

Lemma4

If

A _ B

^thenan

_ (A) =

^an

_ (B)

^.

This lemmaimplies thatiffor each transition

A ^{( M,α} −→ ⁾ A ⁰

^{thepossiblyboundname in}

α

^is

converted to the least not active name of

A

^{then the actions onmatching} transitions are equal.

Non-redundanttransitionswiththeiractionsconvertedasdescribedarecallednormal-

ized transitions.