[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
	types of verification
		Proof vs Model
		How automated?
		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