LTLpSeparator is a tool for the separation of LTLp formulae into triples of pure past, pure present and pure future automata. It is based on Linear Temporal Logic and the Gabbay Separation Theorem. Formulae could be passed as text files or directly typed on the command line. The result can be save as a simple text file, as a tree representation image of the formula or as triples of pure past, pure present and pure future automata.

This tool uses Graphviz for the generation of formula ASTs, hence you should first install Graphviz on your system following the instructions here, and LTLf2DFA with all its dependencies for the generation of the DFAs. The instructions are available at LTLf2DFA github page.

• Syntax and parsing support for the Linear Temporal Logic with Past operators (LTLp);
• Conversion of LTLp formulae containing unary temporal operators into an equivalent form of the US temporal logic;
• Visualization of the formulae as ASTs;
• Separation of LTLp formulae into triples of pure past, pure present and pure future formulae written using the booleans and the US connectives only, it is also possible to view the list of elimination rules of the Separation Theorem applied by the algorithm, and to generate the respective triples of automata;
• Visualization of pure formulae as DFA;