Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
cs-486:exams [2017/02/28 17:39]
egm [Midterm Review]
cs-486:exams [2018/12/13 10:50] (current)
egm [Final Review]
Line 1: Line 1:
 == Final Review == == Final Review ==
-The final is in the testing center and is '''​closed book and closed ​notes'''​. It consists ​of one multiple-guess problem and 5 essay 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:
  
-* Create ​minimum labeled traces such that they satisfy ​a given temporal logic formula +* Create ​Kripke structures ​that satisfy temporal logic formulas ([[Homework 7]]) 
-Create ​BDDs from code showing ​the unique and compute tables as a final answer (IDs must follow ​the order of creation from ITE) +Write temporal logic formulas for specification expressed in english--be sure you know both CTL and LTL sub-logics ([[Homework 7]]) 
-* Create a Boolean expression for a transition relation from a simple program ​like the dining philosophers in the homework +* Prove (or disprove) if two temporal logic formulas are equivalent ([[Homework 8]]).  
-* Write a Boolean function describing the initial state of a problem ​and perform ​reachability ​analysis using that function and a transition relation +* Given a Kripke structure and a set of CTL formulas, determine which states are labeled with which formulas ([[Homework 10]]).  
-* Perform CTL model checking using Boolean functions and fix-point computations+* 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]]). 
 +* Create a Boolean expression for a transition relation from a simple ​PROMELA ​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).  ​ 
 +* 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). ​
  
 I expect the test to take 2 hours of student time. I expect the test to take 2 hours of student time.
- 
 == Midterm Review == == Midterm Review ==
  
cs-486/exams.1488328767.txt.gz · Last modified: 2017/02/28 17:39 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0