MULTICYCLES AND RTL LOGIC SATISFIABILITY

The Jahanian-Mok semidecision procedure for safety analysis of timing properties can be expressed in RTL (Real-Time Logic). We improve this procedure by unifying variables and terms containing a Skolem function. In order to guarantee termination of the potentially infinite process, we introduce the notion of a multicycle, that represents an infinite number of cycles. When the class contains at least one positive cycle, the resolution algorithm operates through the multicycle only a finite number of times. The result is an algorithm that applies to a larger class of there exists for-all-formulas and operates with the same efficiency as the Jahanian-Mok procedure.