Abstract
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 support in engineering.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Abadi M, Lamport L & Wolper P (1989) Realizable and unrealizable specification of reactive systems, in Ausiello G et al, Proc 16th Colloquium on Automata, Languages and Programming, LNCS 372, Springer
Barringer H, Fisher M, Gabbay D, Gough G & Owens R (1990a) MetateM: A framework for programming in temporal logic, in de Bakker J et al, REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalisms and Correctness, LNCS 430, Springer
Barringer H, Fisher M, Gabbay D & Hunter A (1990b) Theoretical Aspects of Executing Meta-level Temporal Logic, draft paper, Department of Computing, Imperial College, London
Fitting M, (1983) Proof Methods for Modal and Intuitionistic Logics, Reidel
Gabbay D (1989) The declarative past and imperative future: Executable temporal logic for interactive systems, in Banieqbal B, Barringer H and Pneuli A (eds), Temporal Logic Specification, LNCS 398, p409–448, Springer
Gabbay D, Hodkinson I & Hunter A (1990) RDL: An executable temporal logic for the specification and design of real-time systems, Proc IEE Colloquium on Temporal Reasoning
Gabbay D & Reyle U (1984) N-PROLOG: An extension of PROLOG with hypothetical implication, 1, J. Logic Programming, 4, 319–355
Pneuli A (1977) The temporal logic of programs, in Proc. of the Eighteenth Symp. on the Foundations of Computer Science, p 46–57
Wupper H, Vytopil J, Wieczorek M, & Coesmans P (1989) A real-time systems specification language, Department of Informatics, University of Nijmegen
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gabbay, D., Hodkinson, I., Hunter, A. (1991). Using the temporal logic RDL for design specifications. In: Yonezawa, A., Ito, T. (eds) Concurrency: Theory, Language, and Architecture. CONCURRENCY 1989. Lecture Notes in Computer Science, vol 491. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53932-8_44
Download citation
DOI: https://doi.org/10.1007/3-540-53932-8_44
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53932-2
Online ISBN: 978-3-540-46452-5
eBook Packages: Springer Book Archive