Lecture 9: Small Model Theory A. PnueliSmall Model TheoryAs previously stated, we would like to separate the two main activities (andchallenges) associated withdeductive 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 adebugging tool, then thiswould usually uncover most of the existing bugs. However, if we wish to establishtheabsolute correctness of the system, this is insufficient.Much research has been expended in trying to identify acutoff value N0suchthat∀N : S(N ) |= ψ iff S(N0) |= ψ.So far, only partial results have been obtained byEmerson, 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, forhwhen 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 forMUX-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 forMUX-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 oftypeindex.• Boolean arrays — y1, . . . , yc: array[1..N] of boolean.We define anindex term to be an index variable ijor one of the constants 1, N .Anatomic formula is a boolean variable xk, a boolean term a[t], where a is anarray andt is an index term, or a comparison t1< t2, where t1and t2are indexterms.Aboolean R-assertion is a boolean combination of atomic formulas.AnR 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.AnR-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 arrayy.For example a3-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 whetherM(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 sizen > k + 2 can be reduced to asatisfying model of sizen − 1.LetM 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 any index term. Note that1 <