>> [CS656/556 Course Materials]
Mon Mar 3 14:43:02 PST 2003
656/556 2003 1w 12 models CTL
Admin: CSCI656 students need to hand in a progress report.
Assigned work due: Reading on Finite state machines/automata.
Plus chapter 3.1&3.2
types of verification
Proof vs Model
Full vs Partial properties
For what domain?
When to do it?
Idea of Model Based Verification
model of system, state of system |= specified properties
Abstracting from software to mathematical model.
States and transitions
Compare Finite Automata.
Specifying desirable properties
Can, will, should, might, must, possibly, never, ...
Whenever X happens, then Y will sometime be true.
(Ambiguous in English)
Rules for handling '|='.
in practice, use tools - SPIN, SMV
The hardest part is specifying properties precisely.
CTL ::= `Computational Tree Logic`.
Syntax of CTL
Propositions + 8 modalities decribine future properties.
p = `it is raining`
AX p = `Tomorrow it will rain`.
EX p = `Tomorrow it may rain`.
AF p = `Some day it will rain`.
EF p = `Some day it may rain`.
AG p = `From now on it will always rain`.
EG p = `Someday it will start to rain forever`
A[ p U q ] = `q will be true aand before that p is true`.
E[ p U q ] = `q may be true aand before that p is true`.
Combine these 8 with negation and we get 16 new ways to
create logical statements
Note. If you want a visual aid bookmark pages 160..161, figures 3.5..3.8
Exercises on Syntax Ex3.1 1a 1b 1c
Note: If you would like to see an alternative approach to modal logics
This pages includes a short introduction to CTL:
Assigned Work: Exercises 3.1, #1d, 1e, and 1f.
lab: Final lab on Prolog includes a simulator of a finite state system
next: ch3.3 Semantics & 3.4 Example