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

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.