[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 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