Skip to main content

Linear temporal logic and Z refinement

Derrick, John and Smith, Graeme (2004) Linear temporal logic and Z refinement. In: Rattray, Charles and Maharaj, Savitri and Shankland, Carron, eds. Algebraic Methodology and Software Technology 10th International Conference. Lecture Notes in Computer Science . Springer, Berlin, Germany, pp. 117-131. ISBN 978-3-540-22381-8. E-ISBN 978-3-540-27815-3. (doi:10.1007/b98770) (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided) (KAR id:14126)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided.
Official URL:


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 a temporal logic property which holds for A, what temporal logic 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 answers these questions for LTL, but the approach could also be applied to other temporal logics over states such as CTL and the mu-calculus.

Item Type: Book section
DOI/Identification number: 10.1007/b98770
Uncontrolled keywords: Z refinement, temporal logic, LTL
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:02 UTC
Last Modified: 16 Nov 2021 09:52 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.