[CSUSB] >> [CompSci] >> [Dick Botting] >> [CS656/556 Course Materials] >> class/13
[Index] || [Contents] || [Grades] Mon Mar 3 14:43:02 PST 2003
```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
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