MOP 2.0 Future Time Linear Temporal Logic (FTLTL) Plugin
From FSL
 |
|
 |
|||||
|---|---|---|---|---|---|---|---|
FTLTL |
... | ||||||
| ... | |||||||
| ... | ... | ... | ... | ||||
| ... | ... | ... | ... | ... | ... | ... | ... |
| 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.
