Linear temporal logic and Z refinement

DOI10.1007/978-3-540-27815-3_13MaRDI QIDQ5312975zbMATH OpenOpenAlexFDO

Authors John Derrick, Graeme Smith

Publication date 25 August 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b98770

zbMATH Keywords

LTLrefinementtemporal logicZ

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Temporal-logic property preservation under Z refinement
• scientific article; zbMATH DE number 6287569
• Intuitionistic linear temporal logics
• scientific article; zbMATH DE number 1059327
• Linear time temporal logics over Mazurkiewicz traces
• Linear temporal logic and finite semigroups
• The axiomatization of propositional linear time temporal logic
• Linear temporal logic -- from infinite to finite horizon
• Defeasible linear temporal logic
• Encoding temporal logics in executable Z: A case study for the ZETA system

Cited in

(5)

• Temporal-logic property preservation under Z refinement
• Property transformation under specification change
• Resets vs. aborts in linear temporal logic
• Proving temporal properties of Z specifications using abstraction
• Invariant-driven specifications in Maude

This page was built for publication: Linear temporal logic and Z refinement

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5312975)