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

Both sides previous revision Previous revision Next revision | Previous revision | ||

cs-486:exams [2017/04/19 13:11] egm [Final Review] |
cs-486:exams [2018/12/13 10:50] (current) egm [Final Review] |
||
---|---|---|---|

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