Learn Shen
Community Wiki
OS Kernel
OS Library
Shen Professional


Model Checking

Mark Tarver 2017

1. Model Checking

Model checking involves testing to see if a given set of propositions in a formal language has a model. In the case of propositional calculus the programs that test for the satisfiability of a set of formulae are called SAT solvers. Rather more general is a first-order model checker that operates with the concept of a model for a sentence of first-order logic.

1. Model Checking

2. A Model Checker

In first-order model theory an interpretation for a propositional atom is a truth-value (true or false).  An interpretation I of a first-order atom P(t1,...,tn) requires a domain (non-empty set) D.  I  assigns to P an n-ary relation I(P) drawn from D and an object I(ti) from D for each ti. The truth-conditions can now be stated simply. P(t1,...,tn) is true under I just when the tuple <I(t1),...,I(tn)> is in I(P). 

Thus if we fix D to the set of natural numbers and assign to the relation symbol R the relation > occupied by all pairs of number <m, n> such that m > n, and to a the number 5 and to b the number 3, then the resulting interpretation is true (is a model) for R(a, b).   From then on the model theory for the logical connectives follows the expected pattern.

I(~ p) = true if I(p) = false
I(~ p) = false if I(p) = true
I(p v q) = true if I(p) = true or I(q) = true
I(p v q) = false if I(p) = I(q) = false
I(p & q) = true if I(p) = I(q) = true
I(p & q) = false if I(p) = false or I(q) = false
I(p => q) = true if I(p) = false or I(q) = true
I(p => q) = false if I(p) = true and I(q) = false
I(p <=> q) = true if I(p) = I(q)
I(p <=> q) = false if I(p) <> I(q)

When it comes to the quantifiers, first-order model theory introduces us to the idea of the domain D of a quantifier.  exists x P(t1,..., x,...,tn)  is true under I just when there is an object d in D such that <I (t1), ..., d,..., I (tn)> is in I(P).   forall x P(t1,...,x,...,tn) is true under I just when for every object d in D <I(t1), ..., d,..., I(tn)> is in I(P). 

2. A Model Checker

The model checker in this package operates with the concept that quantifiers have domains which are effectively enumerable by means of data structures called series (sometimes called streams or progressions elsewhere). A series has

  1. An initial element.
  2. A computable means of generating a successor from any element.
  3. A terminating function that returns a boolean signifying that the last element of the series has been reached.

This data structure is represented here by a parametric type series over three element lists.

(datatype series

B : A; S : (A --> A); T : (A --> boolean);
[B S T] : (series A);)

For example the 3 element list [0 (+ 1) (/. E false)] represents the natural number series and has the type (series number). The numbers 0 to 1000 can be reprsented by [0 (+ 1) (< 1001)].

The two quantifiers in the package are represented by exists? and forall?. For instance (exists? X [0 (+ 1) (< 15)] (= (+ X X) 10)) claims that there exists a number within the interval 0-14 which when added to itself gives 10. (exists? X [200 (+ 1) (< 230)] (prime? X)) claims a number within the interval 200-229 is prime. (forall? X [0 (+ 1) (< 15)] (even? (+ X X) 10)) claims every member of this interval is even. These functions return boolean results.

Multiple quantifiers are allowed and quantified variables can appear in a series; (exists? X [0 (+ 1) (/. E false)] (forall? Y [0 (+ 1) (< X)] (not (= (* Y Y) X)))) states that there is a natural number X such that for every natural number Y less than X, X is not identical to the square of Y.

There is no facility in this version to return values for X in such cases though the user can arrange for them to be printed; e.g.

(exists? X [0 (+ 1) (< 15)] (show X (= (+ X X) 10)))

(define show
{A --> boolean --> boolean}
_ false -> false
X Y -> (do (print X) Y))

prints 5 and returns true.