Go backward to The Rules of Simple Temporal Logic Go up to Top Go forward to Additional Rules

The Basic Rules of TLA

• TLA1.

  P and (f = f') => P'

  always P <=> P and always [P => P']f

• TLA2.

  P and <A>f => Q and [A]g

  always P and always <A>f => always Q and always [A]g

Additional Rules

• INV1.

  I and [A]f => I'

  I and always [A]f => always I

• INV2.

  |- always I => (always [A]f <=> always [A and I and I']f)

• WF1.

  P and [A]f => (P' or Q') P and <A and A>f => Q' P => Enabled <A>f

  always [A]f and WFf(A) => (P |-> Q)