[CSUSB] >> [CompSci] >> [Dick Botting] >> [CS656/556 Course Materials] >> class/12
[Index] || [Contents] || [Grades] 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

Chapter 3
Section3.1
types of verification
Proof vs Model
How automated?
Full vs Partial properties
For what domain?
When to do it?
Idea of Model Based Verification
http://www-2.cs.cmu.edu/~modelcheck/onr/cip.htm
model of system, state of system |= specified properties
Abstracting from software to mathematical model.
States and transitions
Compare Finite Automata.
Specifying desirable properties
`modalities`:
Can, will, should, might, must, possibly, never, ...
Example:
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.

Section3.2
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
see
http://www.csci.csusb.edu/dick/maths/logic_9_Modalities.html