MOP 1.0 Future Time Linear Temporal Logic (FTLTL) Plugin

Jump to: navigation, search


This is JavaMOP1.0, which is now deprecated. Go to JavaMOP for the current version.

  

MOP

ERE

CFG

PTLTL

FTLTL

PTCaRet

...

JavaMOP

JavaERE

JavaCFG

JavaPTLTL

JavaFTLTL

JavaPTCaRet

...

BusMOP

BusERE

...

BusPTLTL

... ... ...
... ... ... ... ... ... ...
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

Choose an example:
     

    Please press the Run button once and wait; it may take a few seconds to run FTLTLPlugin1.0; the execution of FTLTLPlugin1.0 using this web interface is limited to 2 minutes of CPU time and 500 MB of RAM.

    Personal tools
    Namespaces

    Variants
    Views
    Actions
    Navigation