Induction in the timed interval calculus

Wabenhorst, Alex (2003) Induction in the timed interval calculus. Theoretical Computer Science, 300 1-3: 181-207. doi:10.1016/S0304-3975(01)00378-4


Author Wabenhorst, Alex
Title Induction in the timed interval calculus
Journal name Theoretical Computer Science   Check publisher's open access policy
ISSN 0304-3975
Publication date 2003-05-07
Sub-type Article (original research)
DOI 10.1016/S0304-3975(01)00378-4
Volume 300
Issue 1-3
Start page 181
End page 207
Total pages 27
Editor M. Nivat
G. Ausiello
M. Mislove
Place of publication The Netherlands
Publisher Elsevier
Collection year 2003
Language eng
Subject C1
280402 Mathematical Logic and Formal Languages
700199 Computer software and services not elsewhere classified
Abstract The Timed Interval Calculus, a timed-trace formalism based on set theory, is introduced. It is extended with an induction law and a unit for concatenation, which facilitates the proof of properties over trace histories. The effectiveness of the extended Timed Interval Calculus is demonstrated via a benchmark case study, the mine pump. Specifically, a safety property relating to the operation of a mine shaft is proved, based on an implementation of the mine pump and assumptions about the environment of the mine. (C) 2002 Elsevier Science B.V. All rights reserved.
Keyword Computer Science, Theory & Methods
Real-time Specification And Reasoning
Interval Logic
Temporal Logic
Induction
Timed Traces
Specification
Refinement
Q-Index Code C1

Document type: Journal Article
Sub-type: Article (original research)
Collections: 2004 Higher Education Research Data Collection
School of Information Technology and Electrical Engineering Publications
 
Versions
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 1 times in Thomson Reuters Web of Science Article | Citations
Scopus Citation Count Cited 1 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Wed, 15 Aug 2007, 01:45:33 EST