robust vacuity for branching temporal logic

ISCAS OpenIR

	robust vacuity for branching temporal logic
	Gurfinkel Arie; Chechik Marsha
	2012
发表期刊	ACM TRANSACTIONS ON COMPUTATIONAL LOGIC
ISSN	1529-3785
卷号	13 期号:1 页码:-
摘要	There is a growing interest in techniques for detecting whether a logic specification is satisfied too easily, or vacuously. For example, the specification "every request is eventually followed by an acknowledgment" is satisfied vacuously by a system that never generates any requests. Vacuous satisfaction misleads users of model-checking into thinking that a system is correct. It is a serious problem in practice. There are several existing definitions of vacuity. Originally, Beer et al. 1997 formalized vacuity as insensitivity to syntactic perturbation (syntactic vacuity). This formulation captures the intuition of "vacuity" when applied to a single occurrence of a subformula. Armoni et al. argued that vacuity must be robust; not affected by semantically invariant changes, such as extending a model with additional atomic propositions. They show that syntactic vacuity is not robust for subformulas of linear temporal logic, and propose an alternative definition; trace vacuity. In this article, we continue this line of research. We show that trace vacuity is not robust for branching time logic. We further refine the notion of vacuity so that it applies uniformly to linear and branching time logic and does not suffer from the common pitfalls of prior definitions. Our new definition, bisimulation vacuity, is a proper and nontrivial extension of both syntactic and trace vacuity. We discuss the complexity of detecting bisimulation vacuity, and identify several practically-relevant subsets of CTL* for which vacuity detection problem is reducible to model-checking. We believe that in most practical applications, bisimulation vacuity provides both the desired theoretical properties and is tractable computationally.; There is a growing interest in techniques for detecting whether a logic specification is satisfied too easily, or vacuously. For example, the specification "every request is eventually followed by an acknowledgment" is satisfied vacuously by a system that never generates any requests. Vacuous satisfaction misleads users of model-checking into thinking that a system is correct. It is a serious problem in practice. There are several existing definitions of vacuity. Originally, Beer et al. 1997 formalized vacuity as insensitivity to syntactic perturbation (syntactic vacuity). This formulation captures the intuition of "vacuity" when applied to a single occurrence of a subformula. Armoni et al. argued that vacuity must be robust; not affected by semantically invariant changes, such as extending a model with additional atomic propositions. They show that syntactic vacuity is not robust for subformulas of linear temporal logic, and propose an alternative definition; trace vacuity. In this article, we continue this line of research. We show that trace vacuity is not robust for branching time logic. We further refine the notion of vacuity so that it applies uniformly to linear and branching time logic and does not suffer from the common pitfalls of prior definitions. Our new definition, bisimulation vacuity, is a proper and nontrivial extension of both syntactic and trace vacuity. We discuss the complexity of detecting bisimulation vacuity, and identify several practically-relevant subsets of CTL* for which vacuity detection problem is reducible to model-checking. We believe that in most practical applications, bisimulation vacuity provides both the desired theoretical properties and is tractable computationally.
收录类别	SCI
关键词	Verification Vacuity Detection
部门归属	Gurfinkel Arie Carnegie Mellon Univ Inst Software Engn Pittsburgh PA 15213 USA. Chechik Marsha Univ Toronto Toronto ON M5S 1A1 Canada.
学科领域	Computer Science ; Science & Technology - Other Topics
资助者	NSERC; OGS; IBM
语种	英语
内容类型	期刊论文
URI标识	http://ir.iscas.ac.cn/handle/311060/15093
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Gurfinkel Arie,Chechik Marsha. robust vacuity for branching temporal logic[J]. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC,2012,13(1):-.
APA	Gurfinkel Arie,&Chechik Marsha.(2012).robust vacuity for branching temporal logic.ACM TRANSACTIONS ON COMPUTATIONAL LOGIC,13(1),-.
MLA	Gurfinkel Arie,et al."robust vacuity for branching temporal logic".ACM TRANSACTIONS ON COMPUTATIONAL LOGIC 13.1(2012):-.