On the complexity of semantic self-minimization
File(s)
Accepted version
Author(s)
Antonik, A
Huth, M
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 donÆt know. Generalized model checking is the most precise verification for such models (all donÆt know answers imply that some refinements satisfy the formula, some donÆt), 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 donÆt 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.\r\n
Date Issued
2008
Citation
Electronic Notes in Theoretical Computer Science, 2008, 250 (1), pp.3-19
ISSN
1571-0661
Publisher
Elsevier
Start Page
3
End Page
19
Journal / Book Title
Electronic Notes in Theoretical Computer Science
Volume
250
Issue
1
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
Source Volume Number
250
Coverage Spatial
Oxford, UK