MOP 2.0 Future Time Linear Temporal Logic (FTLTL) Plugin
|MOP Matrix: a clickable map of MOP pages.|
This page discusses the MOP future-time linear temporal logic (FTLTL) plugin. It also allows to type in an FTLTL specification and then generate a monitor for it. FTLTL is a logic for specifying properties of reactive and concurrent systems. FTLTL provides temporal operators that refer to the future states of an execution trace relative to a current point of reference. The logic plugin here is based on a rewriting-based algorithm for generating an optimized monitoring program from an FTLTL formula.
Note: if there are any technical difficulties please alert firstname.lastname@example.org
Please press the Run button once and wait; it may take a few seconds to run FTLTLPlugin2.0; the execution of FTLTLPlugin2.0 using this web interface is limited to 2 minutes of CPU time and 500 MB of RAM.