# PTLTLPlugin4

From FSL

PTLTL plugin for MOP allows one to synthesize monitors from from past time linear temporal logic (PTLTL) descriptions. The generated monitors are based on a series of assignments to array elements, one element for each temporal operator in the formula. From these array assignments a static finite state machine is generated for monitoring purposes (the finite state machine is slightly more efficient than array assignments, and it eases the generation of enable sets, which are explained in detail in Efficient_Formalism-Independent_Monitoring_of_Parametric_Properties).