An expressive temporal logic for basic LOTOS

A temporal semantics far Basic LOTOS, i.e. LOTOS without value passing, is presented. The semantics is provided using a compositional approach by which it is possible to associate temporal logic formulae to each language construct. The relationships between this semantics and the operational semantics of the language have been studied in detail, showing the expressiveness of the logic with respect to the operational semantics modulo luce equivalence. The capability of the given semantics to be used to verify interesting properties of programs is also investigated, and a study for more expressive semantics is discussed.