Modelleren van Complexe Systemen

Over het examen

• Duur van het examen: 4 uur
• Het examen bestaat uit 3 delen:
  • Gesloten boek over de theorie. Mondeling met schriftelijke voorbereiding. (8pt)
  • Open boek oefeningen (7pt)
  • Project (met evt. vragen bij de mondelinge verdediging) (5pt)

Examens

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")
  • ?
  • 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 ${⊢}_{tot}(a\ge 2)P(d=is\mathrm{\_}prime(a))$, waarbij is_prime(a) 1 is als a priem is en 0 anders.

Examen 19 januari 2009

• Stukje code van de boeken: wat ontbreekt hier?
• 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?

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.

Oefeningen gedeelte

Oefening 1

Evaluate the truth of the following formula

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

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

• $G:=(b,c),(c,b)$
• $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: $\mathrm{\forall }x\mathrm{\forall }y(GrandParent(x,y)\supset \mathrm{\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.