Formele systemen en hun toepassingen

2005

17-01-05 9u

1. Definieer de notie van "zwakke simulatie tot op ~" (weak simulation up to ~) en formuleer en bewijs het verband met zwakke equivalentie voor concurrente proces expressies (7 punten)

2. Geef een mogelijke representatie van binaire bomen in de pi-calculus (7 punten)

3. Bespreek waarom klassieke equivalentie van automaten (de zogenaamde taal-equivalentie) niet geschikt is als equivalentie-maat voor reactieve systemen (6 punten)

Bijvragen:

1. =lambda=> betekent dat er verschillende tau acties voor en achter lambda kunnen voorkomen. als P~Q en P=lambda=>P' en dus Q=lambda=>Q' met P'~Q' zijn die sequenties van taus en lambda hetzelfde voor beiden experimenten?

2. geen

3. stel dat we systemen beschouwen zonder interne reacties en we daar ~ op definieren. Is dit dan een voldoende maat om systemen equivalent te noemen of kan je een voorbeeld geven van twee systemen die ~ zijn maar niet observationeel hetzelfde doen?

17-01-05 14u

1. Bewijs dat sterke equivalentie een procescongruentie is.

2. Hoe kan je recursieve proces definities simuleren met behulp van de ! operator in de pi-calculus?

3. Kan je een M en N vinden waarvoor A= tau. B + M en B= tau.A + N niet zwak equivalent zijn? Zo ja, geef een A en B. Zo nee, bewijs.

05-02-05 9u

1. Formuleer en bewijs "Unique solution of equations".

2. Schrijf een sequential process expression voor een binaire stack + teken een deel van de (oneindige) transitiegraaf.

3. Bespreek hoe je datastructuren kunt voorstellen in de pi-calculus (= booleans + lijsten geven en uitleggen). Vluchtige (ephemeral) en persistente data uitleggen en verschil geven.

2004

19-01-04

1) Leg uit waarom klassieke equivalentie van automaten ( taal-equivalentie ) ontoereikend is voor reactieve systemen

-> Gewoon schema'tje tekenen van die koffie/thee automaat

2) formuleer de stelling ivm de unieke oplossing van een stelsel vergelijkingen en bewijs ze

-> Maak vooral ivm theorië dat ge de intuïtie erachter snapt

3)

A = tB + M B = tA + N

Zijn er keuzes voor M, N zodat A en B niet zwak equivalent zijn ? Zoja, geef een voorbeeld, zo nee, bewijs.

-> A & B altijd zwak equivalent -> Intuïtie achter bewijs opnieuw belangrijk

Al bij al niet zo moeilijk, als ge't snapt moet het zeker lukken... Hij stelt wat bijvragen ( heeft mij erin laten lopen bij vraag 1:

. zijn states, abcd externe actions . . / \ | a a a / \ | . . . | | / \ b b b b | | / \ . . . . | | | | c d c d | | | | . . . . hij vroeg of deze sterk equivalent zijn -> nee zei ik hij vroeg of ik ze observationeel kon onderscheiden -> na wat twijfelen: nee toen was ik dus mijne kluts kwijt, want sterk equivalent moet zogezegd overeenkomen met observationeel equivalent

'fin, hij gaf toe dat het een vervelend voorbeeld was .)

2003

18-08-03

1) Geef een sequentiele proces expressie voor een binaire stack (die oneindig kan groeien) teken hiervan het transitie-diagramma

2) Leg uit hoe in de pi-calculus met behulp van ! recursieve processen kunnen gebruikt worden.

3) Definieer bisimulatie en geef enkele voorbeelden/tegenvoorbeelden.

28-01-03

1) formuleer en bewijs de stelling van unique handling (hfdst 10 dus)

2) oefening maak een specificatie (sequential process) en een implementatie (concurrent process) van een boolean-stack, en leg in grote lijnen uit hoe je zou bewijzen dat de implementatie aan de specificatie voldoet.

3) wat is sterke simulatie tot op congruentie, wat is de relatie hievan met sterke equivalentie, bewijs deze relatie