ABD - PSL Temporal Layer Operators

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.