Consistent Partial Model Checking
Michael Huth, Shekhar Pradhan · Electronic Notes in Theoretical Computer Science · 2004
We propose assertion-consistency (AC) semi-lattices as suitable orders for the analysis of partial models. Such orders express semantic entailment, multiple-viewpoint and multiple-valued analysis, maintain internal consistency of reasoning, and subsume finite De Morgan lattices. We classify those orders that are finite and distributive and apply them to design an efficient algorithm for multiple-viewpoint checking, where checks are delegated to single-viewpoint models - efficiently driven by the order structure. Instrumentations of this algorithm enable the detection and location of inconsistencies across viewpoint boundaries. To validate the approach, we investigate multiple-valued models and their compositional property semantics over a finite distributive AC lattice. We prove that this semantics is computed by our algorithm above whenever the primes of the AC lattice determine projected single viewpoints and the order between primes is preserved as refinements of single-viewpoint models. As a case study, we discuss a multiple-valued notion of state-machines with first-order logic plus transitive closure. © 2004 Elsevier B.V. All rights reserved.