Fifth Annual IEEE Symposium on

Logic in Computer Science (LICS 1990)

Paper: A logic of concrete time intervals (at LICS 1990)

Authors: Lewis, H.R.

Abstract

A description is given of: (1) a finite-state model for asynchronous systems in which the time delays between the scheduling and occurrence of the events that cause state changes are constrained to fall between fixed numerical upper and lower time bounds; (2) a branching-time temporal logic suitable for describing the temporal and logical properties of asynchronous systems, for which the structures of (1) are the natural models; and (3) a functional verification system for asynchronous circuits which generates, from a Boolean circuit with general feedback and specified min/max rise and fall times for the gates, a finite-state structure as in (1), and then exhaustively checks a formal specification of that circuit in the language (2) against that finite-state model

BibTeX

  @InProceedings{Lewis-Alogicofconcretetim,
    author = 	 {Lewis, H.R.},
    title = 	 {A logic of concrete time intervals},
    booktitle =  {Proceedings of the Fifth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1990},
    year =	 1990,
    editor =	 {John Mitchell},
    month =	 {June}, 
    pages =      {380--389},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }