# PTLTL Monitoring Algorithm2.1

From FSL

Finite state machines are generated from the PTLTL specification using a state reachability algorithm. To monitor the finite state machine the normal finite state machine monitoring algorithm is used. Because not all events of interest are necessarily used in a PTLTL formula, there is a default transition in every FSM state.