PSL: Further Temporal Layer Operators

(The important operators on this slide are the implications operators (first two). Other may be lectured again in TL and MC course).

PSL sequences can be combined with implication and conjunction operators in the `temporal layer'.

• { P |-> Q } P is followed by Q (one state overlapping),
• { P |=> Q } P is followed by Q (immediately afterwards),
• { P && Q } P and Q occur at once (length matching),
• { P & Q } P and Q succeed at once,
• { P within Q } P occurred at some point during Q,
• { P until Q } P held at all times until Q started,
• { P before Q } P held before Q held.