On the Complexity of Semantic Self-minimization
On the Complexity of Semantic Self-minimization
复制标题
论语义自我最小化的复杂性
DOI：
10.1016/j.entcs.2009.08.002
复制
发表时间：
2009
影响因子：
--
通讯作者：
Antonik A
中科院分区：
文献类型：
--
作者：
Antonik A
部分克里普克结构只对状态空间的一部分进行建模，因此能够在根据时态逻辑公式验证系统之前对系统进行积极的抽象。模型的这种偏好性意味着验证可能回答为真(所有精化满足所检查的公式)、假(没有精化满足所检查的公式)或不知道。广义模型检查是对这类模型最精确的验证(所有不知道答案都意味着一些精化满足公式，有些不满足)，但计算代价很高。针对部分克里普克结构的组合模型检查算法是有效的、合理的(所有答案是真的和假的都是真的)，但可能会因为回答不知道而不是事实的真或假而失去精度。最近的工作表明，对于大多数实际相关的时态逻辑公式模式，这种组合算法不会出现这样的精度损失。以这种方式从不丢失精度的公式称为语义自最小化。本文系统地研究了判断命题逻辑、命题模态逻辑或命题模态模演算的公式在语义上是自简的复杂性。
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.
登录
查看更多内容
部分规范的决策问题：经验和最坏情况的复杂性
DOI：
--
发表时间：
2008
期刊：
影响因子：
--
作者：
Adam Antonik
通讯作者：
Adam Antonik
DOI：
10.1007/978-3-540-78499-9_9
发表时间：
2008
期刊：
ACM Trans. Program. Lang. Syst.
影响因子：
--
作者：
Adam Antonik;M. Huth;K. Larsen;Ulrik Nyman;A. Wąsowski
通讯作者：
A. Wąsowski
CTL 交集 LTL 中模型检查部分状态空间的有效模式
DOI：
10.1016/j.entcs.2006.04.004
发表时间：
2006
期刊：
[1988] Proceedings. Third Annual Information Symposium on Logic in Computer Science
影响因子：
--
作者：
Adam Antonik;M. Huth
通讯作者：
M. Huth
模态和混合规格已有 20 年历史
DOI：
--
发表时间：
2008
期刊：
Bull. EATCS
影响因子：
--
作者：
Adam Antonik;M. Huth;K. Larsen;Ulrik Nyman;A. Wąsowski
通讯作者：
A. Wąsowski
DOI：
10.1109/lics.2002.1029816
发表时间：
2002
期刊：
Proceedings 17th Annual IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
T. Reps;Alexey Loginov;Shmuel Sagiv
通讯作者：
Shmuel Sagiv