Formele systemen en hun toepassingen

Fout bij het aanmaken van de miniatuurafbeelding: Bestand is zoek

2006-2007

2007-02-02 9h

1. Definiëer bissimulatie + voorbeelden & tegenvoorbeelden (5pt)
2. Formuleer & bewijs unique solutions (7pt)
3. Hoe worden datastructuren in pi-calculus voorgesteld + leg verschil tussen volatile & persistent data uit. (8pt)

2007-01-16 9h

1. Er is een relatie gedefinieerd tussen transities en reacties. Geef en bewijs.
2. Definieer de notie van "sterke simulatie tot op ~" (strong simulation up to ~) en formuleer en bewijs het verband met sterke equivalentie voor concurrente proces expressies.
3. Geef een mogelijke representatie van binaire bomen in de $\pi$-calculus.

2005-2006

2006-02-03 9h

Volgend weinig origineel vragen trio:

1. Definieer de notie van "sterke simulatie tot op ~" (strong simulation up to ~) en formuleer en bewijs het verband met sterke equivalentie voor concurrente proces expressies.
2. Formuleer en bewijs "Unique solution of equations".
3. Geef een mogelijke representatie van binaire bomen in de $\pi$-calculus.

26-01-06 14u

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

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($\approx$) zijn? Zo ja, geef een A en B. Zo nee, bewijs.

(Spoilers: 1. Stelling 5.6 | 2. p. 95 | 3. Nee)

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. ${\Rightarrow }^{\lambda }$ betekent dat er verschillende $\tau$ acties voor en achter $\lambda$ kunnen voorkomen. als P~Q en P${\Rightarrow }^{\lambda }$P' en dus Q${\Rightarrow }^{\lambda }$Q' met P'~Q' zijn die sequenties van $\tau$'s 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) Kan je een M en N vinden waarvoor $A=\tau .B+M$ en $B=\tau .A+N$ niet zwak equivalent($\approx$) zijn? Zo ja, geef een A en B. 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
|       |    |       |
.       .    .       .

zijn deze sterk equivalent? kan men ze observationeel onderscheiden?

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) Hoe kan je recursieve proces definities simuleren met behulp van de ! operator in de $\pi$-calculus?

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 mogelijke representatie van binaire bomen in de $\pi$-calculus. (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. Hoe kan je recursieve proces definities simuleren met behulp van de ! operator in de $\pi$-calculus?

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