Consistent Partial Model Checking

We propose assertion-consistency (AC) semi-lattices as suitable orders for the anal- ysis of partial models. Such orders express semantic entailment, multiple-viewpoint and multiple-valued analysis, maintain internal consistency of reasoning, and sub- sume nite De Morgan lattices. We classify those orders that are nite and distribu- tive and apply them to design an ecien t algorithm for multiple-viewpoint checking, where checks are delegated to single-viewpoint models | ecien tly driven by the order structure. Instrumentations of this algorithm enable the detection and lo- cation of inconsistencies across viewpoint boundaries. To validate the approach, we investigate multiple-valued models and their compositional property semantics over a nite distributive AC lattice. We prove that this semantics is computed by our algorithm above whenever the primes of the AC lattice determine 'pro- jected' single viewpoints and the order between primes is preserved as renemen ts of single-viewpoint models. As a case study, we discuss a multiple-valued notion of state-machines with rst-order logic plus transitive closure.