Efficient Patterns for Model Checking Partial State Spaces in CTL & LTL

File Description SizeFormat 
Efficient Patterns for Model Checking Partial.pdfdefault185.43 kBAdobe PDFDownload
Title: Efficient Patterns for Model Checking Partial State Spaces in CTL & LTL
Author(s): Antonik A
Huth M
Item Type: Journal Article
Abstract: Compositional model checks of partial Kripke structures are efficient but incomplete as they may fail to recognize that all implementations satisfy the checked property. But if a property holds for such checks, it will hold in all implementations. Such checks are therefore under-approximations. In this paper we determine for which popular specification patterns, documented at a communityled pattern repository, this under-approximation is precise in that the converse relationship holds as well for all model checks. We find that many such patterns are indeed precise. Those that arent lose precision because of a sole propositional atom in mixed polarity. Hence we can compute, with linear blowup only, a semantic minimization in the same temporal logic whose efficient check renders the precise result for the original imprecise pattern. Thus precision can be secured for all patterns at low cost. © 2006 Elsevier B.V. All rights reserved.
Publication Date: 5-May-2006
Citation: Electronic Notes in Theoretical Computer Science Vol.( 158 ) No.( ) pp 41 - 57
URI: http://hdl.handle.net/10044/1/807
Publisher Link: http://dx.doi.org/10.1016/j.entcs.2006.04.004
Start Page: 41
End Page: 57
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 158 (May 2006). doi:10.1016/j.entcs.2006.04.004.
Volume: 158
Appears in Collections:Quantitative Analysis and Decision Science



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

Creative Commons