Linear Temporal Logic and Z Refinement

Speaker: John Derrick (University of Kent)

When: 2:00, Tuesday, 12 October 2004

Venue: 78-420

Since Z, being a state-based language, describes a system in terms of its state and potential state changes, it is natural to want to describe properties of a specified system also in terms of its state. One means of doing this is to use Linear Temporal Logic (LTL) in which properties about the state of a system over time can be captured. This, however, raises the question of whether these properties are preserved under refinement. Refinement is observation preserving and the state of a specified system is regarded as internal and, hence, non-observable.

In this paper, we investigate this issue by addressing the following questions. Given that a Z specification A is refined by a Z specification C, and that P is an LTL property which holds for A, what LTL property Q can we deduce holds for C? Furthermore, under what circumstances does the property Q preserve the intended meaning of the property P? The paper presents a general approach to answering these questions that could also be applied to other temporal logics such as CTL and the mu-calculus.

Hospitality: Graeme Smith

Contact: Phil Cook (SSE seminar co-ordinator) (philc@itee.uq.edu.au)

SSE seminar web page: http://www.itee.uq.edu.au/~sse/Seminars.html