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
This pages includes a short introduction to CTL:
	http://www.csci.csusb.edu/dick/maths/logic_9_Modalities.html#Computational%20Tree%20logic


Assigned Work: Exercises 3.1, #1d, 1e, and 1f.

lab: Final lab on Prolog includes a simulator of a finite state system
	http://www.csci.csusb.edu/dick/cs656/prolog/lab4.html

next: ch3.3 Semantics & 3.4 Example
	http://www.csci.csusb.edu/dick/cs656/class/13.html