Skip to content

Algorithm for the separation of LTLp formulae into a combination of pure past, present and future formulae

License

Notifications You must be signed in to change notification settings

xsk07/LTLpSeparator

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

LTLpSeparator

LTLpSeparator is a tool for the separation of LTLp formulae into a combination of pure, past, present and future formulae. The separation algorithm is based on the Gabbay' Separation Theorem. Formulae could be passed as text files or directly typed on the command line. The result can be saved as simple text file, as an image depicting the tree representation of the formula. Furthermore, LTLpSeparator can generate the corresponding separated automata set.

Prerequisites

This tool uses Graphviz for the generation of the images depicting the tree representation of formulae, hence you should first install Graphviz on your system following the instructions here. For the generation of DFAs, LTLpSeparator uses LTLf2DFA with all its dependencies, its installation instructions are available at LTLf2DFA github page.

Features

  • Syntax and parsing support for the Linear Temporal Logic with Past operators (LTLp);
  • Conversion of LTLp formulae into an equivalent form with only the temporal operators U and S;
  • Visualization of the formulae as trees;
  • Visualization of pure formulae as DFAs;
  • Generation of the separated automata set corresponding to the separated formula;

Contact

Please contact the developer, Seweryn Kaniowski, for any information, comment or bug reporting: [email protected]

About

Algorithm for the separation of LTLp formulae into a combination of pure past, present and future formulae

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published