Consistent partial model checking
Author(s)
Huth,M.
Pradhan,S.
Type
Journal Article
Abstract
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.
Date Issued
2004
Citation
Electronic Notes in Theoretical Computer Science, 2004, 73, pp.45-85
ISSN
1571-0661
Start Page
45
End Page
85
Journal / Book Title
Electronic Notes in Theoretical Computer Science
Volume
73
Copyright Statement
© 2004 Elsevier B.V. This is the author’s version of a work that was accepted for publication in Electronic Notes in Theoretical Computer Science. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version was subsequently published in Electronic Notes in Theoretical Computer Science, volume 75 (October 2004). doi:10.1016/j.entcs.2004.08.003 .
Source Volume Number
73