
25 Mar
2019
25 Mar
'19
1:24 p.m.
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)