Logic in Computer Science (LICS 1997)

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

Authors: Max 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 Kanovich and Takayasu Ito},
    title = 	 {Temporal Linear Logic Specifications for Concurrent Processes},
    booktitle =  {Proceedings of the Twelfth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1997},
    year =	 1997,
    editor =	 {Glynn Winskel},
    month =	 {June}, 
    pages =      {48--57},
    location =   {Warsaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }