search
Differences
This shows you the differences between two versions of the page.
|
cs-686:quizzes-and-exams [2014/09/02 11:01] egm created |
cs-686:quizzes-and-exams [2014/09/02 11:01] (current) egm |
||
|---|---|---|---|
| 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: | + | List topics... |
| - | + | ||
| - | * Create minimum labeled traces such that they satisfy a given temporal logic formula | + | |
| - | * Create BDDs from code showing the unique and compute tables as a final answer (IDs must follow the order of creation from ITE) | + | |
| - | * Create a Boolean expression for a transition relation from a simple program like the dining philosophers in the homework | + | |
| - | * Write a Boolean function describing the initial state of a problem and perform reachability analysis using that function and a transition relation | + | |
| - | * Perform CTL model checking using Boolean functions and fix-point computations | + | |
| - | + | ||
| - | I expect the test to take 2 hours of student time. | + | |
| - | + | ||
| - | == Midterm Review == | + | |
| - | + | ||
| - | One page of notes is allowed for the exam. You are responsible for knowing the testing center hours: double check the schedule for Saturday! Below is a comprehensive list of topics on the exam. Please note that some of the topics were not covered directly by the homework, so you will want to perhaps work a few problems on your own to prepare. | + | |
| - | + | ||
| - | * Describe the LTL syntax, CTL syntax, and the different in semantics between LTL and CTL | + | |
| - | * Write English descriptions as properties in CTL, LTL, or CTL*. Negate temporal logic formulas. | + | |
| - | * Create minimum labeled traces such that they satisfy a given temporal logic formula. | + | |
| - | * Convert a Kripke structure to a Buechi automaton. | + | |
| - | * Express the language accepted by a Buechi automaton as a regular expression augmented with the omega operator. | + | |
| - | * Compute the intersection of two Buechi automaton. | + | |
| - | * Perform double-depth-first-search on a Buechi automaton. | + | |
| - | * Implement fairness in on-the-fly model checking. | + | |
| - | * Perform explicit state model checking given a Kripke and CTL property. | + | |
| - | + | ||
| - | I expect the test to take at least 1 hour of student time. The total time limit on the test is 2 hours. | + | |
