Topological analysis of refinement

File Description SizeFormat 
Topological analysis of refinement.pdf476.59 kBAdobe PDFDownload
Title: Topological analysis of refinement
Author(s): Huth M
Item Type: Journal Article
Abstract: A modal transition system has a class of implementations, its maximal refinements. This class determines satisfiability and validity judgments, and their compositional approximations, for formulas of Hennessy-Milner logic. Using topology, we prove structural properties of these judgments: refinement is reverse containment of classes of implementations, Hennessy-Milner logic characterizes refinement through validity judgments, implementation classes are topologically closed sets, Hennessy-Milner logic enjoys a compactness theorem on such classes, and a robust consistency measure between modal transition systems is definable. In particular, every formula of Hennessy-Milner logic is the finite disjunction of Hennessy-Milner logic formulas for which validity checks are reducible to model checks. © 2006 Elsevier B.V. All rights reserved.
Publication Date: 31-Aug-2006
Citation: Electronic Notes in Theoretical Computer Science Vol.( 161 ) No.( ) pp 3 - 23
Publisher Link:
Start Page: 3
End Page: 23
Copyright Statement: © 2006 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 161 (August 2006). doi:10.1016/j.entcs.2006.04.022.
Volume: 161
Appears in Collections:Quantitative Analysis and Decision Science

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

Creative Commons