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