15-414 Bug Catching:Model CheckingSoonho [email protected] Oct 2011Model CheckingModel CheckingWhat is “Model”?Model CheckingKripke Structure is a triple , wherehS, R, Li• is the set of states• is the transition relation (left-total), and• gives the set of atomic propositions true in each stateSR ✓ S ⇥ SL : S !P(AP )p p, qqs0 s1s3s2Model CheckingWhat to Check?Model Checking ProblemKripke StructureProperty(Temporal Logic Formula)stateFind all states s such that M has property ƒ at state s.M,s |= fModel Checking ProblemKripke StructureProperty(Temporal Logic Formula)p p, qqs0 s1s3s2stateps0EX qFind all states s such that M has property ƒ at state s.M,s |= f?Model Checking ProblemKripke StructureProperty(Temporal Logic Formula)p p, qqs0 s1s3s2stateps0EX qFind all states s such that M has property ƒ at state s.M,s |= f|=Model Checking ProblemKripke StructureProperty(Temporal Logic Formula)p p, qqs0 s1s3s2stateEX qFind all states s such that M has property ƒ at state s.M,s |= fp, qs1?Model Checking ProblemKripke StructureProperty(Temporal Logic Formula)p p, qqs0 s1s3s2stateEX qFind all states s such that M has property ƒ at state s.M,s |= fp, qs16|=Model Checking ProblemKripke StructureProperty(Temporal Logic Formula)stateEX qFind all states s such that M has property ƒ at state s.M,s |= fp p, qqs0 s1s3s2Model CheckingWhat’s Temporal Logic (esp, CTL*)?The Logic CTL*The computation tree logic CTL* combines both branching-time and linear-time operators.In this logic a path quantifier can prefix an assertion composed of arbitrary combinations of the usual linear-time operators.1. Path quantifier:A - “for every path”E - “there exists a path”2. Linear-time operators: X p - p holds next time F p - p holds sometime in the future G p - p holds globally in the future p U q - p holds until q holdsSemantics of State FormulasFor a state formula f, the notationmeans that f holds at state s in the Kripke structure M.It’s inductively defined as follows:M,s |= fM, s |= p , p 2 L(s)psM, s |= ¬f , M, s 6|= fM,s |= f1_ f2, M, s |= f1or M, s |= f2Semantics of State FormulasFor a state formula f, the notationmeans that f holds at state s in the Kripke structure M.It’s inductively defined as follows:M,s |= fs |= E(g) , there exists a path ⇡ starting wit h ssuch that ⇡ |= g.…. …. …. ….Semantics of State FormulasFor a state formula f, the notationmeans that f holds at state s in the Kripke structure M.It’s inductively defined as follows:M,s |= fs |= A(g) , For all path ⇡ starti n g wi t h s,we have ⇡ |= g.…. …. …. ….Semantics of Path FormulasFor a path formula f, the notationmeans that f holds along path in the Kripke structure M. It’s inductively defined as follows:M, ⇡ |= f⇡….s = ⇡0s |= fM,⇡ |= f , s is the first stat e of ⇡ and s |= f.Semantics of Path FormulasFor a path formula f, the notationmeans that f holds along path in the Kripke structure M. It’s inductively defined as follows:M, ⇡ |= f⇡M,⇡ |= Xf , M, ⇡1|= fSemantics of Path FormulasFor a path formula f, the notationmeans that f holds along path in the Kripke structure M. It’s inductively defined as follows:M, ⇡ |= f⇡M,⇡ |= Xf , M, ⇡1|= f….M,⇡1|= f⇡0Semantics of Path FormulasFor a path formula f, the notationmeans that f holds along path in the Kripke structure M. It’s inductively defined as follows:M, ⇡ |= f⇡M, ⇡ |= Gf , for al l i  0,⇡i|= fSemantics of Path FormulasFor a path formula f, the notationmeans that f holds along path in the Kripke structure M. It’s inductively defined as follows:M, ⇡ |= f⇡⇡0M, ⇡ |= Gf , for al l i  0,⇡i|= f….Semantics of Path FormulasFor a path formula f, the notationmeans that f holds along path in the Kripke structure M. It’s inductively defined as follows:M, ⇡ |= f⇡M, ⇡ |= Ff , there exists i  0,⇡i|= fSemantics of Path FormulasFor a path formula f, the notationmeans that f holds along path in the Kripke structure M. It’s inductively defined as follows:M, ⇡ |= f⇡⇡0M, ⇡ |= Ff , there exists i  0,⇡i|= f….Semantics of Path FormulasFor a path formula f, the notationmeans that f holds along path in the Kripke structure M. It’s inductively defined as follows:M, ⇡ |= f⇡M,⇡ |= f1Uf2, there exists k  0 such that M, ⇡k|= f2and for all 0  j<k, M, ⇡j|= f1Semantics of Path FormulasFor a path formula f, the notationmeans that f holds along path in the Kripke structure M. It’s inductively defined as follows:M, ⇡ |= f⇡M,⇡ |= f1Uf2, there exists k  0 such that M, ⇡k|= f2and for all 0  j<k, M, ⇡j|= f1….⇡0….Model Checking ProblemKripke StructureProperty(Temporal Logic Formula)stateFind all states s such that M has property ƒ at state s.M,s |= fHow to Solve it?Model Checking ProblemKripke StructureProperty(Temporal Logic Formula)stateFind all states s such that M has property ƒ at state s.M,s |= fFixed-Point Computation, using the following Identity!AF f1= lfpZ.f1_ AX ZEF f1= lfpZ.f1_ EX ZAG f1= gfpZ.f1^ AX ZEG f1= gfpZ.f1^ EX ZA[f1Uf2]=lfpZ.f2_ (f1^ AX Z)E[f1Uf2]=lfpZ.f2_ (f1^ EX Z)p qpp qpp qpp qpE[pUq]=lfpZ.q _ (p ^ EX Z)Kripke Structure⌧1(False)⌧2(False)⌧3(False)This examples is from the textbook (page