The full details are in the HOL script files below. These are the current working version at Cambridge. Every so often I check consistent versions into the SourceForge repository.

- Definition of Kripke structures

- Definition of finite paths (lists)

- Definition of infinite paths

- Definition of abstract syntax

- Definition of unclocked semantics

- Definition of clocked semantics

- Definition of rewrites

- Theorems proved about PSL semantics

MICHAEL J. C. GORDON

University of Cambridge

Computer Laboratory

Room FE19

William Gates Building

JJ Thomson Avenue

Cambridge CB3 0FD

United Kingdom

work phone: +44 1223 334627

work fax: +44 1223 334678

email: