PV2 ⊧ MLTLconvertergiven a MLTL formula, generate an equivalent in another LTL dialect to be used with an external solver

Converts Mission-time LTL (MLTL) to either LTL, $LT{L}_f$ (LTL over finite traces), SMV or SMT

Application domain/field

• Satisfiability checking
• Mission-time LTL
• MLTL satisfiability checking

Type of tool

Translator

Expected input

MLTL formula and a converter flag. The converter flag indicates whether it should be translated to LTL, $LT{L}_f$, SMV or SMT-LIB v2.

Expected output

Reports whether the MLTL formula is satisfiable or not.

Internals

Uses aalta (LTL solver), aaltaf ($LT{L}_f$ solver), nuXmv (SMV model checker), Z3 (SMT solver). These tools are used to check the satisfiability of the input MLTL formula and their encodings.

Comments

They tested the different translations and it seemed that the SMT-based approach tends to perform best for satisfiability checking. They advise to use MLTL-SAT via KLIVE for satisfiability checking of MLTL formulas with interval ranges less than 100.