|
Abstract : |
Abstract. This paper investigates the use of abstract-interpretationinspired techniques for improving the performance of procedures for determining when systems satisfy formulas in branching-time temporal logic. A framework for abstracting system descriptions is developed, and a particular method for generating abstract systems from given abstractions on system states is defined and shown to be both safe and optimal, in the sense that concrete systems satisfy all the temporal formulas enjoyed by their abstracted counterparts. One may then use a model checker on an abstracted (and hence smaller) system in order to infer properties of a concrete system. 1, |
