Constraint oriented temporal logic specification

Abstract

We present a partial solution to the Dagstuhl RPC-Memory Specification Problem which is carried out in linear-time temporal logic (LTL). Our language is quite similar to TLA (Temporal Logic of Actions) by Lamport. However, our use of this language provides some (in our opinion) interesting novelties. A major contribution of this paper is in our opinion a demonstration of different structuring mechanisms that exist in LTL. We use flexible predicates to represent synchronizing events, as in e.g., LOTOS, that serve for communication between components. In the specification of a component, the central part is a set of formulas that for each state variable states the constraints under which it may change, and for each event states the constraints (in terms of state changes) under which it may occur. We define a graphical syntax for parts of a temporal logic specification that involve “control”.

This contribution contains solutions to the specification problems, except for the timing extension, i.e., we solve Problem 1, 2 and 3 except for the verification parts which is only briefly covered.