MOP 2.1 Future Time Linear Temporal Logic (FTLTL) Plugin
|MOP Matrix: a clickable map of MOP pages.|
(Note: FTLTL logic plugin is under porting to LogicRepository 2.1. It will be available soon.)
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; see links in the top-right box for details and syntax. Simply choose (and modify) one of the examples below from the list on the left, or write your own in the text box, then click Run. to see the result. If you find any bug or have any comment, please send us a message at firstname.lastname@example.org.
Please press the Run button once and wait; it may take a few seconds to run FTLTLPlugin2.1; the execution of FTLTLPlugin2.1 using this web interface is limited to 2 minutes of CPU time and 500 MB of RAM.