Temporal logics Express properties of event orderings in time Branching Time Linear Time Every moment has several Every moment has a unique successors successor Infinite tree Infinite sequences(words) Computation Tree LogIc(CTL) Linear Temporal LogIc(LTL)Temporal Logics ◼ Express properties of event orderings in time ◼ Linear Time ◼ Every moment has a unique successor ◼ Infinite sequences (words) ◼ Linear Temporal Logic (LTL) ◼ Branching Time ◼ Every moment has several successors ◼ Infinite tree ◼ Computation Tree Logic (CTL)