29
IRUS TotalDownloads
Altmetric
On the complexity of semantic self-minimization
File | Description | Size | Format | |
---|---|---|---|---|
complexity-semantic-minimization.pdf | Accepted version | 313.65 kB | Adobe PDF | View/Open |
Title: | On the complexity of semantic self-minimization |
Authors: | 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. |
Issue 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 |