add support for EQLTL
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 in
varsfrom the labels of
Adjust the translations. To translate
∃(a,b) f(a,b,c,d), first translate
f(a,b,c,d), and then apply
b. (Note in Couvreur/FM, removing
a,bcould 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
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.