MOP 2.0 Future Time Linear Temporal Logic (FTLTL) Plugin

Jump to: navigation, search


Private:MOP Languages MatrixMOP Languages

MOP

Private:MOP Logic Repository MatrixMOP 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.



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:
  • Complex
  • Grant
  • HashSet
  • TrafficLight
  • a a* b b* c c* d
 

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.

Personal tools
Namespaces

Variants
Views
Actions
Navigation