In this paper we consider techniques to identify and remove redundant predicates during predicate abstraction. We give three criteria for identifying redundancy. A predicate is redundant if any of the following three holds (i) the predicate is equivalent to a prepositional function of other predicates, (ii) removing the predicate preserves safety properties satisfied by the abstract model (iii) removing it preserves bisimulation equivalence. We also show how to efficiently remove the redundant predicates once they are identified. Experimental results are included to demonstrate the effectiveness of our methods. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Clarke, E., Grumberg, O., Talupur, M., & Wang, D. (2003). Making predicate abstraction efficient: How to eliminate redundant predicates. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2725, 126–140. https://doi.org/10.1007/978-3-540-45069-6_14
Mendeley helps you to discover research relevant for your work.