DOC PREVIEW
CMU CS 15414 - Puzzles with SMV

This preview shows page 1-2-3-4-25-26-27-51-52-53-54 out of 54 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 54 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 54 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 54 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 54 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 54 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 54 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 54 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 54 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 54 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 54 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 54 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 54 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

Puzzles with SMVBug Catching in 2006 FallNov. 09, 2006Gi-Hwon Kwon22Agenda• Puzzles as Model Checking Problem Missionary cannibal problem Bridge crossing problem Maze game Push-Push game Sokomind-PLUS game Sokomind Game• Challenge works Puzzle as Bounded Model Checking Problem Puzzle as Directed Model Checking Problem33Puzzle Worldssolvable in several timestemporal propertiessolvable in one timeno temporal properties44Missionary Cannibal Problem2255Missionary Cannibal Problem• State is 3-tuple (M,C,B) M = {0,1,2} on the right side C = {0,1,2} on the right side B = {L,R} initial state: (2,2,R)  final state: (0,0,L) unsafe state: (m,c,?), where m < c• Transitions (0,1) : 1 cannibal on board (0,2) : 2 cannibals on board (1,0) : 1 missionary on board (1,1) : 1 missionary and 1 cannibal on board (2,0) : 2 missionaries(2,2,R)(0,0,L)66Missionary Cannibal ProblemEF (0,0,L)¬EF (0,0,L)77Missionary Cannibal Problem88Quiz #199Solution1010Crossing Bridge Problem1111Quiz #2¬EF (time<=30 & all family on the left side& lamp also on the left side)1212Solution1313Maze Gamesattackerexityoudelay1414Maze Games¬E[ ¬unsafe U exit]15151616Quiz #3¬E[ ¬unsafe U exit]1717Solution1818Maze Games15 levels1919Maze Games2020Model Checking Results151413121110987654321Level14x914x98x88x88x86x66x66x66x66x66x66x66x66x66x6Size18423718163202.06943979952881.57728344033080.44797431131560.47667633431880.46273356823920.20523818224840.22634266725640.22433745024680.18493127723480.20252840123000.13373389424200.18482810723120.17443356323840.18593592224400.16StepsBDDMemory(KB)Time(sec)2121So FarAre you happy ?☺When model checking people sad ? 2222Push Push GamesTwo questionsIs there a feasible path to a goal state ?Which one is optimal ?agentgoal positionboxgoal state2323Push Push Games¬EF (goal state)2424Quiz #4¬EF (13 & 23 & 33 & 43 & 53 & 63)2525Solution2626Push Push Games50 levels2727Model Checking Results2828Naïve Model Checking Results37 levels are solved13 levels are failedmodel checkers’capabilitysize of the gameHow to avoid the state explosion ?no state explosion state explosion occurs☺ 2929State Explosion AvoidanceDefensive approachOffensive approach• Abstraction • Symmetry reduction• Partial order reduction……• Efficient data structures• Distributed and parallelized• Buy an expensive computer……3030Abstractionreduced model M’deadlockposition• Removing irrelevant parts w.r.t. properties to be verified• Reduced model M’ still preserves properties of interestsoriginal model MWhich parts abstracted away ?Reduction of the original model into a smaller one3131Abstraction××××witness w.r.t. 'MM≡witness|witness|=⇒=MM'M××××M’3232Abstraction Results3333Abstraction Results49 levels are solvedLast level is failedA reduced model is still too largeWhat have to do when abstraction is failed ?no state explosionstate explosion occurs☺ 3434Relay Model Checkingg1∧g2∧g3Conventional model checkingDivide and conquerg1∧g2∧g3g1∧g2g13535Relay Model Checking¬EF (73 & 74 & 75)3636Relay Model Checking3737Relay Model Checking3838Relay Model Checking3939ResultsGood newsHow to get the optimal solution ?338 steps is not optimal338Bad newsinit338 steps4040ObservationsLinear ordering of subgoals#1. Conservative, not complete • Not always working.• But if it works, then the path is a witness in an original model.#2. Goal ordering is important #3. No guarantees an optimal solution• Optimization is needed #4. Sometimes, we get lost on the way to a goal• Guiduance is needed4141Modified Model CheckerCurrent NuSMV• 3 times traversals• BDD storage on RAMModified NuSMV• 2 times traversals• BDD storage on HD4242Modified Model Checker322Eventually we get an optimal path !!322 steps4343SokoMind-PLUS Game4444Quiz #4¬EF (ball1=goal1 & ball2=goal2 & ball3=goal3)4545Solution4646Sokomind-PLUS Game20 levels4747Model Checking ResultsBut 16th~ 20thlevels are failed !!4848SokoMind Games60 levels4949Model Checking Resultssolved58582010failed307629solved187187398solved229229517solved165165496failed313545solved229229474solved7070243solved8181252solved146146371RemarkWorld recordsNumber of stepsNumber of positionsLevelfailed…………60failed…………59failedfailedfailedfailedfailed3696614failed4337113failed3657712failed4567111RemarkWorld recordsNumber of stepsNumber of positionsLevel5050Puzzles as Model Checking ProblempuzzlesolvingconditionMtruebad designedno solutions existgoal¬AGEncoderSMVDecodermodelcounter-exampleformulaφ) φ¬,(MMCfalse +πoptimal solutionwell designedmodel checker5151However?How to bridge the gap ?Model CheckerPuzzle Size5252Challeange WorksPuzzles as Bounded Model Checking ProblemEncoderSimplifierSAT SolverDecoderCNF CNFSAT?yessolutionk < kmax?k := k+1yesnonok := kinitpuzzlesymbol tablemodel☺ bound5353Challeange WorksPuzzles as Directed Model Checking Problemgoalgoalstart startTraditional Model CheckingDirected Model Checkingexplicit MC+guided search5454Challeange WorksPuzzles are waiting for Your Breakthrough Technique !!Thank


View Full Document
Download Puzzles with SMV
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Puzzles with SMV and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Puzzles with SMV 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?