## Paper: A modal process logic (at LICS 1988)

**Kim G. 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 G. Larsen and Bent Thomsen}, title = {A modal process logic}, booktitle = {Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science (LICS 1988)}, year = {1988}, month = {July}, pages = {203--210}, location = {Edinburgh, Scotland, UK}, publisher = {IEEE Computer Society Press} }