On the complexity of semantic self-minimization

File Description SizeFormat 
complexity-semantic-minimization.pdfAccepted version313.65 kBAdobe PDFDownload
Title: On the complexity of semantic self-minimization
Author(s): Antonik, A
Huth, M
Item Type: Journal Article
Abstract: Partial Kripke structures model only parts of a state space and so enable aggressive abstraction of systems prior to verifying them with respect to a formula of temporal logic. This partiality of models means that verifications may reply with true (all refinements satisfy the formula under check), false (no refinement satisfies the formula under check) or dont know. Generalized model checking is the most precise verification for such models (all dont know answers imply that some refinements satisfy the formula, some dont), but computationally expensive. A compositional model-checking algorithm for partial Kripke structures is efficient, sound (all answers true and false are truthful), but may lose precision by answering dont know instead of a factual true or false. Recent work has shown that such a loss of precision does not occur for this compositional algorithm for most practically relevant patterns of temporal logic formulas. Formulas that never lose precision in this manner are called semantically self-minimizing. In this paper we provide a systematic study of the complexity of deciding whether a formula of propositional logic, propositional modal logic or the propositional modal mu-calculus is semantically self-minimizing. © 2009 Elsevier B.V. All rights reserved.
Publication Date: 1-Sep-2009
Citation: Electronic Notes in Theoretical Computer Science Vol.( 250 ) No.( 1 ) pp 3 - 19
URI: http://hdl.handle.net/10044/1/5792
Publisher Link: http://dx.doi.org/10.1016/j.entcs.2009.08.002
DOI: 10.1016/j.entcs.2009.08.002
ISSN: 1571-0661
Publisher: Elsevier
Start Page: 3
End Page: 19
Copyright Statement: © 2009 Elsevier B.V. All rights reserved. NOTICE: 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, VOL:250, ISSUE:1, (2009) DOI:10.1016/j.entcs.2009.08.002
Volume: 250
Appears in Collections:Quantitative Analysis and Decision Science



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

Creative Commons