Hi Philipp,

On Sun, Nov 8, 2020 at 9:36 AM Philipp schwartz <pschwartz090@gmail.com> wrote:
> My question is, is it possible to get boolean result if LTL formula accepts or rejects a word?
> e.g. In case the LTL formula is "aUb" is it possible to check that the formula is accepting "cycle(b)"?

% ltlfilt -f 'a U b' --accept-word 'cycle{b}' -c
1
% ltlfilt -f 'a U b' --accept-word 'cycle{!b}' -c
0

Beware that since AP={a,b} are atomic propositions, cycle{b} is not a
word, but the set of words where b is always true.  The --accept-word
option matches any formula that *intersect* the given set, so it just
has to accept one word.  (The --reject-word match formulas that do not
intersect the given set, so they have to reject all words.)

As a consequence, the following should not be a surprise:

% ltlfilt -f 'a U b' --accept-word 'cycle{!a}' -c
1

This is because the word cycle{!a & b} which is one of the words
represented by cycle{!a} is accepted by 'a U b'.

Best regards
--
Alexandre Duret-Lutz