A toolbox with code for context free grammar verificiation for logical formulas

I work with Linear Temporal Logic (LTL) formulas. I am looking for a toolbox to verify if an LTL formula can satisfy a given Context-Free Grammar (CFG).

For example, we have the LTL formula G(x_10). In that LTL formula, G is the temporal operator always (or globally), and x_1 is the first mode of a finite trajectory of binary values.

For example, x:=1,0,1; 1,1,1; 1,1,0. This trajectory satisfies G(x_10) because x_1 (the first mode) is alsway true (the first mode is always 1).

My question is if there is any toolbox with code where we can give a logical formula (LTL formula in my case) and a CFG to check whether the formula satisfies the CFG?

Any help is greatly appreciated!