Using the Temporal Logic RDL for Design Specifications

In summary, RDL is an intuitionistic temporal logic for the specification of requirements and design of time-dependent systems. Coverage of RDL includes a backward chaining theorem prover for constructing a design from a requirement, and an execution mechanism for constructing a model of the design such that the model can be checked to satisfy the requirement at each point. A brief overview of executable temporal logic is presented together with a discussion of the advantages of an intuitionistic version. RDL is being developed as a formalism that would be appropriate for AI-based design supportin engineering.

• Type: Conference
• Year: 1989
• Where: CONCUR
• Authors: Dov M. Gabbay, Ian M. Hodkinson, Anthony Hunter
• Keywords: Chaining Theorem Prover, CONCUR 1989, Distributed And Parallel Computing, Executable Temporal Logic, Intuitionistic Temporal Logic