Lecture 9: Small Model Theory A. PnueliSmall Model TheoryAs previously stated, we would like to separate the two main activities (andchallenges) associated with deductive verification:• The invention of auxiliary constructs.• Establishing the validity of the premises of the relevant rule.In this lecture, we will present one of the simplest methods for deciding validity ofthe premises – the small model theory.Analysis of Reactive Systems, NYU, Spring, 2006 149Lecture 9: Small Model Theory A. PnueliParameterized SystemsIn its simplest form, a parameterized system is a parallel composition, such asS(N) = P [1] k · · · k P [N] or S(N) = C k P [1] k · · · k P [N ]where N > 1 is a parameter and P [1], . . . , P [N] are finite-state processes.Uniform Verification: Establish in one verification effort that all instances of thesystem satisfy a property ψ. That is, S(N) |= ψ, for every N > 1.Analysis of Reactive Systems, NYU, Spring, 2006 150Lecture 9: Small Model Theory A. PnueliNon-Mathematical InductionOf course, we can check separately S( 2) |= ψ, S(3) |= ψ, S(4) |= ψ, etc. Supposethey all come out valid. What can we conclude?To the extent that formal verification is viewed as a debugging tool, then thiswould usually uncover most of the existing bugs. However, if we wish to establishthe absolute correctness of the system, this is insufficient.Much research has been expended in trying to identify a cutoff value N0suchthat∀N : S(N ) |= ψ iff S(N0) |= ψ.So far, only partial results have been obtained by Emerson, Ip, and Namjoshi.Analysis of Reactive Systems, NYU, Spring, 2006 151Lecture 9: Small Model Theory A. PnueliExample: MUTEXMUTEX[N] ::in N : natural where N > 1local x : boolean where x = 1Nh=1P [h] : :loop forever doℓ0: Non-Criticalℓ1: request xℓ2: Criticalℓ3: release xThe semaphore instructions “request x” and “release x” appearing in theprogram stand, respectively, for hwhen x = 1 do x := 0i and x := 1Suppose we wish to establish the invariance of the assertionp : at−ℓ2[1] →(x = 0). This assertion is not inductive by itself. We need tostrengthen it into the inductive assertion:ϕ: ∀i 6= j : (at−ℓ2,3[i] + at−ℓ2,3[j] + x) ≤ 1It only remains to check the validity of the premises of rule INV.Analysis of Reactive Systems, NYU, Spring, 2006 152Lecture 9: Small Model Theory A. PnueliChecking the Premises for MUX-SEM[5]We can check the validity of the premises by using BDD techniques, e.g. usingTLV. In file mux5.pf we write:To calc-phi;Let phi := 1;For (i in 1...N)For (j in i+1...N)Let phi := phi &(((P[i].loc in 2..3) + (P[j].loc in 2..3) + x) <= 1);End -- For (j in i+1...N)End -- For (i in 1...N)End -- To calc-phi;Analysis of Reactive Systems, NYU, Spring, 2006 153Lecture 9: Small Model Theory A. PnueliPremise Checking for MUX-SEM[5] ContinuedLet p := ((P[1].loc=2) -> (x=0));calc-phi;Let counter := Theta & !phi; -- Check Premise 1If (counter)Print ‘‘\n Premise 1 invalid: ‘‘,counter,’’\n’’; Quit;End -- If (counter)Let counter := phi & rho & !next(phi); -- Check Premise 2If (counter)Print ‘‘\n Premise 2 invalid: ‘‘,counter,’’\n’’; Quit;End -- If (counter)Let counter := phi & !p; -- Check Premise 3If (counter)Print ‘‘\n Premise 3 invalid: ‘‘,counter,’’\n’’; Quit;End -- If (counter)Analysis of Reactive Systems, NYU, Spring, 2006 154Lecture 9: Small Model Theory A. PnueliR-AssertionsConsider the following signature:• Boolean variables — x1, . . . , xa: boolean.• Index variables — i1, . . . , ib: [1..N]. 1 and N are considered to be constants oftype index.• Boolean arrays — y1, . . . , yc: array[1..N] of boolean.We define an index term to be an index variable ijor one of the constants 1, N .An atomic formula is a boolean variable xk, a boolean term a[t], where a is anarray and t is an index term, or a comparison t1< t2, where t1and t2are indexterms.A boolean R-assertion is a boolean combination of atomic formulas.An R assertion is built out of boolean R assertions to which we apply furtherboolean operations and quantification over index variables. For example:∀i : ∃j ≥ i : y[j] 6= y[i]∀i : (1 ≤ i ≤ N ) → ∃j : i ≤ j ∧ j ≤ N ∧ y[j] 6= y[i]Note that the first formula can be viewed as an abbreviation of the second formula.An R-assertion of the form ∀i1, . . . , ik: ∃j1, . . . , jm:ϕ, whereϕis a booleanR-assertions is called an AER-assertion.Analysis of Reactive Systems, NYU, Spring, 2006 155Lecture 9: Small Model Theory A. Pnuelin-ModelsLet ψ be an R-assertion. An n-model M(n) over the vocabulary of ψ provides thefollowing interpretation to the elements appearing in ψ:• Each boolean variable xjis assigned a value from {0, 1}.• Each index variable ijis assigned a value from [1..n]. The constants 1 and Nare assigned the values 1 and n.• Each array variable ajis assigned a boolean array of size n.In general, it is not necessary to assign values to index variables which appearbounded in ψ. Thus, an adequate model over the vocabulary of the AER-assertion ∀i : ∃j ≥ i : y[j] 6= y[i] should only interpret the constant N (as n)and the array y.For example a 3-model for this formula can be specified by the assignment:N = 3, y = (0, 1, 1)Given an R-assertion ψ and a model M(n), we can evaluate ψ over M(n), andfind out whether M(n) satisfies ψ. R-assertion ψ is said to be valid if it is satisfiedby every model.Analysis of Reactive Systems, NYU, Spring, 2006 156Lecture 9: Small Model Theory A. PnueliA Small Model TheoremLet ψ : ∀i1, . . . , ik: ∃j1, . . . , jm:ϕbe a closed AER-assertion.Claim 15. [Small Model Theorem]Assertion ψ is valid iff it is satisfied by all models M(n) for n ≤ k + 2.Proof Sketch:In order to prove the claim, it is sufficient to show that if the negationχ = ¬ ψ = ∃i1, . . . , ik: ∀j1, . . . , jm: ¬ϕhas a satisfying model M (n) of sizen > k + 2 then it also has a satisfying model of size ≤ k + 2. We establish thisby showing that every satisfying model of size n > k + 2 can be reduced to asatisfying model of size n − 1.Let M be a satisfying model of size n > k+2. Model M assigns to 1, i1, . . . , ik, Nvalues ranging in the set 1..n. This set of values can contain at most k + 2 < ndistinct values. Thus, there must exists some value r ∈ 1..n which is not theinterpretation of