Consistent partial model checking

File Description SizeFormat 
Consistent partial model checking.pdf400.09 kBAdobe PDFDownload
Title: Consistent partial model checking
Author(s): Huth,M.
Pradhan,S.
Item 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.
Publication Date: 25-Oct-2004
Citation: Electronic Notes in Theoretical Computer Science Vol.( 73 ) No.( ) pp 45 - 85
URI: http://hdl.handle.net/10044/1/806
Publisher Link: http://dx.doi.org/10.1016/j.entcs.2004.08.003
ISSN: 1571-0661
Start Page: 45
End Page: 85
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 .
Volume: 73
Appears in Collections:Quantitative Analysis and Decision Science



Items in Spiral are protected by copyright, with all rights reserved, unless otherwise indicated.

Creative Commons