# Modelleren van Complexe Systemen

Ga naar: navigatie, zoeken

# Informatie over het examen

• Duur van het examen: 4 uur
• Het examen bestaat uit 3 delen:
• Gesloten boek over de theorie. (8pt)
• Open boek oefeningen. (7pt)
• Project. (5pt)

# Examens

## 2013-2014

### Maandag 18 augustus 2014

Theory (closed book)

1. (3pts) State and prove the general FO-inexpressivity theorem, and use it to prove there is no FO theory that expresses ${\displaystyle \Phi }$ = "Vertex A can reach vertrex B in graph G. Can you express this statement in other logics?
• Alternatively, state GÃ¶dels incompleteness theorem, and present some implications (with formal proof if given in this course).
2. (3pts) Describe the efficient version of the CTL-model checking algorithm.
1. Formally specify input and output
2. Specify the algorithm for the adequate set {${\displaystyle \neg ,\wedge }$,EX,EU,EG}.
3. Analyze its complexity.
4. What is a simple fairness constraint. Explain how to refine the CTL algorithm in case there are additional fairness constraints.
3. (1pts) We saw a polynomial transformation of propositional formulas into CNF form in which the base operation is as follows: ${\displaystyle \psi [\phi ]}$ by ${\displaystyle \psi [P_{\phi }]\wedge (P_{\phi }\vee \neg \phi )\wedge (\neg P_{\phi }\vee \phi )}$ where ${\displaystyle P_{\phi }}$ is a new propositional symbol. Show that this transformation is not equivalence preserving. In what weaker sense is it "equivalent"?
4. (1pts) We want to express the set of all tuples of students s and teachers t, such that s is enrolled in all courses of t. The following set-expression: {(s,t) : ${\displaystyle \forall }$c (Instructor(t,c) => Enrolled(s,c))} is not correct. Why is it wrong and correct it.

Exercises (open book)

1. Model this in the LTC formalism in an extension of first-order logic. Use the predicate P(grantor, grantee, label,Time) to express the state graph (P for "Permission").
2. The above revoke operation is only one of many known in Access Control (it iscalled "weak global delete" (WGD)). Another often used revocation scheme is the "weak local delete" (WLD). WLD is used for example when an administrator a leaves an IT department but his rights are revoked so that users with permissions from a are not affected. To this end, the administrator b that revokes a's delegation access, takes over all permissions that a had granted. This kind of revocation can only be applied to a delegation edge. It removes this edge and replaces a by b in all edges with grantor a. Add this to your model.
3. What sort of (useful) computational problems can be solved using this LTC? What sort of inference is required for these?
2. The following program computes the integer quotient n/m for stricly positive integers m and n with the fnal result in a. It takes time logarithmic in the quotient a, if we assign unit cost to the integer operations. Shwo that the program is totally correct. Explain non-trivial applications of the "Implied"-inference rule. Hint: for the second loop, it suffices to prove for its input chat c=2^k for some k >= 0 an n < c*m. The invariant of the second loop contains an expression of the form exp1 * m <= n < exp2* m where exp1, exp2 are arithmetic expressions in terms of a and c provinding safe lower and upper bounds for n/m. Find these expressions. Don't forget the variants and their proof.
c:=1;
while c*m <= n do
c:=2*c
od;
a:=0;
while c!= 1 do
c:=c/2;
if (a+c)*m > n then
skip
else
a:=a+c;
fi
od

### Woensdag 22 januari 2014

Theory (closed book)

1. (2pts) State DCA and prove that in general, it cannot be expressed in FO.
2. Solve either the bonus question or the alternative question:
1. (bonus: 5.5pts) LTL-model checking. Specify the input and output of the algorithm in a formal way, give the definition of S^x, ->^x and C^x and explain them briefly, and specify the algorithm and its correctness theorem. For an example, see M^x for verifying phi = not a U b in s=q3.
2. (alternative: 4pts) Discuss the different methods for verifying invariants using LTC.
3. (1pt) What is the two-watched literal scheme?

Exercises (open book)

1. Model the domain of concrete delivery in an extention of FO logic. Use a vocabulary with at least the follwing types: int, Time (subtype of int), Truck, Location, Customer (subtype of Location), ProductionSite (subtype of Location) and the functions (which are input for the CDP): Capacity: Truck -> int, Start: Customer -> Time, End: Customer -> Time, RequestedAmount: Customer -> int, DeliveryTime:-> int, TravelTime: Location x Locations -> Time, Depot:-> Location.
2. which inference is needed to solve the CDP?
2. Consider the following program P which takes as input an integer variable > 0 and array a[1..N] and returns p=1 if a is a palindrome and p=0 otherwise. Show that |-tot (N>=1) P (p=palindrome(a[1..N])) where palindrome(a[1..N]) is 1 if a[i]=a[N+1-i] for every 1<=i<=N and 0 otherwise. Explain non-trivial applications of the "Implied"-inference rule.
p = 1;
i = 1;
while (p = 1 & i <= N/2) {
p = (a[N+1-i]=a[i]);
i = i + 1;
}

## 2012-2013

### Vrijdag 18 januari 2013

Gesloten boek deel (theorie)

• (3pts) Bewijs dat de eindigheid van het universum niet in FO kan uitgedrukt worden
• (3,5pts) Bonusvraag: LTL model checker
• constructie S^x
• constructie ->^x
• een voorbeeld geven van een pad waaraan toch niet voldaan is. Hetzelfde tekeningetje als in de slides was gegeven.
• hoe M^x gebruikten om te checken of M,q_3 |= ~(a U b)
• (3pts) Alternatieve vraag: Geef de syntax, formele en informele semantiek van CTL*. Bewijs waarom AG EF p wel in CTL en niet in LTL te schrijven is. Vergelijk ook CTL, LTL en CTL*.
• (1 pts) !x!t (Fever(x) <=> Temperature(x,t) and t > 37) Deze zin is fout. Leg uit en verbeter.
• (1 pts) Bewijs: een propositionele clause is valid als en slechts als er een complementaire literal p en ~p inzit.

Open boek (oefeningen)

• (5 pts) LTC oefening over Mijnenveger
• (2 pts) Gegeven 4 CTL formules, welke hoort er niet bij. Maak een transitiestructuur.

### Maandag 14 januari 2013

Gesloten boek deel (theorie)

• (3pts) Inductiebewijs: uitleggen + op voorbeeld toepassen
• (3pts) Algoritme om CTL formule te evalueren op model uitleggen
• (1pts + 1pts) 2 kleine vraagjes (Godel incompleteness theorem + completenes theorem + waarom niet inconsistent, delta-model generatie + voorbeeld van een softwaresysteem en applicatie van delta generatie geven)

Open boek (oefeningen)

• (4pts) LTC oefening over een bowlingbaan
• (3pts) Hoare logic oefening op het Prime voorbeeld dat hieronder ergens staat.

## 2011-2012

### Maandag 16 januari 2012

• (3pts) Tseitsing uitleggen + complexiteit + toepassen op een vb
• (3pts) uitleggen hoe je invarianten kan bewijzen met inductie + toepassen op een voorbeeld.
• (1pts) P/5 predicaat met eerste 2 argumenten keys en de rest ervan afhankelijk, uitdrukken in FO
• (1pts) delta-model generation
• (3pts) oef: DPLL voor P<=> A XOR B , S <=> A AND B
• (4pts) oef: Hoare logic: Programma dat voor een input aangeeft ov het een priemgetal is
d = a-1
while ( (a mod d) != 0 ) {
d = d-1
}
if (d > 1) {
d=0
}

Show that ${\displaystyle \vdash _{tot}(a>=2)Prime(a)(d=is\_prime(a))}$.

met is_prime = 1 als het getal een priemgetal is, 0 anders.

## 2010-2011

### Maandag 31ste januari 2011

• (4pts) dpll uitleggen + clause learning + toepassen op een voorbeeldje.
• (4pts) uitleggen hoe je invarianten kan bewijzen met inductie + toepassen op een voorbeeld.(vroeg hij hard op door)
• (7pts) oefeningen: ltc-vraag en hoare logica vraag(programma dat natuurlijke getallen omkeerd)

### Donderdag 27 januari 2011

#### Theorie

• (4pts) The domain closure axiom plays an important role in this course. Explain what it is and prove that in general, it cannot be expressed in FO. What is the relation to the Peano axioms? Do you know a way to express it in other logics (an example suffices)? Where, why and how is this concept so relevant for this course? Why is it not necessary to express it in IDP?
• (3pts) Consider the following scenario:
State 0: Bob has book1, John has book2, Mary has book3
Bob gives book1 to John
John gives book1 to Mary
And the theory: <theory from example in slides>
Explain what is missing in this theory and present different representation techniques to solve this in as much detail as possible. Give the correct theory. Assume that instead of the deterministic action Give, we have a non-deterministic action Raffle(Person,Book,T) (Raffle means "verloten") with the effect that the owner gives a book away to an arbitrary person. Represent the pre-condition of this action by a state axiom and the effect of this action by a transition axiom.
• (1pts) What is the difference between the (second order) induction axiom and the induction schema?

#### Oefeningen

• (3.5pts) Formalize the alternating bit protocol in the linear time calculus. In the alternating bit protocol, a server attempts to send messages over an unreliable communication channel to a client. Here the messages are just increasing numbers 0, 1, 2, ... Internally, a server contains a bit, called the sender bit, which initially is 0. The client contains also a bit, called the expected bit, initially 0. There are two types of actions:
• The server can send and receive messages. The sent messages contain its sender bit and the current message m. The same message is resend until acknowledgement is received. If the server receives a message from the client, then this message is ignored if it does not contain the current sender bit, and otherwise, the sender bit is swapped, and the next message m+1 can be send.
• The client can also send and receive messages. It sends acknowledgement messages containing the inverse of the expected bit. If the client receives a message from the server that does not contain the expected bit, it ignores the message. Otherwise, it swaps its expected bit.
A property of the alternating bit protocol is that messages are received in the right order. Express this as an FO formula.
• (3.5pts) Consider the following program Reverse that reverses the digits of a natural number n:
m = 0
p = 0
while ( n != 0 ) {
p = p + 1
m = m * 10 + n % 10
n = n / 10
}
Show that ${\displaystyle \vdash _{tot}(n>0\land n=\sum \limits _{i=0}^{k}c_{i}*10^{i})Reverse(n)(m=\sum \limits _{i=0}^{k}c_{i}*10^{k-i})}$.
Remark: in case you find an error in the program, please correct it.

## 2009-2010

### Maandag 25 januari 2010

#### Theorie

• Geef en bewijs het compactness theorem. Geef ook aan hoe je dit kan gebruiken om bewijzen van inexpressibility uit te drukken (dus het proof skeleton geven).
• LTL model checking: Gegeven M en de transitierelatie (->alfa) van ~ (A U B) zoals in voorbeeld uit cursus.

Gevraagd:

• Hoe stel je (in het algemeen!) de transitierelatie (->alfa) op?
• Leg in je uitleg ook current en next state conditions uit.
• Pas dit toe in het voorbeeld op (q3') (dus adhv next state conditions zeggen welke states bereikbaar zijn van q3'.
• Leg op een hoog niveau uit hoe je deze modellen (M en ->alfa) gebruikt om |= aan te tonen.
• Welke zijn de additionele fairness constraints voor (->alfa) en waarom zijn deze nodig?
• Korte vragen (gecombineerd 1 blz.)
• ID: leg uit waarom we FO hebben uitgebreid met ID. Wat is het verschil tussen de definitionele implicaties en de afgeleide materiele implicaties? Verduidelijk met een voorbeeld.
• Vertel zoveel mogelijk van het SAT-probleem op 1/2 blz.

#### Oefeningen

• Je moet een NuSMV model maken voor een microgolfoven die tekstueel is beschreven. Het ging zoiets als volgt:

Een gebruiker kan 4 acties doen: open_door, close_door, start_oven en reset_oven. De oven heeft 3 inwendige componenten: door_open, heating_on en error_on. Al deze variabelen zijn booleaans.

Als de deur dicht is en de gebruiker drukt op start_oven, dan moet de oven (gedurende een WILLEKEURIGE tijd) blijven koken. Als de deur open is en er wordt op start_oven gedrukt, gaat de oven in de error_on toestand. De gebruiker moet de deur sluiten en daarna op reset_on drukken zodat error_on wordt uitgeschakeld. Als open_door wordt uitgevoerd tijdens heating_on, moet de oven onmiddelijk stoppen met cooken. ...

• Geef het transitiemodel (dus naast de code ook een getekende grafe!).
• Verifieer de volgende LTL- en CTL-specificaties:

een vijftal specificaties die je moest verifieren in de trend van: G(G(door_closed)->FG(cooking_on)) ...

• Program verification: gegeven is een programma dat 2 cijfers in base 2 voorstelling optelt (c[0..N] = a[0..N-1] + b[0..N-1]).

Het programma ging zoals volgt:

c[0..N] = 0

i = 0

while(i<n){

s = c[i+1] + a[i] + b[i]
c[i+1] = s % 2
c[i] = s / 2
i = i + 1

}

opmerking: de prof. vermelde tijdens het examen dat INDIEN er een fout in het programma zat, je deze moest verbeteren en correctheid van de VERBETERDE code moest bewijzen.

• Bewijs TOTALE correctheid van (n > 0) P (c = a+b).
• Stel dat je ook nog wil uitdrukken dat de rij a onveranderd blijft gedurende het algoritme. Hoe doe je dit?

### Vrijdag 15 januari 2010

#### Theorie

• Bewijs op een formele manier dat reachability niet kunnen uitdrukken in FO. Welke gevolgen heeft dit?
• Gegeven een aantal FO-zinnen over het voorbeeld van de boeken. Wat ontbreekt er? (inertie, UNA, DCA...)
• 3 kleine vraagjes ("combined answers should fit on one page"):
• Geef de verschillende vormen van inferentie van FO. Geef ook een toepassing.
• Wat is non-chronological backtracking in de context van het DPLL algoritme?
• Wat is het undecidability theorem van Church?

#### Oefeningen

• Een oefening over een metro. Er is een klein metro-net gegeven met 11 stopplaatsen dat er uit ziet als volgt:

Een trein start op locatie 1 en gaat naar rechts. Als hij naar rechts gaat en op locatie 7 komt kan hij kiezen of hij naar locatie 8 of 9 gaat. Als hij naar links gaat en op locatie 5 komt kan hij kiezen om naar locatie 2 of 4 te gaan. Als hij op locatie 1, 3, 9 of 11 komt zal hij omkeren (en op andere locaties niet!). Elke tijdseenheid gaat de trein ÃƒÂ©ÃƒÂ©n station verder. Het omkeren duurt ook ÃƒÂ©ÃƒÂ©n tijdseenheid.

• Druk dit model uit in LTC. Maak hiervoor gebruik van het LeftOf predicaat: LeftOf={(Locatie 1, Locatie 2), (Locatie 2, Locatie 5), ...}.
• Construeer een transitiemodel voor het metro-net (voor gebruik bij de LTL en CTL formules in de volgende vraag).
• Vertaal de volgende uitdrukkingen naar LTL of CTL en geef voor elke uitdrukking aan of hij waar is of niet.
• Hier werden er een stuk of 5 uitdrukkingen gegeven die ik niet meer weet.
• Een Hoare-logic oefening waarbij de totale correctheid van een programma dat integers omkeert bewezen moest worden:
m = 0
p = 0
while (n != 0) {
p = p + 1
m = m * 10 + n % 10
n = n / 10
}

Preconditie: n >= 0 en n = ${\displaystyle \sum _{i=0}^{k}c_{i}10^{i}}$

Postconditie: m = ${\displaystyle \sum _{i=0}^{k}c_{i}10^{k-i}}$

## 2008 - 2009

### Vrijdag 23 januari 2009

#### Theorie

• Bewijs dat we geen inductieve predicaten kunnen uitdrukken in FOL.
• Geef het algoritme voor CTL model checking en bespreek de complexiteit
• 3 kleine vraagjes ("combined answers should fit on one page")
• Neem een predicaat P/5. Hoe kan je uitdrukken in FO dat de eerste twee argumenten een primary key vormen? (Een mogelijke oplossing: !x,y,z,u,w,r,s,t ( (P(x, y, z, u, w) ^ P(x, y, r, s, t) => z = r ^ u = s ^ w = t))
• Hoe kan IDP gebruikt worden om interessante testcases te genereren bij een programma?
• Bij modale logica, wat betekenen logical omniscience en total introspection? Geef de formules.

#### Oefeningen

• modelleer volgend systeem in AL: iets van een automatische garagepoort met 5 posities (1..5) waarin 1 gesloten is en 5 open, een toestand "opening_door" en "closing_door" en meerdere afstandsbedieningen die het open of close commando kunnen geven (waarbij open voorrang heeft op close als ze tegelijk ingedrukt worden). Hierbij de vraag om enkele axiomas van de guided simulation in LTC uit te drukken ("op tijdstip 10 wordt de poort gesloten"), en de vraag hoe je invarianten van dit systeem zou bewijzen (zwakke + sterke manier).
• Gegeven volgende code P:
d = a - 1
while( (a mod d) != 0 ) {
d = d - 1
}
if(d > 1){
d = 0
}

Bewijs dat ${\displaystyle \vdash _{tot}(a\geq 2)P(d=is\_prime(a))}$, waarbij is_prime(a) 1 is als a priem is en 0 anders.

### Examen 19 januari 2009

• Stukje idp code van de boeken: wat ontbreekt hier? (inertie, una, dca ...)
• Tekening van automaat voor model, en een automaat voor AUB: Hoe komt dit tot stand (algemeen, niet op voorbeeld)
• Enkele kleine vraagjes:
• Wat is het verschil tussen comman, general en distributed knowledge?
• Leg de twee kampen theorie uit. Wat heeft dit van belang voor Multi agent systems en protocollen?
• Compactness theorie en complicaties voor de limieten van de FO-logic
• oefeningen:
• DPLL algoritme op een paar statements toepassen met enkele kleine vraagjes
• De windows music player zune liep op 31/12/2008 vast. De batterij laten leeglopen en de volgende dag pas weer opladen bleek de enigste oplossing. Code werd gegeven ivm data berekenen in de Zune. Bewijs partiele correctheid. Bewijs volledige correchtheid. Wat liep er mis?

## 2007 - 2008

### Examen 18 januari 2008

#### Theorie-gedeelte

• Prove that in First Order logic, we cannot express finiteness of the domain of discourse. (i.e., there is no FO theory with only models with a finite domain.)
• Explain a CTL model checking algorithm and discuss its complexity
• Small questions: the combined answers should fit on one page.
• Explain what is the semi-decidability of FO.
• Explain what is the frame problem.
• As we saw, reachability (transitive closure) cannot be expressed in FO, and Alloy is an alternative syntax for FO. And yet, Alloy contains a transitive closure operator. How is this possible? Solve the paradox.

#### Oefening 1

Evaluate the truth of the following formula

${\displaystyle \forall x\forall y(R(x,y)\leftrightarrow G(x,y)\vee \exists z(R(x,z)\wedge R(y,z)))}$

in the following pair of graphs G and R with domain {a, b, c}:

• ${\displaystyle G:={(b,c),(c,b)}}$
• ${\displaystyle R:={(a,b),(a,c),(b,c),(c,b),(b,b),(c,c)}}$

It does not suffice to say true or false. You have to explain why. What is the transitive closure of G?

#### Oefening 2

Translate the following sentence in ALLOY-syntax in at least two ways: ${\displaystyle \forall x\forall y(GrandParent(x,y)\supset \exists zParent(x,z)\wedge Paren(x,y))}$

Vice versa, translate the following ALLOY-statement in first order logic syntax:

all P : PDS | {
all c : P.components, s : Service |
let c' = s.(c.(P.schedule)) {
(some c' iff s in c.import) && (some c' => s in c'.export) } }

#### Oefening 3

Formalize the alternating bit protocol in the linear time calculus. In the alternating bit protocol, a serer attempts to send messages over an unreliable communication channel to a client. Here the messages are just increasing numbers 0, 1, 2... Internally, a server contains a bit, called the sender bit, which initially is 0. The client contains also a bit, called the expected bit, initially 0. There are two types of actions:

• The server can send and receive messages. The sent messages contain its sender bit and the current message m. The same message is resent until acknowledgement is received. If the server receives a mesage from the client, then this message is ignored if it does not contain the current sender bit, and otherwise, the sender bit is swapped, and the next message m + 1 can be sent.
• The client can also send and receive messages. It sends acknowledgement messages containting the inverse of the expected bit. If the client receives a message from the server that does not contain the expected bit, it ignores the message. Otherwise, it swaps its expected bit.

A property of the alternating bit protocol is that messages are received in the right order. Express this as a FO formula.