Model Checking with thePartial Order ReductionEdmund M. Clarke, Jr.Computer Science DepartmentCarnegie Mellon UniversityPittsburgh, PA 152131Asynchronous ComputationThe interleaving model for asynchronous systems allowsconcurrent events to be orderedarbitrarily.To avoid discriminating against any particular ordering, theevents are interleaved in all possible ways.The ordering between independent transitions is largelymeaningless!!2The State Explosion ProblemAllowing all possible orderings is a potential cause of the stateexplosion problem.To see this, considerntransitions that can be executedconcurrently.In this case, there aren!different orderings and2ndifferent states(one for each subset of the transitions).If the specification does not distinguish between these sequences,it is beneficial to consider onlyone withn+ 1states.2321??12112333RR R??R3Partial Order ReductionThe partial order reduction is aimed at reducing the size of thestate space that needs to be searched.It exploits thecommutativity of concurrently executedtransitions, which result in the same state.Thus, this reduction technique is best suited forasynchronoussystems.(Insynchronous systems, concurrent transitions are executedsimultaneously rather than being interleaved.)s2s1rsR  R4Partial Order Reduction (Cont.)The method consists of constructing a reduced state graph.Thefull state graph, which may be too big to fit in memory, isnever constructed.Thebehaviors of the reduced graph are a subset of the behaviorsof the full state graph.The justification of the reduction method shows that thebehaviors that are not present do not add any information.5Partial Order Reduction (Cont.)The name partial order reduction comes from early versions ofthe algorithms that were based on the partial order model ofprogram execution.However, the method can be described better as model checkingusing representatives, since the verification is performed usingrepresentatives from the equivalence classes of behaviors.D. Peled. All from one, one for all: on model checking usingrepresentatives. In Proc. 5th Workshop on Comput.-AidedVerification, pages 409–423, 1993.6Modified Kripke StructuresThe transitions of a system play a significant role in the partialorder reduction.The partial order reduction is based on thedependency relationthat exists between the transitions of a system.Thus, we modify the definition of a Kripke structure slightly.A state transition system is a quadruple(S; T ; S0; L)wherethe set of statesS, the set of initial statesS0, and the labelingfunctionLare defined as for Kripke structures, andTis a set of transitions such that for each2T,SS.A Kripke structureM= (S; R; S0; L)may be obtained bydefiningRso thatR(s; s0), 92T[(s; s0) ]:7Basic DefinitionsA transition2Tis enabled in a statesif there is a states0suchthat(s; s0)holds.Otherwise,is disabled ins. The set of transitions enabled insisenabl ed(s).A transitionis deterministic if for every statesthere is at mostone states0such that(s; s0).Whenis deterministic we often writes0=(s)instead of(s; s0).Note:We will only consider deterministic transitions!8Basic Definitions (Cont.)A pathfrom a states0is a finite or infinite sequence=s00!s11!: : :such that for everyi,i(si; si+1)holds.Here, we do not require paths to be infinite. Moreover, any prefixof a path is also a path.Ifis finite, then the length ofis the number of transitions inand will be denoted byjj9Reduced State GraphGoal is to reduce the number of states considered in modelchecking, while preserving the correctness of the property.Will assume that areduced state graph is first generatedexplicitly usingdepth-first search.The model checking algorithm is then applied to the resultingstate graph, which hasfewer states and edges.Thisspeeds up the construction of the graph and uses lessmemory, thus resulting in a more efficient model checkingalgorithm.Actually, the reduction can be applied on-the-fly while doingthe model checking.The DFS can also be replaced by breadth first search andcombined withsymbolic model checking.10Depth-First-Search Algorithm1hash(s0);2 seton stack(s0);3expand state(s0);4 procedureexpand state(s)5w or k set(s) :=ampl e(s);6 whilew or k set(s)is not empty do7 let2w or k set(s);8w or k set(s) :=w or k set(s)n fg;9s0:=(s);10 ifnew(s0)then11hash(s0);12 seton stack(s0);13expand state(s0);14 end if;15cr eate edg e(s; ; s0);16 end while;17 setcompl eted(s);18 end procedure11Depth-First-Search Algorithm (Cont.)The reduction is performed by modifying the standard DFSalgorithmto construct the reduced state graph.The search starts with an initial states0(line 1) and proceedsrecursively.For each statesit selects only a subsetampl e(s)of the enabledtransitionsenabl ed(s)(in line 5).The DFS explores only successors generated by these transitions(lines 6-16).The DFS algorithm constructs the reduced state graphdirectly.Constructing the full state graph and later reducing it woulddefy the purpose of the reduction.12Depth-First-Search Algorithm (Cont.)When model checking is applied to the reduced state graphit terminates with a positive answer when the property holdsfor the original state graph.it produces a counterexample, otherwiseNote: The counterexample may differ from one obtained usingthe full state graph.13Ample SetsIn order to implement the algorithm we must find a systematicway of calculatingampl e(s)for any given states.The calculation ofampl e(s)needs to satisfy three goals:1. Whenampl e(s)is used instead ofenabl ed(s), enoughbehaviors must be retained so DFS gives correct results.2. Usingampl e(s)instead ofenabl ed(s)should result in asignificantly smaller state graph.3. The overhead in calculatingampl e(s)must be reasonablysmall.14Dependence and IndependenceAn independence relationITTis a symmetric,antireflexive relation such that fors2Sand(; )2I:Enabledness If; 2enabl ed(s)then2enabl ed((s)).Commutativity; 2enabl ed(s)then((s)) =((s)).Thedependency relationDis the complement ofI, namelyD= (TT)nI :NoteThe enabledness condition states that a pair of independenttransitions do notdisable one another.However, that it is possible for one to enable another.15Potential ProblemsSuppose thatandcommute:s2s1rsR  RIt does not matter whetheris executed