Formele systemen en hun toepassingen

2004-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.

2003-2004

30-01-04

1) Geef de definitie van bisimulatie, geef ook vb'en en tegenvb'en.

2) Definieer een sequentiele proces dat een stapel van booleaanse waarden voorstelt (=specificatie), geef een implementatie van zo'n stapel mbv concurrente proces expressies (opgebouwd uit een aantal kleine bouwstenen). Leg uit (in grote lijnen) hoe je de correctheid van je implementatie kan bewijzen.

3) Er is een relatie gedefinieerd tussen transities en reacties. Geef en bewijs.

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

2002-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

24-01-03 VM

1) bespreek waarom taal-equivalentie niet meer werkt voor reactieve systemen..

2) definieer bisimulatie en geef enkele voorbeelden/tegenvoorbeelden

blijkbaar verwacht ie bij uw voorbeelden eentje waarbij A B simuleert, B A simuleert maar er toch geen bisimulatie is. (dat had ik niet)

bijvraag: op welke wiskundige structuur kan je zo'n bisimulatie toepassen ? (niet gewoon LTS ofzo)

3) geef een pi-calculus-representatie van binaire bomen. (en een voorbeeldje, en een bijvraag over persistentie, en over rekenen met die bomen met Treecases vb)

18-01-03

(gegeven: een blad met de reactie-regels, de transitie-regels en de structurele congruentie-regels)

1. Formuleer en bewijs de "Unique Solutions of Equations" stelling.

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

3. Ontwerp een sequentiële procesuitdrukking voor een drankautomaat. Deze aanvaardt stukken van .5EUR, 1EUR, en 2EUR. Water kost 1EUR, limonade 1,5EUR. De automaat moet geld kunnen teruggeven. (Bijvraagje: wat indien je rekening wilt kunnen houden met het beschikbare geld in de automaat?)