add support for EQLTL
Read Stutter-Invariant Languages, ω-Automata, and Temporal-Logic.
A basic plan would be:
-
Add an ∃ unary operator -
modify the LTL parser to accept ∃ only at the top-level. -
add a function label_filter(tgba_digraph_ptr& aut, bdd vars)
that removes all variables invars
from the labels ofaut
. -
Adjust the translations. To translate ∃(a,b) f(a,b,c,d)
, first translatef(a,b,c,d)
, and then applylabel_filter
to removea
, andb
. (Note in Couvreur/FM, removinga,b
could be done during the same pass that complements promises.) -
Implement Etessami's conversion from BA to EQLTL. -
Implement a conversion from TGBA to EQLTL.
A more general idea would be to allow ∃ at all level in the
formulas, during the translation, we have to apply bdd_exist
on
the BDD-rewriting of any subformula of a ∃ operator.
Would it be correct to do the same with ∀ and bdd_forall
? If that is true, that gives us a conceptually simple way to negate an automaton: translate it to EQLTL, negate it (giving an ∀-quantified LTL formula), and translate it back.