Logic in Computer Science (LICS 1988)

Paper: A modal process logic (at LICS 1988)

Authors: Kim Guldstrand Larsen Bent Thomsen

Abstract

A novel logic is introduced for the introduction of nondeterministic and concurrent processes expressed in a process algebra. For a process algebra to be useful as a process language, it must possess compositionality, i.e. it should be possible to decompose the problem of correctness for a combined system with respect to a given specification of similar and simpler correctness problems for the components of the system. The logic presented allows such specifications to be expressed. It is an extension of process algebra in the sense that process constructs are included as connectives in the logic. Moreover, the formulas of the logic are given an operational interpretation based on which a refinement ordering between formulas is defined

BibTeX

  @InProceedings{LarsenThomsen-Amodalprocesslogic,
    author = 	 {Kim Guldstrand Larsen and Bent Thomsen},
    title = 	 {A modal process logic},
    booktitle =  {Proceedings of the Third Annual IEEE Symp. on Logic in Computer Science, {LICS} 1988},
    year =	 1988,
    editor =	 {Yuri Gurevich},
    month =	 {July}, 
    pages =      {203--210},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}
  }