ISCAS OpenIR
robust vacuity for branching temporal logic
Gurfinkel Arie; Chechik Marsha
2012
SourceACM TRANSACTIONS ON COMPUTATIONAL LOGIC
ISSN1529-3785
Volume13Issue:1Pages:-
English AbstractThere 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.
Indexed TypeSCI
KeywordVerification Vacuity Detection
DepartmentGurfinkel Arie Carnegie Mellon Univ Inst Software Engn Pittsburgh PA 15213 USA. Chechik Marsha Univ Toronto Toronto ON M5S 1A1 Canada.
SubjectComputer Science ; Science & Technology - Other Topics
SponsorshipNSERC; OGS; IBM
Language英语
Content Type期刊论文
URIhttp://ir.iscas.ac.cn/handle/311060/15093
Collection中国科学院软件研究所
Recommended Citation
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):-.
Files in This Item:
There are no files associated with this item.
Related Services
Recommend this item
Bookmark
Usage statistics
Export to Endnote
Google Scholar
Similar articles in Google Scholar
[Gurfinkel Arie]'s Articles
[Chechik Marsha]'s Articles
Baidu academic
Similar articles in Baidu academic
[Gurfinkel Arie]'s Articles
[Chechik Marsha]'s Articles
Bing Scholar
Similar articles in Bing Scholar
[Gurfinkel Arie]'s Articles
[Chechik Marsha]'s Articles
Terms of Use
No data!
Social Bookmark/Share
All comments (0)
No comment.
 

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