Browse by author
Lookup NU author(s): Dr Stephen Paynter
Full text for this publication is not currently held within this repository. Alternative links are provided below where available.
This paper redefines RTL within classical many-sorted logic with natural number and real arithmetic. In doing so, RTL is generalised in a number of ways. In particular, functionality is handled through the use of timed variables. Various models of time for RTL are discussed, and it is argued that, providing events satisfy a countable occurrence property, time in RTL can be continuous. A number of useful RTL theorems are stated, and it is shown that RTL can naturally express all the usual temporal requirements that are placed on real-time systems. RTL is compared with other timed logics.
Author(s): Paynter SE
Editor(s): Oliveira, J.N., Zave, P.
Publication type: Conference Proceedings (inc. Abstract)
Publication status: Published
Conference Name: FME 2001: Formal Methods for Increasing Software Productivity
Year of Conference: 2001
Pages: 300-317
ISSN: 0302-9743 (Print) 1611-3349 (Online)
Publisher: Springer
URL: http://dx.doi.org/10.1007/3-540-45251-6_17
DOI: 10.1007/3-540-45251-6_17
Library holdings: Search Newcastle University Library for this item
Series Title: Lecture Notes in Computer Science
ISBN: 9783540417910
