evaluate a formula in a structure
examples:
check for the existence of a trace satisfying the formula
proceed bottom up on the subformulae
idea: proceed in reverse order: from subformulae to formula
first step: identify all subformulae
example: (a∨¬b) U ( F(¬a∧¬b) ∧ X(¬a∧b) )
extract all subformulae
omit literals
consider all subformulae of points 1-4
disregard duplicates
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
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
proceed from the simplest subformulae to the more complex
in this case:
begin with the first one, for example
¬a∧¬b true implies F(¬a∧¬b) true
not enough
F(¬a∧¬b) true in the second node
reachable from the first node
therefore, F(¬a∧¬b) true in the first node
others...
F(¬a∧¬b) true if a node where F(¬a∧¬b) is true is reachable
¬a∧b true in the third node
X(¬a∧b) true in the second node
generally: true if subformula true in a direct successor
if two formulae are true in the same node
their conjunction is so as well
note...
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" is true if its second subformula is true
"until" is true if:
original formula is in the first state
formula is true in a trace of the structure
⇒ |
A and B both true in a node ⇒ A∧B true in the node
same for ∨ and ¬
⇒ |
A true in a successor ⇒ XA true in the node
(or: A true ⇒ XA true in all predecessors)
⇒ |
base case: A true implies FA true
⇒ |
FA in a successor ⇒ FA true
⇒ |
all nodes initially marked GA
base case: remove GA from nodes not marked A
⇒ |
all successors have GA removed ⇒ remove GA
why "all"?
existential model checking
⇓
if GA is true in a successor, cannot be removed
⇒ |
B true ⇒ AUB true
⇒ |
A true and AUB true in a successor ⇒ AUB true
check formula F(a∧XXb) on:
first: subformulae
b in a successor ⇒ Xb in the state
Xb in a successor ⇒ XXb in the state
a true and XXb true ⇒ a∧XXb true in the same state
a∧XXb true ⇒ F(a∧XXb) true in the same state
(base case of recursion for F)
F(a∧XXb) true in a successor ⇒ F(a∧XXb) true
(recursive step for F)
final state of labels
F(a∧XXb) in initial state ⇒ formula true in the structure
check G(Xa∨(aU¬b)) on the following structure:
first step: subformulae
label, starting from bottom line
a in a successor ⇒ Xa
¬c in a state ⇒ bU¬c same state
b in a state, bU¬c in a successor
⇓
bU¬c in the state
Xa ⇒ Xa∨(bU¬c) (same state)
bU¬c ⇒ Xa∨(bU¬c) (same state)
mark all nodes with G(Xa∨(bU¬c))
erase G(Xa∨(bU¬c)) from all nodes not containing Xa∨(bU¬c)
remove G(Xa∨(bU¬c)) if the same formula is erased in all successors
final state of labels
initial state labeled G(Xa∨(bU¬c)) ⇒ formula true in the structure