Model checking

evaluate a formula in a structure

examples:

the system will never be off for more than two consecutive time points:
G(¬off ∨ ¬Xoff ∨ XX¬off)
a request is at some point served:
G(¬request ∨ Fserved)
at startup, display some logo until the OS is on
logo U os_on
(no G here: formula required to hold only at the beginning)

Labeling algorithm

check for the existence of a trace satisfying the formula

proceed bottom up on the subformulae


Labeling algorithm: principle

idea: proceed in reverse order: from subformulae to formula


Labeling algorithm: subformulae

first step: identify all subformulae

example: (a∨¬b) U ( F(¬a∧¬b) ∧ X(¬a∧b) )

extract all subformulae

omit literals


Subformulae

  1. (a∨¬b) U ( F(¬a∧¬b) ∧ X(¬a∧b) )
  2. a∨¬b, F(¬a∧¬b) ∧ X(¬a∧b)
  3. F(¬a∧¬b), X(¬a∧b)
  4. ¬a∧¬b, ¬a∧b

consider all subformulae of points 1-4

disregard duplicates


Labeling algorithm: structure

checks whether the structure contains a trace satisfying the formula

works by marking the nodes of the structure with the subformulae

structure:

subformulae: (a∨¬b) U ( F(¬a∧¬b) ∧ X(¬a∧b) ), a∨¬b, ( F(¬a∧¬b) ∧ X(¬a∧b) ), F(¬a∧¬b), X(¬a∧b), ¬a∧¬b, ¬a∧b


Propositional formulae

the interpretations tells the value of the non-modal subformulae

in this case: a∨¬b, ¬a∧¬b and ¬a∧b

label nodes with formulae true there


Modal operators

proceed from the simplest subformulae to the more complex

in this case:

begin with the first one, for example


Finally, now

¬a∧¬b true implies F(¬a∧¬b) true

not enough


Finally, recursively

F(¬a∧¬b) true in the second node

reachable from the first node

therefore, F(¬a∧¬b) true in the first node

others...


Finally, all

F(¬a∧¬b) true if a node where F(¬a∧¬b) is true is reachable


Next

¬a∧b true in the third node

X(¬a∧b) true in the second node

generally: true if subformula true in a direct successor


Conjunction

if two formulae are true in the same node
their conjunction is so as well

note...


Subformulae, not all formulae

how about (¬a∧¬b)∧X(¬a∧b) in the second node?

true, but not a subformula of the original formula

not useful   ⇒   do not add label


Until now

"until" is true if its second subformula is true


Until, recursively

"until" is true if:


Final result

original formula is in the first state

formula is true in a trace of the structure


The labeling algorithm

  1. find all subformulae
  2. label nodes with the simplest subformulae true there
  3. proceed bottom up to the original formula

Labeling rules: propositional

A and B both true in a node   ⇒   A∧B true in the node

same for and ¬


Labeling rules: next

A true in a successor   ⇒   XA true in the node

(or: A true ⇒ XA true in all predecessors)


Labeling rules: finally (base)

base case: A true implies FA true


Labeling rules: finally (recursive)

FA in a successor   ⇒   FA true


Labeling rules: globally (base)

all nodes initially marked GA

base case: remove GA from nodes not marked A


Labeling rules: globally (recursive)

all successors have GA removed ⇒ remove GA

why "all"?

existential model checking

if GA is true in a successor, cannot be removed


Labeling rules: until (base)

B true   ⇒   AUB true


Labeling rules: until (recursive)

A true and AUB true in a successor   ⇒   AUB true


First example

check formula F(a∧XXb) on:


First example (1)

first: subformulae


First example (2)

b in a successor ⇒ Xb in the state


First example (3)

Xb in a successor ⇒ XXb in the state


First example (4)

a true and XXb true ⇒ a∧XXb true in the same state


First example (5)

a∧XXb true ⇒ F(a∧XXb) true in the same state

(base case of recursion for F)


First example (6)

F(a∧XXb) true in a successor ⇒ F(a∧XXb) true

(recursive step for F)


First example (7)

final state of labels

F(a∧XXb) in initial state ⇒ formula true in the structure


Second example

check G(Xa∨(aU¬b)) on the following structure:


Second example (1)

first step: subformulae

label, starting from bottom line


Second example (2)

a in a successor   ⇒   Xa


Second example (3)

¬c in a state   ⇒   bU¬c same state


Second example (4)

b in a state, bU¬c in a successor

bU¬c in the state


Second example (5)

Xa   ⇒   Xa∨(bU¬c) (same state)

bU¬c   ⇒   Xa∨(bU¬c) (same state)


Second example (6)

mark all nodes with G(Xa∨(bU¬c))


Second example (7)

erase G(Xa∨(bU¬c)) from all nodes not containing Xa∨(bU¬c)


Second example (8)

remove G(Xa∨(bU¬c)) if the same formula is erased in all successors


Second example (9)

final state of labels

initial state labeled G(Xa∨(bU¬c)) ⇒ formula true in the structure