LTLPlugin4

LTL plugin for MOP allows one to synthesize monitors from linear temporal logic (LTL) descriptions. The LTL plugin supports both past and future time linear temporal logic operators. The past time operators in LTL differ from those in PTLTL, however, in that the operators in PTLTL use a ``sliding time window" semantics, i.e. they are evaluated for each temporal state of a given system, while those of LTL are evaluated essentially only for the initial state (e.g., (*) X will always fail because there is no past in the initial state of a system, essentially past time operators must be nested within future time operators to be of any use).