Hi,
I am using
spot.from_ltlf().translate()
to translate LTL rules into a finite automata (with alive property). Now I want to verify
certain words that whether they are accepted by the automata or not. These words will be
generated from a powerset of the set of atomic propositions. Lets suppose I have AP =
{a,b,c,d}. How do I generate words from the powerset of AP and verify it on the automata.
Should the word always contain a cycle and a prefix part. If yes, what should be the cycle
part and what should be the prefix part.
I will be waiting for your response.
Thanks and Regards,
Hashim Ali
Research Assistant
Laboratory for Cyber-Physical Networks and Systems (Cyphynets)
Lahore University of Management Sciences (LUMS)