Proving Possibility Properties

A method is described for proving “always possibly” properties of specifications in formalisms with linear-time trace semantics. It is shown to be relatively complete for TLA (Temporal Logic of Actions) specifications. Key words: Branching time, linear time, temporal logic.

• Type: Journal
• Year: 1998
• Where: TCS
• Authors: Leslie Lamport
• Keywords: Key Words, Linear-time Trace Semantics, TCS 1998, Temporal Logic, Theoretical Computer Science