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)
Hi Hashim On Mon, Mar 25, 2019 at 1:25 PM hashim ali <hashim_ali94@outlook.com> wrote:
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.
Because of from_ltlf(). I believe you are talking about finite words.
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.
I do not understand what this means.
Should the word always contain a cycle and a prefix part.
Spot only deals with infinite words that are lasso-shaped. [*] The cycle part is mandatory, the prefix is not. If you want to compare some finite words against Büchi automata generated from the output of from_ltlf(), you should convert your finite words to use the same convention as in the output of from_ltlf(): put your finite words as a prefix where "alive" should also always hold, and add a cycle with !"alive". E.g. over AP={a,b}, the finite word a&b;a&!b would be encoded as the infinite word a&b&alive;a&!b&alive;cycle{!alive}. [*] In fact, because the twa_word object is labeled by Boolean formulas (and not just conjunctions of litterals), it can actually represent more than one word; it's more like a set of words with the same shape. Or a restriction of an automaton to some lasso shape if you prefer.
Hi, Thank you for writing back. I am doing exactly like this. I append cycle{!alive} to my finite word before parsing it to an automaton. but I don't know what should be the length of my prefix i.e. how many steps it should have. I guess its more of a theoretical question, so can you direct me to some source where I can read on this. For example, if I have a one state automaton my prefix would have only one step e.g. a&b and for two state automaton it may have two steps like this a&b ; a&!b. Is there any method that I can calculate the number of steps. Thanks and Regards, Hashim Ali Research Assistant Laboratory for Cyber-Physical Networks and Systems (Cyphynets) Lahore University of Management Sciences (LUMS) ________________________________ From: Alexandre Duret-Lutz <adl@lrde.epita.fr> Sent: 26 March 2019 20:33 To: hashim ali Cc: spot@lrde.epita.fr Subject: Re: [Spot] Generate Words for verification Hi Hashim On Mon, Mar 25, 2019 at 1:25 PM hashim ali <hashim_ali94@outlook.com> wrote:
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.
Because of from_ltlf(). I believe you are talking about finite words.
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.
I do not understand what this means.
Should the word always contain a cycle and a prefix part.
Spot only deals with infinite words that are lasso-shaped. [*] The cycle part is mandatory, the prefix is not. If you want to compare some finite words against Büchi automata generated from the output of from_ltlf(), you should convert your finite words to use the same convention as in the output of from_ltlf(): put your finite words as a prefix where "alive" should also always hold, and add a cycle with !"alive". E.g. over AP={a,b}, the finite word a&b;a&!b would be encoded as the infinite word a&b&alive;a&!b&alive;cycle{!alive}. [*] In fact, because the twa_word object is labeled by Boolean formulas (and not just conjunctions of litterals), it can actually represent more than one word; it's more like a set of words with the same shape. Or a restriction of an automaton to some lasso shape if you prefer.
On Wed, Mar 27, 2019 at 7:46 AM hashim ali <hashim_ali94@outlook.com> wrote:
Hi, Thank you for writing back. I am doing exactly like this. I append cycle{!alive} to my finite word before parsing it to an automaton. but I don't know what should be the length of my prefix i.e. how many steps it should have. I guess its more of a theoretical question, so can you direct me to some source where I can read on this.
For example, if I have a one state automaton my prefix would have only one step e.g. a&b and for two state automaton it may have two steps like this a&b ; a&!b. Is there any method that I can calculate the number of steps.
Why do you assume that such a bound exists? If your automaton has any cycle in the alive part it will recognize words that are arbitrary large. -- Alexandre Duret-Lutz
Then, How can I generate word prefixes from the power-set of AP which are arbitrarily large? Also, it may not be necessary that there is a cycle in the alive part (prefix). the prefix may has two or more steps and then I append cycle{!alive} and then parse it to the automaton. Thanks and Regards, Hashim Ali Research Assistant Laboratory for Cyber-Physical Networks and Systems (Cyphynets) Lahore University of Management Sciences (LUMS) ________________________________ From: Alexandre Duret-Lutz <adl@lrde.epita.fr> Sent: 27 March 2019 14:30 To: hashim ali Cc: spot@lrde.epita.fr Subject: Re: [Spot] Generate Words for verification On Wed, Mar 27, 2019 at 7:46 AM hashim ali <hashim_ali94@outlook.com> wrote:
Hi, Thank you for writing back. I am doing exactly like this. I append cycle{!alive} to my finite word before parsing it to an automaton. but I don't know what should be the length of my prefix i.e. how many steps it should have. I guess its more of a theoretical question, so can you direct me to some source where I can read on this.
For example, if I have a one state automaton my prefix would have only one step e.g. a&b and for two state automaton it may have two steps like this a&b ; a&!b. Is there any method that I can calculate the number of steps.
Why do you assume that such a bound exists? If your automaton has any cycle in the alive part it will recognize words that are arbitrary large. -- Alexandre Duret-Lutz
participants (2)
-
Alexandre Duret-Lutz -
hashim ali