Institutional Repository
| robust vacuity for branching temporal logic | |
| Gurfinkel Arie; Chechik Marsha | |
| 2012 | |
| Source | ACM TRANSACTIONS ON COMPUTATIONAL LOGIC
 |
| ISSN | 1529-3785 |
| Volume | 13Issue:1Pages:- |
| English Abstract | 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. |
| Indexed Type | SCI |
| Keyword | Verification Vacuity Detection |
| Department | Gurfinkel Arie Carnegie Mellon Univ Inst Software Engn Pittsburgh PA 15213 USA. Chechik Marsha Univ Toronto Toronto ON M5S 1A1 Canada. |
| Subject | Computer Science ; Science & Technology - Other Topics |
| Sponsorship | NSERC; OGS; IBM |
| Language | 英语 |
| Content Type | 期刊论文 |
| URI | http://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. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment