Modelleren van Complexe Systemen

Ga naar: navigatie, zoeken

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

in the following pair of graphs G and R with domain {a, b, 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:

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.