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

Link to this comparison view

cs-486:homework-7-2016 [2017/01/11 19:12] (current)
egm created
Line 1: Line 1:
 +This homework is to practice using BDDs for symbolic model checking.
 +==Paper Pencil==
 +# ('''​3 points'''​) Write a CTL property for the transition relation for the dinning philosophers system in [[Homework 3]]--the property must require a least or greatest fix-point to compute.
 +# ('''​5 points'''​) At an abstract level, similar to what we did on the board in lecture, perform symbolic model checking for the formula in the prior problem. Be sure to show each step of the fix-pont computation. Please note that if the '''​when'''​ clause is correctly treated as a single atomic action (i.e., the test, state update, and goto are one step), then there are only 10 reachable states.
 +Use the CUDD package for the following problems.
 +# ('''​10 points'''​) Write a program in CUDD using your solution from [[Homework 6]] that does symbolic model checking for your formula in the prior problem.
cs-486/homework-7-2016.txt ยท Last modified: 2017/01/11 19:12 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