MOP 2.1 Future Time Linear Temporal Logic (FTLTL) Plugin

Jump to: navigation, search


MOP LanguagesMOP Languages

MOP

Special:LogicRepository2.1MOP LogicRepository

FSM

ERE

CFG

PTLTL

FTLTL

PTCaRet

...

JavaMOP

JavaFSM

JavaERE

JavaCFG

JavaPTLTL

JavaFTLTL

JavaPTCaRet

...

BusMOP

BusFSM

BusERE

...

BusPTLTL

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


Choose an example:
     

    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.

    Personal tools
    Namespaces

    Variants
    Views
    Actions
    Navigation