Specifying Properties of Basic LOTOS Specifications Using Temporal Logic

Citation

Shankland C (1996) Specifying Properties of Basic LOTOS Specifications Using Temporal Logic. In: FORTE'95 (8th International Conference on Formal Description Techniques for Distributed Systems and Communications Protocols). FORTE'95 - 8th International Conference on Formal Description Techniques for Distributed Systems and Communications Protocols. Chapman and Hall.

Abstract
Temporal logic can be used to describe desirable properties of a system in a more abstract, less constructive manner than when using process algebra alone. This is a well researched area for other process algebras, but not so for LOTOS. This paper is an initial attempt to fill that gap by investigating the use of the modal μ-calculus with Basic LOTOS, laying the groundwork for work on Full LOTOS, i.e. including data types, and logic.

Keywords
Basic LOTOS; specification and verification; partial specification; modal μ-calculus