1.1. Atomaire processen. Net zoals strings (woorden) gevormd worden door letters uit een alfabet, worden processen

1

Hoofdstuk 1: Basis Proces Algebra

Hoofdstuk 1 BPA Basis Proces Algebra

1.0.

Inleiding

Wat is een proces? Een proces is iets dat voortgaat, verloopt, met stappen in de tijd. Processen komen overal in het dagelijks leven voor: in de rechtsspraak, in de industrie, en in de informatica. Net zoals je kunt rekenen met getallen in de algebra, of met logische uitspraken in de

logica,

kun

je

ook

rekenen

met

processen.

Zo’n

rekenmethode

voor

processen,

procesalgebra genaamd, is ongeveer 20 jaar geleden ontwikkeld, door onder andere de engelse on-

derzoekers Hoare en Milner. Beiden

hebben

voor

hun

werk

de

Turing Award gekregen, de ‘Nobelprijs voor informatica’. Procesalgebra

is in de ja-

ren 60 begonnen als automaten-

theorie, een onderdeel van ‘For-

mele Talen’. Ruwweg is een automaat iets dat in verschillende toe-

standen kan verkeren, en acties

Robin Milner

Tony Hoare

kan doen om van de ene in de andere toestand te komen. Een automaat kan daarmee ook gezien worden als een proces. De acties zijn hier nog onderling onafhankelijk. In de jaren 70 kwam de

noodzaak op om ook communicatie tussen acties te beschrijven; het trefwoord hierbij is ‘concurrency’. Systemen zijn nu niet langer op zichzelf staand, maar ‘interactief’ of ‘reactief’.

De belangrijkste calculi voor dergelijke systemen of procesen zijn CSP (Communicating Sequential Processes) van Hoare, en CCS (Calculus of Communicating Systems) van Milner.

Begin jaren 80 is een variant van deze formele systemen ontstaan die ACP heet, Algebra of Communicating Processes. In dit eerste hoofdstuk behandelen we de kern van ACP, Basis Proces algebra (BPA).

College ITI, deel I , Procesalgebra, VU, voorjaar 2002

06-02-2002

2


1.1.

Atomaire

processen.

Net zoals strings (woorden) gevormd worden door letters uit een alfabet, worden processen opgebouwd uit atomaire processen, die niet verder te ontleden zijn. We geven die atomaire

processen, ook wel ‘acties’ of ‘stappen’ of ‘events’ (gebeurtenissen) genoemd, vaak aan met letters a,b,c,... Wat die acties precies zijn, hangt af van de toepassing.

1.1.1.

V O O R B E E L D . Gegeven is een bord met 5 maal 5

vakjes. We willen de beweging van de zwarte stip (

) over

het bord beschrijven. De acties zijn: up, down, left, right, afgekort als, u, d, l, r. Het

na

elkaar

doen

van

acties

geven

we

aan

als

vermenigvuldiging. Zo is r.r.r de beweging die bestaat uit 3

stappen naar rechts; en r.r.r.u.u.u is een beweging van de punt naar het grijze veld. Vaak laten we de ‘punt’ weg, zodat

het laatste ‘bewegingsproces’ is: rrruuu. Een andere manier

Figuur 1.1

om op het grijze veld te komen is rururu. We gebruiken ook

exponenten, net als in gewone algebra, en kunnen dan voor de laatste twee processen schrijven: 3

3

3

r u , respectievelijk (ru) .

1.1.2. OPGAVE. Hoeveel manieren zijn er om met de acties u,d,l,r de stip naar het grijze veld te brengen? En als alleen de acties u en r gebruikt mogen worden?

1.2. Samengestelde

processen.

Boven hebben we al gezien hoe uit atomaire processen (acties) processen kunnen worden

samengesteld door de operatie “.”, vermenigvuldiging, ook wel ‘sequentiële compositie’ genoemd, omdat het een sequentie van acties maakt.

Er zijn nog andere operaties om processen op te bouwen. De eerste andere operatie is

met de “+”, som, ook wel ‘alternatieve compositie’ genoemd. Bijvoorbeeld in de situatie van Figuur 1.1 staat r

3

u

3

+ (ru)

3

voor het proces dat òf r

3

u

3

doet,

3

òf (ru) . Er wordt dan dus een

keuze gemaakt tussen beide alternatieven.

1.2.1. VOORBEELD. We bepalen het proces dat de beweging(en) beschrijft van de stip naar het

grijze veld op het 2-bij-3 bord als in Figuur 1.2.1(a), met alleen u en r acties. In de vakjes zijn

de ‘tussen-processen’ al ingevuld. Het gevraagde proces is dus r(ru + ur) + urr. Merk op dat in

deze ‘procesterm’ in één uitdrukking verschillende mogelijke procesverlopen weergegeven zijn.

Als we alleen in de feitelijke executies (procesverlopen) geïnteresseerd zijn, moeten we


06-02-2002

3


bij

elke

+

een

keuze

maken; we krijgen dan

een “trace” of executie.

rr

Dit proces heeft dus 3

r

traces; rru, rur en urr.

r(ru+ur) + urr

1.2.1.OPGAVE. Zie het 3-

ru + ur

u

bij-3 bord in Figuur 1.2.1(b). (i)

Bepaal

dat

de

naar

het

bewegingen

proces van

(a)

beschrijft, met alleen

(b) Figuur 1.2.1

u en r acties.

(ii)

Geefde afzonderlijke traces.

Met de + en de . hebben we de basis-operaties om samengestelde processen te maken

uit de elementaire acties. Processen die alleen opgebouwd zijn uit atomen met + en ., heten basis procestermen. Er gelden voor + en . enkele wetten net als in gewone algebra. Deze staan in Tabel 1.1. Sommige van deze wetten zijn letterlijk hetzelfde als in gewone algebra, - maar de wet

x + x = x is nieuw, en betekent dat de keuze tussen proces x doen of proces x doen

hetzelfde is als proces x doen.

Merk ook op dat de “.” hier niet commutatief is, zoals in gewone algebra; het proces ur

is verschillend van ru, de volgorde van de acties doet er toe. Wel is u + r = r + u.

(A1)

x + y = y + x

(commutativiteit)

(A2)

x + (y + z) = (x + y) + z

(associativiteit)

(A3)

x + x = x

(idempotentie)

(A4)

(x + y) . z = x.z + y.z

(rechtsdistributiviteit)

(A5

x.(y.z) = (x.y).z

(associativiteit)

Table 1.1: BPA

1.2.3. OPGAVE.

Show that (a + b)

3

= a(a(a + b) + b(a + b)) + b(a(a + b) + b(a + b)).

1.2.4. NOTATIE.

om het gebruik van haakjes te beperken schrijven we bijvoorbeeld a.b.c in plaats van


06-02-2002

4


(a.b).c;

de . bindt sterker dan de +, dus (a.b) + c schrijven we als a.b + c;

buitenste haakjes worden weggelaten;

de . wordt vaak weggelaten, net als in ‘gewone’ algebra, dus in plaats van a.b + c schrijven

we ab + c.

1.2.5. OPMERKING. We hebben niet algemeen z (x + y) = zx + zy, met als instantiatie bijvoorbeeld a(b + c)

= ab + ac. De reden is dat de ‘timing’ van de keuzemomenten verschillend is: in a(b + c) wordt na de a-actie pas voor b of c gekozen; in ab + ac wordt voor de a-actie, al meteen bij het begin, gekozen. Dit verschil in timing

van keuzes is belangrijk wanneer er communicatie tussen acties in het spel is, zoals in een later hoofdstuk. Dat

de vergelijking a(b + c) = ab + ac dan onwenselijk is, wordt dan precies gemaakt. Intuitief kunnen we het verschil tussen a(b + c) en ab + ac nu al inzien, bijvoorbeeld als volgt: automaten, K1 en K2.

Figuur 1 toont twee koffie-

K1 werkt zo: na inworp van 1 euro kan op de

knop K (koffie) gedrukt worden, of op T voor thee.

Als dit er is, volgt uitgifte van het gewenste artikel.

K

T

K

T

Als beide artikelen op zijn, gebeurt er niets.

K 2 werkt zo: Hier moet men van te voren

K1

kiezen voor koffie of thee; als het er is, volgt uitgifte,

K2

anders gebeurt er niets. Als de reservoirs altijd goed

gevuld zijn, is er geen verschil tussen K 1 en K2 . (Als ze altijd leeg zijn, ook niet.) Maar als ze soms vol, soms leeg zijn, is er wel verschil. Bij K1 kunnen we na weigering van knop K nog proberen thee te nemen. Maar bij

K2 zijn we na weigering van knop K onze euro kwijt. Dus:

1.3.

Procesgrafen.

‘procesalgebra’, procesgrafen.

In

deze

bestaande

uit

sectie

inworp.(K + T) ≠ inworp.K + inworp.T.

behandelen

procesgrafen,

of

we

een

preciezer,

BPA,

een

equivalentieklassen

van

model

voor

1.3.1. D EFINITIE. Laat A een verzameling atomaire acties zijn. Een procesgraaf over A is een drietal (N, E, r) zodat: N is een verzameling van elementen die we punten of knopen noemen; E is een verzameling gelabelde pijlen; dat wil zeggen: E

N x A x N. Om aan te geven dat

een element (s, a, t) in E zit, gebruiken we de notatie s → a t. Gelabelde pijlen heten ook transities. r ∈ N is een bijzondere knoop, die we de wortel noemen. Een knoop heet een eindknoop als er geen pijlen uit vertrekken. We zullen altijd samenhangende procesgrafen beschouwen, dat wil zeggen dat elk punt vanuit de wortel bereikbaar moet zijn. De graaf mag dus geen ‘loshangende’ stukken bevatten.


06-02-2002

5


(Als in de loop van een constructie op grafen toch onbereikbare delen ontstaan, halen we deze meteen weg. Het verwijderen van onbereikbare delen heet ‘garbage collection’.

Een procesgraaf heet cyclisch als hij een lus (of ‘cykel’)

bevat (dat wil zeggen dat vanuit

een knoop in een aantal stappen dezelfde knoop weer te bereiken valt), anders acyclisch. Een punt heet cyclisch als het op een cykel ligt. Een eindigsplitsende graaf is een graaf, waarbij uit elke knoop slechts eindig veel zijden uitgaan. Een eindige graaf

(i)

bevat slechts eindig veel knopen en zijden. Een een

graaf

waarin

acyclisch

nooit

twee

samenkomen; als

er

p r o c e s b o o m is

die

naar

anders

iedere

is

a

a

en

zijden

b

b

gezegd,

knoop

(ii) a

a

a

b

c

(iii)

b

(iv) a

c

b

a

b

c

a

a

b

een

uniek pad is vanuit de wortel. De procesgraaf bestaande uit alleen

een

wortel,

en

geen

pijlen, heet triviaal. Procesgrafen kunnen oneindig zijn, en oneindige vertakkingen vertonen.

(v)

(vi) a

b

a

b

a

b

(vii) a

a

a

a

a

a

a

a

a

a a

1.3.2. VOORBEELDEN.

1.3.3. VOORBEELD . Het volgend voorbeeld van een procesgraaf, in Figuur 1.3, geeft het procesgedrag van een Stack, waarop data elementen 0 en 1 gezet kunnen worden. De actie 0 wil zeggen: plaats een 0 op de stack; idem voor 1. Met andere woorden: push 0, push 1. De onderlijnde acties 0 en 1 betekenen: pop 0, pop 1 (haal 0 van de stack, resp. 1). We zullen later zien hoe dit proces gespecificeerd kan worden met recursievergelijkingen.

1.4.

Het

graafmodel.

We zullen nu van deze verzameling procesgrafen een model maken van de theorie BPA.


06-02-2002

6


1.4.1.

DE F I N I T I E .

Gegeven

een

alphabet A van atomaire acties, is

sta ck

G(A) de verzameling van alle niet-

triviale procesgrafen over A waarvan

0

de wortel acyclisch is. 0

1.4.2. DEFINITIE.Op G(A) definieren we operaties ‘som’ en ‘product’ als

0

volgt. Zij g1, g2 ∈ G(A). De

g1 , + +

som

g2

0

1

0

0

1

1

1

1

1

0

0

1

0

1

0

1

0

1

0

1

1

wordt

gedefinieerd als de graaf die ontstaat door de wortels van g 1 en g 2 met elkaar te identificeren. Het product g 1

..

terminating

sta ck

0

g2 van g1 en g2

0

ontstaat door g2 vast te plakken aan alle

eindknopen

wordt

steeds

van

de

geïdentificeerd

g1 .

wortel

met

de

Daarbij van

g2

betreffende

0

0

0

1

0 1

1 0

1

0

1

1 0

1

0 1

1

1

0 0

1

1

eindknoop van g1.

1.4.3. VOORBEELD. Zie Figuur 1.6.

1.4.4. D ISCUSSIE . Waarom bevat G(A) alleen de grafen met acyclische wortel? Dit lijkt vreemd, omdat

daarmee interessante en nuttige procesgrafen als die van Stack in Figuur 1.5 uitgesloten zijn. Dit is gedaan vanwege het volgende probleem. Beschouw grafen g1, g2 als in Figuur 1.7.

Als we deze optellen zoals gedefinieerd voor G(A), door de wortels te identificeren, krijgen we g3. Maar als we

g1 eerst ‘uitrollen’ tot de graaf h1 die oneindig veel a-stappen doet, en idem g2 tot h2 die oneindig veel b-stappen

doet, en dan h1, h2 optellen, krijgen we h3. Duidelijk is dat g3 en h3 zeer verschillend zijn wat betreft mogelijke

paden: in g 3 is een pad dat bijv. afwiselend een a-stap en en b-stap doet, maar in h 3 niet. Toch is h 3 de

‘bedoeling’, want cyclische grafen zijn eigenlijke een verkorte versie van hun ‘unwinding’. Als we toch root-

cyclische grafen willen optellen, moeten we eerst een klein stukje de graaf uitrollen (‘unwinding’), zodat de root acyclisch wordt. Dit gebeurt als volgt.

1.4.5. DEFINITIE. Zij g = (N, E, r) een procesgraaf, niet noodzakelijk root-acyclisch. Dan is g° =

(N°, E°, r°)

de root-unwinding van g, als volgt gedefinieerd:

r° is een nieuwe knoop, dus r ∉ N;


06-02-2002

7


N° = N U {r°}; E° =

E U {(r°, a, v) | (r, a, v) ∈ E}

Met andere woorden, r° bootst r na:

g1

g2

als er een ‘oude’ transitie r →a v in g

a

was, komt er een ‘nieuwe’ transitie r°→a v in g°.

b

c

Opmerking: Bij het construeren van

laten staan, en de nieuwe r ° met de

g

1

+ + g

b

daardoor

g

2

nieuwe transities r° → a v daarbij te die

a

a

g° is het handig om de ‘oude’ g te

tekenen.Knopen

b

a

wortel , moeten vervolgens worden

.. g

a

c

b

a

verwijderd (garbage collection).

2

a

c

onbereikbaar worden uit de nieuwe

1

b

b

a

a

1.4.6. OPGAVE. Zij g root-acyclisch. Laat zien dat g en g° dan hetzelfde zijn.

1.4.7. OPGAVE. Zij g de procesgraaf van Stack in Figuur 8.5. Geef g°.

Door het procedé van root-unwinding te itereren, kunnen we een procesgraaf helemaal

cycle-vrij maken, dat wil zeggen, uitrollen tot boom (‘tree-unwinding’).

1.4.8. OPGAVE. Geef de eerste paar ‘lagen’ van de treeunwinding van de Stack procesgraaf.

1.4.9. D EFINITIE. acties.We

Zij A een verzameling atomaire

definieren

termopbouw)

de

inductie

procesgraaf

(gesloten) BPA-term t:

G(a)

(met

G(t)

naar

van

de

een

G(ab)

a b

G((a +

a)(b + b))

a

a

b

b

b

= o →a o

G(s + t) = G(s) + + G(t)


06-02-2002

8


G(s.t) = G(s)

..

g

G(t)

g

1

a

Dit is nog niet alles, want om

g

2

3

b

a

b

een model te hebben van BPA moeten ook de axioma’s van BPA en

wat

daaruit

h

volgt,

waar zijn. Dat betekent dat we bijvoorbeeld de procesgrafen G((a + a)(b + b)) en G(ab) moeten BPA Deze

identificeren,

omdat

(a + a )(b + b) = ab. twee

grafen

zijn

in

h

1

a

b

a

b

a

b

a

b

Figuur 1.8 weergegeven.

h

2

a

3

b

a

b

a

b

a

b

a

b

Met welk criterium moeten we dergelijke grafen identificeren?

Figuur 1.8

Het blijkt dat de juiste notie is:

de notie van bisimulatie. Deze notie speelt een centrale rol in procesalgebra.

1.5.

Bisimulatie.

1.5.1. D EFINITIE . Laten g = (N, E, r) en g’ = (N’, E’, r’) twee procesgrafen zijn over de verzameling A. Een relatie R

N x N’ heet een bisimulatie tussen g en g’, notatie R: g

g’,

als

(r, r’) ∈ R voor alle a ∈ A geldt: als s →a t

en (s, s’) ∈ R, dan is er een knoop t’ ∈ N’ zodat s’ →a t’

en (t,t’) ∈ R. en vice versa.

We noemen twee procesgrafen g en g’ bisimilair, notatie g

g’, als er een bisimulatie bestaat

tussen g en g’.


06-02-2002

9


g

h

R

s

⇒

t

a

g

R

s

s'

h

R

s

⇒

t a

g

a R

R

s

t'

h t

a s'

t'

t

a

s'

g

h

a R

t'

Figuur 1.9

1.5.2. OPGAVE. Laat zien dat

Als g

een equivalentierelatie is.

g’ denken we aan g en g’ als ‘dezelfde’ graaf, die verschillende ‘versies’ zoals g

en g’ kan hebben. Een mogelijk probleem is nu dat de optelling + en vermenigvuldiging van g1 en g 2 wel eens af zouden kunnen hangen van de gebruikte versies g 1’ en g2’. We zouden een probleem hebben als het volgende geval zich voordeed:

g1

maar niet

g1’,

g1 + + g2

g2

g2’,

g1’ + + g 2 ’,

en analoog voor vermenigvuldiging. Gelukkig doet dit geval zich niet voor, en hebben we:

1.5.3. PROPOSITIE.Gegeven zijn vier procesgrafen g, h, g’, h’ ∈ G(A).Dan: (i) g

g’, h

h’ ⇒ g + h

g’ + h’


06-02-2002

10


(ii) g

g’, h

h’ ⇒ g . h

g’ . h’

We kunnen nu het graafmodel definiëren.

We hebben nu de volgende belangrijke stelling, waarvan het precieze bewijs nog wat

detailwerk vergt, dat we achterwege laten. 1.5.4.

D EFINITIE . Het graafmodel is het grafendomein G(A) met daarin bisimilaire grafen

geidentificeerd, notatie G(A)/

, in woorden G (A)

vermenigvuldiging g.g’ van g, g’ ∈ G(A)/

modulo

. Optelling g + g’ en

,worden verkregen door willekeurige (root-

acyclische) representanten (‘versies’) van g, g’ op te tellen, respectievelijk te vermenigvuldigen.

1.5.5. S T E L L I N G . Zij A een actie-alphabet. Dan geldt voor alle gesloten termen s, t ∈ Ter(BPA):

BPA

s = t ⇔

We hebben met G(A)/

G(s)

G(t).

dus een model van BPA gemaakt. De interpretatie van term t ∈

Ter(BPA), is als volgt: [t] ] = {g | g

G(t)}.

Deze stelling is een correctheids- en volledigheidsstelling van de

theorie BPA ten opzichte van de semantiek gegeven door het graafmodel. Een toepassing van de volledigheidsstelling is dat we nu kunnen bewijzen dat sommige vergelijkingen niet uit BPA zijn af te leiden. Bijvoorbeeld, de vergelijking a(b + c) = ab + ac is niet uit BPA af te leiden. Namelijk, bekijk de grafen G(a(b + c)) en G(ab +

ac). Het is makkelijk te bewijzen dat deze grafen niet bisimileren. Dus is de vergelijking niet afleidbaar.

1.4.7. OPGAVE. (i) Bewijs dat g

g°.

(ii) Zij g* de tree-unwinding van g. Dan geldt: g passen.

1.4.8. OPGAVE. (i). (ii)

(iii) (iv)

g*. ‘Begrijp’ dit feit door het op enkele voorbeelden toe te

Goed of fout: elke graaf met oneindig veel punten heeft een oneindig pad.

Goed of fout: als grafen g en h bisimilair zijn, hebben ze hetzelfde aantal eindknopen. Goed of fout: als g en h bisimilair zijn en g

is acyclisch, dan ook h.

Bewijs: als g en h bisimilair zijn, en g heeft een oneindig pad, dan heeft ook h een oneindig pad.

1.4.9. OPGAVE. Zij g een acyclische graaf. Bewijs dat de volgende twee eigenschappen equivalent zijn: College ITI, deel I , Procesalgebra, VU, voorjaar 2002

06-02-2002


(i)

(ii)

11

g heeft geen punt waarin twee zijden samenkomen;

naar ieder punt van g is er een uniek pad vanuit de wortel.

Laat zien dat voor de equivalentie van (i) en (ii), het gegeven dat g acyclisch is, echt nodig is. 1.4.10. OPGAVE. Bewijs dat uit BPA niet afleidbaar is: a(b + c) = ab + a(b + c) + ac.


06-02-2002

12


8.2.5. DEFINITIE. Een vergelijking s = t is afleidbaar in de theorie BPA, notatie BPA

s = t,

als men uitgaande van de axioma’s van BPA, en met behulp van de gebruikelijke afleidingsregels voor equationele logica (zie Intermezzo *8.2.5.1), s = t kan afleiden.

*8.2.5.1. INTERMEZZO. De volgende tabel geeft het afleidingssysteem ‘Equationele Logica’, voor een algemene vergelijkingenspecificatie (Σ, E) met signatuur Σ en stel vergelijkingen E.

s = t

(als s = t

s = t

_____________ s

σ

= t

∈ E, axioma)

(voor elke substitutie σ)

σ

s 1 = t1 ,..., sn = tn

______________________________

(voor elke n-aire F ∈ Σ

F(s 1 ,...,s n ) = F(t1 ,...,t n )

congruentie)

t = t

reflexief (axioma)

t 1 = t2

t 2 = t3 ____________________________

transitief

t1 = t 3 s = t

___________

symmetrisch

t = s

Tabel 8.2: Equationele Logica

Hierbij is σ: Var → Ter(Σ) een substitutie.Voor t ∈ Ter( Σ)

is t

σ

als volgt gedefineerd, met

inductie naar de opbouw van t:

x

σ

= σ (x )

F(t 1 ,...,t n )

σ

= F(t1

σ

,...,t n

σ

)

Voor BPA is het afleidingssysteem Equationele Logica dus als volgt (met s,t,t 1 ,t 2 ,t 3 ∈ Ter(BPA):


06-02-2002

13


(A1),...,(A5)

axioma

s = t

_______ s

σ

= t

voor elke substitutie σ

σ

s 1 = t1 ,..., s2 = t2 ________________

congruentie voor +

s 1 +s2 = t1 + t2

s 1 = t1 ,..., s2 = t2 ________________ s 1 . s2 = t1 .

congruentie voor .

t2

t = t

reflexief (axioma)

t 1 = t2 t 2 = t3 ____________________________

transitief

t1 = t 3 s = t

___________

symmetrisch

t = s

Tabel 8.3: Equationele Logica voor BPA

8.2.4.2. VOORBEELD. BPA

aa + aa = a(a + a). Zie Figuur 8.2.

x + x = x _______ a + a = a

x + x = x (ax) __________

(ax)

(subst)

a = a + a a = a (ax) _________________

(subst)

aa + aa = aa aa = a(a + a) _____________________________________________ aa + aa = a(a + a)

(congr .)

(trans)

Figuur 8.2


06-02-2002

14


Een afleiding uit BPA heeft dus de vorm van een boom van vergelijkingen. Een ander, equivalent, ‘format’ is zo’n bewijs te geven als een rij vergelijkingen:

1. x + x = x

(ax)

2. aa + aa = aa

(1, subst)

3. a + a = a

(1, subst)

4. a = a

(ax)

5. a(a + a) = aa

(3,4, congr)

6. aa = a(a + a)

(5, symm)

7. aa + aa = a(a + a)

(2.6. trans)

Figuur 8.2

In de praktijk doen we dit wat simpeler, namelijk door een rij van vergelijkingen achter elkaar te zetten: aa + aa = aa = a(a + a).

(Voor het tentamen volstaat de laatste methode.)


06-02-2002



15

06-02-2002

1.1. Atomaire processen. Net zoals strings (woorden) gevormd worden door letters uit een alfabet, worden processen

Recommend Documents