add support for EQLTL
Read StutterInvariant Languages, ωAutomata, and TemporalLogic.
A basic plan would be:
 Add an ∃ unary operator
 modify the LTL parser to accept ∃ only at the toplevel.

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 BDDrewriting 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.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information