##### Differences

This shows you the differences between two versions of the page.

 cs-486:exams [2017/04/19 13:11]egm [Final Review] cs-486:exams [2018/12/13 10:50] (current)egm [Final Review] Both sides previous revision Previous revision 2018/12/13 10:50 egm [Final Review] 2018/12/13 10:50 egm [Final Review] 2017/12/14 14:04 egm [Final Review] 2017/04/20 15:57 egm [Final Review] 2017/04/19 13:11 egm [Final Review] 2017/04/19 13:05 egm 2017/04/19 12:38 egm [Final Review] 2017/02/28 17:39 egm [Midterm Review] 2014/09/02 10:44 egm created Next revision Previous revision 2018/12/13 10:50 egm [Final Review] 2018/12/13 10:50 egm [Final Review] 2017/12/14 14:04 egm [Final Review] 2017/04/20 15:57 egm [Final Review] 2017/04/19 13:11 egm [Final Review] 2017/04/19 13:05 egm 2017/04/19 12:38 egm [Final Review] 2017/02/28 17:39 egm [Midterm Review] 2014/09/02 10:44 egm created Line 1: Line 1: == Final Review == == Final Review == - The final is on Saturday, April 22nd, from 14:30 -- 17:30 in TMCB 120. One page of notes allowed (any size and any font). It consists short answer problems. Here is a comprehensive list of topics: + The final is on Monday, December 17th, from 11:00 -- 14:00 in TMCB 134. One page of notes allowed (any size and any font). It consists short answer problems. Here is a comprehensive list of topics: - * Given a temporal logic formula, identify if it is LTL, CTL, or CTL* only. * Create Kripke structures that satisfy temporal logic formulas ([[Homework 7]]) * Create Kripke structures that satisfy temporal logic formulas ([[Homework 7]]) * Write temporal logic formulas for specification expressed in english--be sure you know both CTL and LTL sub-logics ([[Homework 7]]) * Write temporal logic formulas for specification expressed in english--be sure you know both CTL and LTL sub-logics ([[Homework 7]]) * Prove (or disprove) if two temporal logic formulas are equivalent ([[Homework 8]]). * Prove (or disprove) if two temporal logic formulas are equivalent ([[Homework 8]]). - * Write LTL properties given a Promela model and specification using ''​remoterefs''​ ([[Homework 9]]). - * Convert arbitrary CTL formulas to formulas that only have '''​EG''',​ '''​EU''',​ and '''​EX'''​ for operators other than normal Boolean operators ([[Homework 10]]). ​ * Given a Kripke structure and a set of CTL formulas, determine which states are labeled with which formulas ([[Homework 10]]). ​ * Given a Kripke structure and a set of CTL formulas, determine which states are labeled with which formulas ([[Homework 10]]). ​ * Play computer and show how BDDs are created and managed with the '''​ITE'''​ method given a program using the Cudd interface. Be sure to show the unique table ''​and''​ the recursive trees tracking the '''​ITE'''​ calls ([[Homework 11]] and [[Homework 12]]). * Play computer and show how BDDs are created and managed with the '''​ITE'''​ method given a program using the Cudd interface. Be sure to show the unique table ''​and''​ the recursive trees tracking the '''​ITE'''​ calls ([[Homework 11]] and [[Homework 12]]). - * Perform SwapVariables on a given BDD (unique table included) to replace certain variables ([[Homework 11]]). + * Create a Boolean expression for a transition relation from a simple ​PROMELA ​program ([[Homework 13]]) - * Create a Boolean expression for a transition relation from a simple program ([[Homework 13]]) + * Write a Boolean function describing the initial state of a system and perform forward ​reachable ​analysis using that function and a given transition relation ([[Homework 13]] but doing it abstractly similar to class rather than with BDDs). ​ - * Write a Boolean function describing the initial state of a system and perform forward ​reachability ​analysis using that function and a given transition relation ([[Homework 13]] but doing it abstractly similar to class rather than BDDs). ​ + * Perform CTL model checking using Boolean functions and fix-point computations ​on a given Kripke structure. Show each iteration of the fix-point calculations ​(abstractly similar to class rather than with BDDs). ​ - * Perform CTL model checking using Boolean functions and fix-point computations (abstractly similar to class rather than with BDDs). ​ + I expect the test to take 2 hours of student time. I expect the test to take 2 hours of student time.