Paper: Temporal Linear Logic Specifications for Concurrent Processes (at LICS 1997)

Authors: Max I. Kanovich Takayasu Ito

Abstract

The aim of the paper is to develop comprehensive logical systems capable of handling both resource-sensitive and time-dependent properties of concurrent processes. As a language for specifying such properties, we introduce 'temporal linear logic' (TLL), an extension of linear logic with certain features of temporal logic. A semantic setting for TLL is given in terms of 'time-state universes'. TLL is proved to be fully adequate for 'time-state' concurrency models.

BibTeX

  @InProceedings{KanovichIto-TemporalLinearLogic,
    author = 	 {Max I. Kanovich and Takayasu Ito},
    title = 	 {Temporal Linear Logic Specifications for Concurrent Processes},
    booktitle =  {Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science (LICS 1997)},
    year =	 {1997},
    month =	 {June}, 
    pages =      {48--57},
    location =   {Warsaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }