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 pmeredit@cs.uiuc.edu
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.