656/556 2003 1w 13 CTL
Assigned work Due: Exercises 3.1, #1d, 1e, and 1f.

From the text Book:
	3.3 semantics
		System:  States(s0,s1,...), properties(p,q,...), transitions.
			FSA/FSM with input ignored!
			Non-deterministic!  One state can lead to many.
		Unwinding: System-> Tree of possible future
		Patterns on trees: EX, AX, EF, EG, AF, AG.
			 http://www.csci.csusb.edu/dick/cs656/CTL.gif
			 http://www.csci.csusb.edu/dick/cs656/CTL.pdf
		Satisfaction:  Model,state|=property.
			Notice: a property can hold in many states in one model.

		Patterns in real specifications.
		 More in:
		   http://www.cis.ksu.edu/santos/spec-patterns/ctl.html

		Equivalences:
		  not EG = AF not, ...
		  AF p = A[ T U p ], ...
		  AG p = p and AX AG p, ...
		  Full List in
     http://www.csci.csusb.edu/dick/maths/logic_9_Modalities.html#Equivalences			
   Added to Chapter 3
	A sample problem from the past...(handout)

		
	3.4 example:  Mutual Exclusion
	    A classic problem -- solved once but still tripping up programmers.
	    Properties
		Safety and Liveness properties.
		Non-blocking
		No strict sequencing
	    First model
	    Second Model

   Exercises 3.2 (p163-165), 3.3(p165-166) and 3.4(p168-169).

Assigned work:Exercises 3.2 (p163-164) #1b (v)(vi)(vii)(viii)

Next:  making model checking easier.

lab: Explore modal logics on the WWW and introduction to SMV
http://auto.search.msn.com/results.asp?FORM=AS14&v=1&RS=CHECKED&srch=4&q=Modal+logic

Survey in ACM Digital Library
http://www.acm.org/pubs/citations/journals/surveys/2000-32-1/p12-bellini

SMV
http://groups.google.com/groups?hl=en&q=CTL+SMV
http://ftp.csci.csusb.edu/dick/cs556/smv/doc/smv.txt
http://ftp.csci.csusb.edu/dick/cs556/smv/doc/


next!
Chapters 3, Sections 3.5, 3.6,3.10 SMV
http://www.csci.csusb.edu/dick/cs656/class/14.html