Fig.1.CP-netfortheDistributedDatabaseexample.
1
Fig.2. Thefull state space (the left-hand side) and SSPS (theright-hand side) of the CP-net for the
distributeddatabaseexamplewith3symmetricdatabasemanagers(n=3).
symmetries. The symmetry specication is required to be consistent [8] which means that it is
requiredto onlyexpresssymmetriesthat areactuallypresentinthesystem.Wewill use
SG to
denotethegroupofpermutationsymmetriesgivenbyaconsistentsymmetryspecicationSG.In
therestofthepaperweassumethataCP-netwithplacesP =fp
1
;p
2
;:::;p
n
gisgiventogetherwith
aconsistentsymmetryspecicationSGwhichdeterminesagroup
SG
ofpermutationsymmetries.
2.3 RestrictionSets
A consistent symmetry specication SG determines a group of permutation symmetries
SG .
DuringgenerationoftheSSPSweneedsomekindof representationof
SG
.Onepossibilityisto
list thepermutation symmetries.Since thesymmetry groupsused for thereductioncanbe very
large,thisisnotafeasiblesolution.
A set ofpermutations ofanatomic coloursetcaninsteadberepresentedasarestrictionset.
Restrictionsetsareintroducedin[8]andformallydenedin[1].Herewewillintroducerestriction
setsbymeansofanexample.Belowweusearestrictionsettorepresentasubsetof[DBM!DBM].
Thesetofpermutationsmappingd(1)tod(2)andtheset fd(2),d(3)gtothesetfd(1),d(3)g
canberepresentedbythefollowingrestrictionset:
d(1) d(2)
d(2) d(3)d(1) d(3)
Each rowin therestrictionset introducesarequirementforthe setof permutations represented
bytherestrictionset.Theindividualrestrictions(rows)expressthatthecoloursontheleft-hand
side must bemapped into the colours of theright-hand side. In[1] it is proven that restriction
sets can be eÆciently intersected (while maintaining the compact representation) and that an
arbitrarysetofpermutationscanberepresentedbyasetofrestrictionsets.Hence,restrictionsets
provideapotentiallycompactrepresentationofsetsof permutations.Intherestof thepaperwe
willuserestrictionsetstorepresentsetsofpermutationsofatomiccoloursets.Hence,asymmetry
specicationcanberepresentedbyasetofrestrictionsetsforeachatomiccoloursetintheCP-net.
3 Condensed State Space Generation
InthissectionwegiveanintroductiontothestandardalgorithmGenerate-SSPSfor
construc-tionoftheSSPSofaCP-net[8].NodesandArcsaresetsofstates(markings)andactions(binding
elements),respectively,anditcontainsthestatesandactionsthatareincludedintheSSPS.
Unpro-cessedisasetofstates,andcontainsthestatesforwhichwehavenotyetcalculatedthesuccessor
0
moves(anactionandtheresultingstate) from thestateM.Node(M)isafunction thatchecks
whether a node symmetric to M is already included in theSSPS. If not,M is added to Nodes
and Unprocessed. Similarly, Arc(M
1 ,b,M
2
)is afunction that checkswhether asymmetricarcis
alreadyincludedin theSSPS, i.e., anarc consistingof abinding elementsymmetric tob from a
markingsymmetricto M
1
toamarkingsymmetrictoM
2
Algorithm:GenerateSSPS()=
1: Nodes fM
10: Unprocessed:=UnprocessednfM
1 g
11: untilUnprocessed=;
Thealgorithmproceedsin anumberofiterations.Ineachiterationastate(M
1
)isselectedfrom
Unprocessedand the successorstates(andactions) arecalculated usingthe Nextfunction. For
eachofthesuccessorstates,M
2
,itischeckedwhether Nodesalreadycontainsastatesymmetric
toM
2
.IfnotM
2
isaddedtobothNodesandUnprocessed.Similarchecksaremadefortheactions.
Thecheckforsymmetricstatesandsymmetricactionsareinstancesoftheorbitproblem.Fromthe
basicgenerationalgorithmitcanbeseenthateÆcientgenerationoftheSSPSishighlydependent
ontheeÆciency ofthealgorithmsfordeterminingthefollowingtwoproblems:1) Whenreaching
a new markingM during generation of the SSPS, is there a marking symmetric to M already
included in the SSPS? And 2) When reaching a new arc (M
1
;b;M
2
) during generation of the
SSPS,isthereasymmetricarcalreadyincludedin theSSPS?
GenerateSSPSisimplementedin theDesign/CPNOE/OStoolandused whencalculating
SSPSs for CP-nets. In Design/CPN a hash function is used when storing the markings during
generationoftheSSPS.WhenreachinganewmarkingduringgenerationoftheSSPSeachmarking
storedwiththesamehashvalueischeckedtoseeifitissymmetrictothenewlyreachedmarking,
i.e., symmetry checksare performed locally between markingsin thecollision lists. The userof
the tool is free to use his own hash function. The only requirement is that the hash function
used is symmetryrespecting, i.e., symmetric statesare mapped tothe samehash value.This is
thecaseforthedefault hashfunction usedin Design/CPN.Hence,whenusing theDesign/CPN
OE/OStoolforthegeneration ofSSPSseÆcientgenerationisdependentontheeÆciency ofthe
two predicates, P
M and P
BE
, determining symmetry between markings and binding elements,
respectively.
TheDesign/CPNOE/OStoolrequiresP
M andP
BE
tobeimplementedbytheuser.Implementing
such predicates is error-pronefor largeCPN models and requires both programmingskills and
a detailed knowledge of the symmetry method. This is especially the case if the predicates are
required to beeÆcient. The required userimplementation of P
M and P
BE
in the Design/CPN
OE/OStoolhasmotivatedthedevelopmentoftheDesign/CPNOPStoolwhich givenaCP-net
andaconsistentsymmetryspecicationautomaticallygeneratesthetwopredicates,P
M andP
BE ,
neededbytheDesign/CPNOE/OStool.Intherest ofthepaperwewill presenttechniquesand
algorithms to obtain implementations of P
M and P
BE
in theDesign/CPN OPS tool which are
canbeautomaticallygenerated.
In the following discussions we will concentrate on the markings since the symmetry check
betweenbindingelementscanbeviewedasaspecialcaseofsymmetrychecksbetweenmarkings:
Given a transition t with variables v
1
of singleton multi-sets (1`b(v
1 );1`b(v
2
);:::;1`b(v
m
)), where b(v) denotes thevalue assigned to v
in the binding b. Since transitions cannot be permuted by permutation symmetries in CP-nets
determining symmetrybetweenbinding elements isthe sameasdeterminingsymmetry between
markings. Hence, in the rest of the paper we will present techniques and algorithms to obtain
aneÆcientimplementationof P
M
, i.e.,givenM
1
;M
2
2M determinewhether 92 such that
4 Basic Algorithm for P
M
InthissectionwewillpresentabasicalgorithmwhichimplementsthepredicateP
M
.Section4.1
presentsthealgorithm.Section4.2presentsexperimentalresultsobtainedusingtheDesign/CPN
OPS tool where the basic algorithm presented in this section is used to determine symmetry
betweenmarkings.
4.1 Presentation ofthe Algorithm
Thealgorithmisbasedonasimpleapproachwhere
SG
,i.e.,thegroupofpermutationsymmetries
allowedbythesymmetryspecicationSG,isiteratedtodeterminewhether92
SG
.ThealgorithmP Basic
Thealgorithmrepeatedlyselectsapermutationsymmetryfrom
SG
(line1)andtestswhether
isasymmetrybetweenthetwomarkings,M
1 and M
2
givenasinput(lines2-4).Theiteration
stopswhenapermutationsymmetryforwhich(M
1 )=M
2
isfound(line3)ortheentire
SG
hasbeeniterated(line6).
The algorithm P Basic
M
potentially tests fewer permutation symmetries than j
SG
j. This is
however not the case if M
1
and M
2
are not symmetric. In that case the algorithm checks the
whole
SG
. Hence, P Basic
M
is only useful for CP-netswith few permutation symmetries.This is
alsosupportedbytheexperimentalresultspresentedbelow.
However,before wepresentthe experimental results of the P Basic
M
algorithm we will briey
introduce how it is tested whether apermutation symmetry maps a marking M
1
).In[1]itisshownhowthesetofpermutationsymmetriesbetween
twomarkingscanbedeterminedastheintersectionofthesetsofpermutationsymmetriesbetween
themarkingsoftheindividualplaces. Hence,todeterminewhetherapermutationsymmetry2
SG
isasymmetrybetweentwomarkingsM
1 andM
2
,weinturntestthemulti-setsconstituting
themarkingsofp
i
2P.Notethatifapermutationsymmetryisnotasymmetryforthemarking
ofaplace p
)the permutation symmetrycannot be asymmetry
between M
1
and M
2
and therefore there is no need to test the remaining places in P. Using
permutation symmetryandtwomarkings,M
1 andM
2
,testswhether(M
1
The algorithm repeatedly selects a place p
i
2 P of the CP-net (line 1) and tests whether is
a symmetry between the markingsof p
i
,otherwiseanewplaceistested.Theiterationproceedsuntilaplacep
i 2P
forwhich isnotasymmetryis found(line3) orallplaceshavebeentested (line6).
4.2 ExperimentalResultsof the P Basic
M
Algorithm
ThissectionpresentsexperimentalresultsobtainedusingtheDesign/CPNOPStool.Thefollowing
resultsare obtainedusing an implementation of P Basic
M
to determinewhether twomarkings are
symmetric.AsimilarapproachisusedfortheimplementationofP
BE .
The Design/CPN OPS tool represents
SG
as a restriction set. When checking symmetry
betweentwomarkingsusing P Basic
M
SG
islisted and thepermutation symmetriesfrom the list
are removedand tested until apermutation symmetry isfound forwhich (M
1 )=M
2 orthe
listisempty.
SSPSs havebeengeneratedfortwodierentCP-netsin anumberofcongurations.The
CP-netsusedintheexperimentsarebrieydescribedbelow.ForadetaileddescriptionoftheCP-nets
wereferto[8,12].
Commit [12].ACP-netmodellingatwo-phasecommitprotocolwithacoordinatorandw
sym-metrical workers.
Distributeddatabase [8]. The CP-netpresentedin Sect. 2 modelling the communication
be-tweennsymmetricaldatabasemanagers.
Table 1 shows the generation statistics for of the SSPS for dierent congurations of the two
CP-nets using the P Basic
M
algorithm. The CP-net column gives the name (C standsfor commit
and D stands for distributed database) and conguration of the CP-net for which the SSPS is
generatedas wellasthenumberof permutationsymmetriesgivenbythesymmetryspecication
SGused forthereduction.TheCountcolumn givestwonumbers:thetotalnumberoftimes the
P
M
predicateis calledduring calculationoftheSSPSand thenumberofcallswhichevaluateto
true,i.e., the numberof thosecalls which determinethat thetwomarkings aresymmetric. The
Testscolumn presents statisticson the numberof permutation symmetriesapplied to markings
during generation ofthe SSPS: Totalgivesthetotal numberof permutation symmetriesapplied
to markings during generation of the SSPS, P Basic
M
gives the average number of permutation
symmetriesappliedineachcallofP Basic
M ,P
Basic
M
=truegivestheaveragenumberofpermutation
symmetries applied in each call of P Basic
M
which evaluates to true (the case where iteration of
the entire
SG
is potentially avoided),and nally, % j
SG
j gives theaverage percentage of the
permutation symmetrieswhich aretested inacallofP Basic
M
.Finally,the Timecolumn givesthe
numberof seconds ittook to generate theSSPS for the given CP-net. A '{' in an entry means
that theSSPS couldnot be generatedwithin 600seconds. All experimental resultspresentedin
thispaperareobtainedona333MHzPentiumIIPCrunningLinux.Themachineisequippedwith
128MbRAM.
FromTable1itcanbeseenthatwhensystemparametersincreasethenumberofpermutation
symmetries tested increasesignicantly. This is caused by the increasingsize of
SG
. From the
P
M
CP-net Count Tests Time
Con.j
720 157 127 27,297 174 44.86 6.2 23
C7 5,040 { { { { { { {
720 126 56 51,693 410 23.1 3.20 16
D
7
5,040 { { { { { { {
Table1.GenerationstatisticsforSSPSgenerationusingtheP Basic
M
algorithm.
% j
SG
j column it can beseen that theaverage percentageof
SG
which are tested in P Basic
M
decreaseswhenthesystemparametersincrease.However,theincreasingsizeof
SG
makesit
im-possibleto generatethe SSPSfor thetwoCP-netswhen systemparameters,i.e., thenumberof
concurrentreadersordatabasemanagers,becomesgreaterthan6.Thisisalsocausedbythe
ap-proachwhere
SG
islistedbeforethepermutationsymmetriesaretested.Forsystemsofincreasing
size j
SG
j imply that theentire
SG
cannot berepresentedin memory and, thus, generationof
theSSPSisnotpossible.Itshould benotedthat theresultspresentedinTable1dependsonthe
orderinwhichthepermutationsymmetriesareapplied.Theorderusedfortheexperimentsisthe
sameorderin each callofP Basic
M
basedonarecursiveunfoldingoftherestrictionset.
Weconcludethatthe experimentsperformed usingP Basic
M
in generation ofSSPSs showthat
therun-timeincurredbytheiterationof
SG
becomessignicantwhensystemparametersgrow.
Hence,in orderto makethe calculationof SSPSs forCP-nets applicablein practice we needto
carefullyconsider thenumberofpermutationsymmetries testedin thegeneration oftheSSPSs.
ThenextsectionpresentstechniqueswhichimproveP Basic
M
inthisdirection.
5 Approximation Techniques
In this section we will presentan algorithm which presents an improved implementation of the
predicate P Basic
M
. Section 5.1 presents the algorithm. Section 5.2 presents experimental results
obtainedusingtheDesign/CPNOPStoolwheretheimprovedalgorithmpresentedinthissection
isusedtodeterminesymmetrybetweenmarkings.
5.1 Presentation ofthe Algorithm
TheproblemwhenusingP Basic
M
forthesymmetrycheckbetweenmarkingsisthatintheworstcase
j
SG
jpermutationsymmetrieswillbechecked.Whendeterminingsymmetrybetweenmarkingsa
selectionof simplecheckscanin manycasesdeterminethat twomarkingsare notsymmetricor
determineasmallersetofpermutationsymmetriesthat haveto bechecked.
InthissectionwewillpresentanewalgorithmforP
M
whichgiventwomarkings,M
1
is a super-set of the set of permutation symmetries mappingM
1
arenot symmetric.However,if
M1;M2
is non-empty wehaveto test
theindividualpermutationsymmetriesin
M1;M2
.Inworstcasej
M1;M2
jpermutationsymmetries
havetobechecked.ThisisthecaseifM
1 andM
2
arenotsymmetric.IfM
1
gj+1 permutation symmetries haveto
be checked. Hence, the goal of the approximationtechnique is to construct
M
gcanbedetermined eÆciently. Thisis, however,notthe case ifthe CP-net
contains structured colour sets. Nevertheless, we will use the technique to eÆciently obtain an
approximation
g,thus reducing thenumber of permutation
symmetrieswhichhavetobecheckedcomparedtotheapproachusedinP Basic
M
.Thisisobtainedat
thecostofdoingtheapproximation.Inthefollowingwewillshowhowsuchanapproximationcan
beobtainedeÆcientlywhen
SG
isrepresentedasarestrictionset.Theapproximationtechnique
isbasedonideasfrom[8,1].
The set of permutation symmetries mapping amarking M
1
to another marking M
2
canbe
found asthe intersection of sets of permutation symmetries mapping M
1
2 P. Similarly, it is shown in [8] and proved in [1] how the set of permutation symmetries
betweensuchmarkingsofplaces,i.e.,multi-sets,canbedeterminedastheintersectionoversetsof
symmetriesbetweensetswithequalcoeÆcientinthemulti-sets,i.e.,forapermutationsymmetry
tobeasymmetrybetweenms
1
andms
2
itmustensurethatacolourappearingwithcoeÆcientc
inms
1
mustbemappedintoacolourappearingwiththesamecoeÆcientinms
2
.Wewillillustrate
usingtheCP-netof theDistributedDatabase(Fig. 1)asanexample.
Let ms
1
=1`d(2)+1`d(3)and ms
2
=1`d(1)+1`d(2)betwo markingsof athe place Inactive
withcoloursetDBM.Inms
1
twocolours(d(2)andd(3))appearwithcoeÆcient1andonecolour
(d(1))appearwithcoeÆcient0.Wecanexpressthemulti-setofcoeÆcientsas2`1+1`0.Inms
2
it is also the case that two colours (d(1) and d(2)) appear with coeÆcient 1 and one colour
(d(3))appearwithcoeÆcient0.Hence,ms
2
hasthesamemulti-setofcoeÆcientsasms
1
namely
2`1+1`0.A permutation
DBM
of the colour set DBM is apermutation mapping ms
1
ensuresthatacolourappearingwithcoeÆcient1inms
1
ismappedtoacolourappearing
with coeÆcient 1 in ms
2
, and similar for the rest of the coeÆcients (here just 0). Hence, we
can construct a restriction set representing the set of permutations between ms
1
and ms
2 by
constructingarestrictionforeachofthecoeÆcientsappearinginms
1
Intheaboveexamplethetwomulti-setshadthesamemulti-setsofcoeÆcients.Thisisanecessary
requirementforthetwomulti-setstobesymmetric[1].Ifnot,theleftandright-handsidesofthe
constructedrestrictionsdonotcontainthesamenumberofelements,andthusdoesnotrepresent
avalidsetofpermutations. Multi-setsofcoeÆcientsareformallydened in[1].Wedene
multi-sets of coeÆcients using the notation used in this paperbelow and present an algorithm which
calculatesthesetofpermutationsymmetriesbetweentwomulti-setsoveranatomiccolourset.
Denition:
For amulti-set ms over acolour set C wedene Coefficients
C
(ms) asthe set of coeÆcients
appearingin ms:
Coefficients
C
(ms)=fi2Nj9c2C such thatms(c)=ig
Letmsbeamulti-setoveracolourC.Fori2Coefficients
C
(ms)wedenethei-coeÆcient-class
formsastheset ofcoloursin C appearingwithcoeÆcienti:
C
i
(ms)=fc2Cjms(c)=ig
Wedenethemulti-setofcoeÆcientsformsby
Cfms(ms)=fms(i)`ig
i2CoeÆcientsC(ms)
multi-setsms
calculatethesetf
A
Thealgorithmtests whetherCfms(ms
1
)=Cfms(ms
2
)(line1), i.e., themulti-setof coeÆcients
are equal. If not ms
1
and ms
2
are not symmetric [1], i.e., the empty set is returned (line 4),
otherwise arestrictionset is constructed containinga restriction(C
i
thecoeÆcientsiin Coefficients(ms
1
)(line2).
Giventwomarkings,M
1 andM
2
,thealgorithmFindPermutationSymme-tries
M
calculates
the aset of permutation symmetries
M1;M2
as theintersection of
SG
and the sets of
permu-tations betweenthe markings ofthe individual places with atomic colour sets (calculated using
FindPermutations
hasanatomiccoloursetgdo
3:
IftheCP-netonlycontainsplaceswithatomiccoloursetstheset
M
1
;M
2
ofpermutation
symme-triescalculatedusingFindPermutationSymmetries
M
g. If the CP-net also contains places with structured colour sets then
M1;M2
to improvetheP Basic
M
algorithmpresentedin Sect. 4,i.e.,to
reduce the number of permutation symmetries which have to be checked. The new algorithm
P
1: for all2FindPermutationSymmetries
M
2: if TestPermutationSymmetry' (,M
1
The algorithm repeatedly selects apermutation symmetry from the set of permutation
sym-metriesapproximatedusingFindPermutationSymmetries
M
(line 1)and testswhether isa
symmetrybetweenthetwomarkings(lines2-4).Theiterationstopswhenapermutation
symme-tryforwhich (M
1 )=M
2
isfound(line3)ortheentire sethasbeeniterated(line6).P Approx
) uses TestPermutationSymmetry' (,M
1 ,M
2
), amodiedversionof thealgorithm
TestPermutationSymmetry presented in Sect. 4, to determine whether (M
1 ) = M
2 . The
dierenceisthatgivenapermutationsymmetryandtwomarkings,M
1 andM
2
,
TestPermu-oftheplaces withatomic coloursetsare alreadyaccountedfor intheapproximationand donot
haveto betestedagain.
The complexity of the calculation of FindPermutationSymmetries
M
is independent of
j
SG
j. This is a very attractive property, since the experimental results presented in Sect. 4
showed that iterating the group of permutation symmetries is not applicable in practice when
thesymmetryspecicationdeterminesalargeset ofpermutationsymmetries.
If the CP-net contains places with atomic colour sets P Approx
M
potentially tests fewer
per-mutation symmetries than P Basic
permutation symmetries are checked when determining whether two markings are symmetric,
whereasat mostjFindPermuta-tionSymmetries
M
permutationsymmetriesaretestedusingP Approx
M
.Theexperimentalresultspresentedlaterinthis
sectionshowthatforthetwoCP-netsusedintheexperimentstheapproximationisveryclose(or
even equal)to theexactset ofpermutationsymmetries mappingM
1 to M
2
. Hence,thenumber
of permutation symmetrieswhich have to be tested is verylow in practice. Furthermore,if the
multi-setsofcoeÆcientsaredierentformarkingsnopermutationsymmetrieshavetobetestedto
multi-setsofcoeÆcientsaredierentformarkingsnopermutationsymmetrieshavetobetestedto