CODEWITHSUNDEEP
model-checking
frogEye
frogEye

Reputation: 364

Language supported by LTL

ltl p {(Xq) || (Fp)},

what will be the formal language accepted of this LTL formula?

For example : ltl p { p && (Xq)}

{w = a0a1a2.... | p∈a0 && q∈a1}

Upvotes: 1

Views: 123

Answers (1)

Patrick Trentin
Patrick Trentin

Reputation: 7342

The property X q || F p accepts words of the language

{ w = w0w1w2... | q ∈ w1 or ∃wi. p ∈ wi }

Another way to look at the accepted language is to draw the Buchi Automaton corresponding to the LTL formula X q || F p:

buchi automaton

Credits: image generated with ltl2ba

Upvotes: 1

Related Questions