Generating Oracles From Your Favorite Temporal Specifications

The paper describes a generic tableau algorithm, which is the basis for ageneral customizable method for producing oracles from temporal logicspecifications. A generic argument gives semantic rules with which to buildthe semantic tableau for a specification. Parameterizing the tableau algorithmby semantic rules permits it to easily accommodate a variety of temporaloperators and provides a clean mechanism for fine-tuning the algorithm toproduce efficient oracles.The paper develops conditions that ensure a set of rules results in a correcttableau procedure. It gives sample rules for a variety of linear-time temporaloperators and shows how rules are tailored to reduce the size of an oracle. Toillustrate the versatility of this method, its application to a high levelinterval logic is discussed.