IA169 Model Checking Bounded model checking and k-induction Jan Strejˇcek Faculty of Informatics Masaryk University Motivation BDDs represents all models of the corresponding propositional formulas in LTL model checking, we want to decide whether some violating run exists if we represent violating runs by a formula, we need to decide its satisfiability SAT solvers can efficiently decide it (despite NP-completeness of the problem) IA169 Model Checking: Bounded model checking and k-induction 2/39 Motivation BDDs represents all models of the corresponding propositional formulas in LTL model checking, we want to decide whether some violating run exists if we represent violating runs by a formula, we need to decide its satisfiability SAT solvers can efficiently decide it (despite NP-completeness of the problem) for satisfiable formulas, SAT solvers provide a model a formula φ is true iff ¬φ is not satisfiable IA169 Model Checking: Bounded model checking and k-induction 3/39 Agenda and sources agenda finite Kripke structures represented by formulas bounded model checking (BMC) for safety properties BMC for LTL properties completeness of BMC k-induction source Chapter 10 of E. M. Clarke, O. Grumberg, D. Kroening, D. Peled, and H. Veith: Model Checking, Second Edition, MIT, 2018. IA169 Model Checking: Bounded model checking and k-induction 4/39 Finite Kripke structures represented by formulas Finite Kripke structures represented by formulas each Kripke structure K = (S, T, S0, L) with finitely many states and a finite set of used atomic propositions can be encoded by propositional formulas states in S correspond to assignments s : V → {0, 1}, where V = {x1, . . . , xn} S0 is identified with a formula S0(x1, . . . , xn) satisfied by initial states transition relation T ⊆ S × S is identified with a formula T(x1, . . . , xn, x′ 1, . . . , x′ n) we replace L : S → 2AP with a formula p(x1, . . . , xn) for each relevant p ∈ AP IA169 Model Checking: Bounded model checking and k-induction 6/39 Finite Kripke structures represented by formulas each Kripke structure K = (S, T, S0, L) with finitely many states and a finite set of used atomic propositions can be encoded by propositional formulas states in S correspond to assignments s : V → {0, 1}, where V = {x1, . . . , xn} S0 is identified with a formula S0(x1, . . . , xn) satisfied by initial states transition relation T ⊆ S × S is identified with a formula T(x1, . . . , xn, x′ 1, . . . , x′ n) we replace L : S → 2AP with a formula p(x1, . . . , xn) for each relevant p ∈ AP 00 p 01 p 10 p 11 ¬p S0(x1, x2) = ¬x1 ∧ ¬x2 T(x1, x2, x′ 1, x′ 2) = (¬x1 ∧ ¬x2 ∧ ¬x′ 1 ∧ x′ 2) ∨ (¬x1 ∧ x2 ∧ x′ 1) ∨ ∨ (x1 ∧ ¬x2 ∧ ¬x′ 1 ∧ ¬x′ 2) ∨ (x1 ∧ x2 ∧ ∧x′ 1 ∧ x′ 2) p(x1, x2) = ¬x1 ∨ ¬x2 IA169 Model Checking: Bounded model checking and k-induction 7/39 Finite Kripke structures represented by formulas we write ⃗x instead of x1, . . . , xn, i.e., we use S0(⃗x), T(⃗x,⃗x′) and p(⃗x) when building formulas about more than one or two states, we will use ⃗x0,⃗x1, . . ., where ⃗xi stands for xi1, . . . , xi n for example, models of T(⃗x0,⃗x1) ∧ T(⃗x1,⃗x2) represent paths of length 2 recall that we assume that each state has at least one successor IA169 Model Checking: Bounded model checking and k-induction 8/39 Bounded model checking (BMC) for safety properties Basic idea of bounded model checking (BMC) if a finite system violates a given property, it often has a short counterexample bounded model checking (BMC) analyzes runs up to the first k steps if an erroneous run is found, we know that the system violates the property; otherwise, we can increase k and try again IA169 Model Checking: Bounded model checking and k-induction 10/39 Basic idea of bounded model checking (BMC) if a finite system violates a given property, it often has a short counterexample bounded model checking (BMC) analyzes runs up to the first k steps if an erroneous run is found, we know that the system violates the property; otherwise, we can increase k and try again let us consider the safety property Gp the property is violated iff some run satisfies F¬p there is a run violating the property within the first k steps iff the following formula is satisfiable S0(⃗x0) ∧ k−1 i=0 T(⃗xi,⃗xi+1) ∧ k i=0 ¬p(⃗xi) IA169 Model Checking: Bounded model checking and k-induction 11/39 Basic idea of bounded model checking (BMC) if a finite system violates a given property, it often has a short counterexample bounded model checking (BMC) analyzes runs up to the first k steps if an erroneous run is found, we know that the system violates the property; otherwise, we can increase k and try again let us consider the safety property Gp the property is violated iff some run satisfies F¬p there is a run violating the property within the first k steps iff the following formula is satisfiable S0(⃗x0) ∧ k−1 i=0 T(⃗xi,⃗xi+1) ∧ k i=0 ¬p(⃗xi) for example, for k = 3 the formula is S0(⃗x0) ∧ T(⃗x0,⃗x1) ∧ T(⃗x1,⃗x2) ∧ T(⃗x2,⃗x3) ∧ ¬p(⃗x0)∨¬p(⃗x1)∨¬p(⃗x2)∨¬p(⃗x3) IA169 Model Checking: Bounded model checking and k-induction 12/39 BMC for safety properties bounded model checker for safety properties 1 set k to some initial (relatively low) number 2 construct the formula ψk = S0(⃗x0) ∧ k−1 i=0 T(⃗xi,⃗xi+1) ∧ k i=0 ¬p(⃗xi) 3 ask a SAT solver for satisfiability of ψk 4 if ψk is satisfiable, then report K ̸|= Gp and construct a counterexample from the obtained model 5 if ψk is unsatisfiable, increase k and go to 2 IA169 Model Checking: Bounded model checking and k-induction 13/39 BMC for safety properties bounded model checker for safety properties 1 set k to some initial (relatively low) number 2 construct the formula ψk = S0(⃗x0) ∧ k−1 i=0 T(⃗xi,⃗xi+1) ∧ k i=0 ¬p(⃗xi) 3 ask a SAT solver for satisfiability of ψk 4 if ψk is satisfiable, then report K ̸|= Gp and construct a counterexample from the obtained model 5 if ψk is unsatisfiable, increase k and go to 2 the size of ψk is linear in k the method is not complete: it never ends for correct systems IA169 Model Checking: Bounded model checking and k-induction 14/39 BMC for LTL properties BMC for LTL properties we want to check whether a (fair) Kripke structure K satisfies an LTL formula φ assume that we have a generalized Büchi automaton B representing a product of K and an automaton for ¬φ K |=(F) φ iff L(B) = ∅ L(B) ̸= ∅ iff there exists an accepting lasso-shaped run of B of the form τ.ρω bounded model checking looks for accepting runs τ.ρω such that |τρ| ≤ k if such a run exists, then L(B) ̸= ∅ and thus K ̸|=(F) φ IA169 Model Checking: Bounded model checking and k-induction 16/39 BMC for LTL properties assume that the GBA B is described by propositional formulas S0(⃗x) is satisfied by initial states T(⃗x,⃗x′) represents the transiton relation (the letters on transitions are ignored as they have no influence on the existence of accepting runs) for each Fl ∈ F, Fl(⃗x) represents the elements of accepting set Fl IA169 Model Checking: Bounded model checking and k-induction 17/39 BMC for LTL properties assume that the GBA B is described by propositional formulas S0(⃗x) is satisfied by initial states T(⃗x,⃗x′) represents the transiton relation (the letters on transitions are ignored as they have no influence on the existence of accepting runs) for each Fl ∈ F, Fl(⃗x) represents the elements of accepting set Fl there exists an accepting run τ.ρω such that |τρ| = k iff the following formula is satisfiable S0(⃗x0) ∧ k−1 i=0 T(⃗xi,⃗xi+1) ∧ k−1 i=0 ⃗xi = ⃗xk ∧ Fl ∈F k−1 j=i Fl(⃗xj) IA169 Model Checking: Bounded model checking and k-induction 18/39 BMC for LTL properties assume that the GBA B is described by propositional formulas S0(⃗x) is satisfied by initial states T(⃗x,⃗x′) represents the transiton relation (the letters on transitions are ignored as they have no influence on the existence of accepting runs) for each Fl ∈ F, Fl(⃗x) represents the elements of accepting set Fl there exists an accepting run τ.ρω such that |τρ| = k iff the following formula is satisfiable S0(⃗x0) ∧ k−1 i=0 T(⃗xi,⃗xi+1) ∧ k−1 i=0 ⃗xi = ⃗xk ∧ Fl ∈F k−1 j=i Fl(⃗xj) τ ρ s0 s1 · · · si−1 si = sk si+1 · · · sk−1 IA169 Model Checking: Bounded model checking and k-induction 19/39 BMC for LTL properties assume that there exists an accepting run τ.ρω such that |τρ| < k then τ.ρω = τ′.ρ′ω where τ′ρ′ is the prefix of τ.ρω such that |τ′ρ′| = k and |ρ′| = |ρ| hence, there exists an accepting run τ.ρω such that |τρ| ≤ k iff ψk is satisfiable ψk = S0(⃗x0) ∧ k−1 i=0 T(⃗xi,⃗xi+1) ∧ k−1 i=0 ⃗xi = ⃗xk ∧ Fl ∈F k−1 j=i Fl(⃗xj) IA169 Model Checking: Bounded model checking and k-induction 20/39 BMC for LTL properties assume that there exists an accepting run τ.ρω such that |τρ| < k then τ.ρω = τ′.ρ′ω where τ′ρ′ is the prefix of τ.ρω such that |τ′ρ′| = k and |ρ′| = |ρ| hence, there exists an accepting run τ.ρω such that |τρ| ≤ k iff ψk is satisfiable ψk = S0(⃗x0) ∧ k−1 i=0 T(⃗xi,⃗xi+1) ∧ k−1 i=0 ⃗xi = ⃗xk ∧ Fl ∈F k−1 j=i Fl(⃗xj) bounded model checker for LTL properties 1 set k to some initial (relatively low) number 2 construct the formula ψk and ask a SAT solver for its satisfiability 3 if ψk is satisfiable, then report K ̸|=(F) φ and construct a counterexample from the obtained model 4 if ψk is unsatisfiable, increase k and go to 2 IA169 Model Checking: Bounded model checking and k-induction 21/39 BMC for LTL properties assume that there exists an accepting run τ.ρω such that |τρ| < k then τ.ρω = τ′.ρ′ω where τ′ρ′ is the prefix of τ.ρω such that |τ′ρ′| = k and |ρ′| = |ρ| hence, there exists an accepting run τ.ρω such that |τρ| ≤ k iff ψk is satisfiable ψk = S0(⃗x0) ∧ k−1 i=0 T(⃗xi,⃗xi+1) ∧ k−1 i=0 ⃗xi = ⃗xk ∧ Fl ∈F k−1 j=i Fl(⃗xj) bounded model checker for LTL properties 1 set k to some initial (relatively low) number 2 construct the formula ψk and ask a SAT solver for its satisfiability 3 if ψk is satisfiable, then report K ̸|=(F) φ and construct a counterexample from the obtained model 4 if ψk is unsatisfiable, increase k and go to 2 the size of ψk (when counting all common subformulas only once) is linear in k the method is not complete: it never ends for correct systems IA169 Model Checking: Bounded model checking and k-induction 22/39 Completeness of BMC Completeness of BMC is there any k such that if BMC does not find any erroneous path using k then the system has to be safe? we will study this question for safety property Gp IA169 Model Checking: Bounded model checking and k-induction 24/39 Completeness of BMC is there any k such that if BMC does not find any erroneous path using k then the system has to be safe? we will study this question for safety property Gp the number of states a state satisfying ¬p is reachable from initial states iff it is reachable in |S| − 1 steps if the formula ψk for k = |S| − 1 is not satisfiable, then K |= Gp if states are modeled by Boolean variables x1, . . . , xn then |S| ≤ 2n this bound is too large to be practical IA169 Model Checking: Bounded model checking and k-induction 25/39 Completeness of BMC diametr of the system graph graph diametr d is the maximal length of all shortest paths between any two graph nodes a state satisfying ¬p is reachable from initial states iff it is reachable in d steps if the formula ψk for k = d is not satisfiable, then K |= Gp IA169 Model Checking: Bounded model checking and k-induction 26/39 Completeness of BMC diametr of the system graph graph diametr d is the maximal length of all shortest paths between any two graph nodes a state satisfying ¬p is reachable from initial states iff it is reachable in d steps if the formula ψk for k = d is not satisfiable, then K |= Gp how to determine d without constructing the graph? asking the user is not realistic safe upper bounds (like d ≤ |S| − 1) are extremely overstated IA169 Model Checking: Bounded model checking and k-induction 27/39 k-induction Proof of correctness by induction another way to prove that K |= Gp with SAT solvers we need to prove that p holds in all states reachable from the initial states induction 1 base case: all initial states satisfy p, i.e., S0(⃗x) ∧ ¬p(⃗x) is unsatisfiable 2 induction step: if a state satisfies p, then each its successor satisfies p, i.e., the following formula is unsatisfiable p(⃗x) ∧ T(⃗x,⃗x′ ) ∧ ¬p(⃗x′ ) IA169 Model Checking: Bounded model checking and k-induction 29/39 Proof of correctness by induction another way to prove that K |= Gp with SAT solvers we need to prove that p holds in all states reachable from the initial states induction 1 base case: all initial states satisfy p, i.e., S0(⃗x) ∧ ¬p(⃗x) is unsatisfiable 2 induction step: if a state satisfies p, then each its successor satisfies p, i.e., the following formula is unsatisfiable p(⃗x) ∧ T(⃗x,⃗x′ ) ∧ ¬p(⃗x′ ) p p p ¬p works well IA169 Model Checking: Bounded model checking and k-induction 30/39 Proof of correctness by induction another way to prove that K |= Gp with SAT solvers we need to prove that p holds in all states reachable from the initial states induction 1 base case: all initial states satisfy p, i.e., S0(⃗x) ∧ ¬p(⃗x) is unsatisfiable 2 induction step: if a state satisfies p, then each its successor satisfies p, i.e., the following formula is unsatisfiable p(⃗x) ∧ T(⃗x,⃗x′ ) ∧ ¬p(⃗x′ ) p p p ¬p p induction step fails IA169 Model Checking: Bounded model checking and k-induction 31/39 k-induction k-induction 1 base case: each path of length k starting in an initial state does not reach any state satisfying ¬p, i.e., the following formula is unsatisfiable S0(⃗x0) ∧ k−1 i=0 T(⃗xi,⃗xi+1) ∧ k i=0 ¬p(⃗xi) 2 induction step: if we prolong any path of length k over states satisfying p by one step, we reach a state satisfying p, i.e., the following formula is unsatisfiable k i=0 p(⃗xi) ∧ T(⃗xi,⃗xi+1) ∧ ¬p(⃗xk+1) the base case uses the formula from BMC: if it is satisfiable then K ̸|= Gp IA169 Model Checking: Bounded model checking and k-induction 32/39 k-induction k-induction 1 base case: each path of length k starting in an initial state does not reach any state satisfying ¬p, i.e., the following formula is unsatisfiable S0(⃗x0) ∧ k−1 i=0 T(⃗xi,⃗xi+1) ∧ k i=0 ¬p(⃗xi) 2 induction step: if we prolong any path of length k over states satisfying p by one step, we reach a state satisfying p, i.e., the following formula is unsatisfiable k i=0 p(⃗xi) ∧ T(⃗xi,⃗xi+1) ∧ ¬p(⃗xk+1) the base case uses the formula from BMC: if it is satisfiable then K ̸|= Gp p p p ¬p p works well for k = 1IA169 Model Checking: Bounded model checking and k-induction 33/39 k-induction k-induction 1 base case: each path of length k starting in an initial state does not reach any state satisfying ¬p, i.e., the following formula is unsatisfiable S0(⃗x0) ∧ k−1 i=0 T(⃗xi,⃗xi+1) ∧ k i=0 ¬p(⃗xi) 2 induction step: if we prolong any path of length k over states satisfying p by one step, we reach a state satisfying p, i.e., the following formula is unsatisfiable k i=0 p(⃗xi) ∧ T(⃗xi,⃗xi+1) ∧ ¬p(⃗xk+1) the base case uses the formula from BMC: if it is satisfiable then K ̸|= Gp p p p ¬p p induction step fails for each k IA169 Model Checking: Bounded model checking and k-induction 34/39 k-induction a state satisfying ¬p is reachable iff it is reachable by an acyclic path hence, the induction step can consider only acyclic paths 2 induction step: if we prolong any path of length k over states satisfying p by one step such that we get an acyclic path, we reach a state satisfying p, i.e., the following formula is unsatifiable k i=0 p(⃗xi) ∧ T(⃗xi,⃗xi+1) ∧ 0≤i