Dear Spot team,
Thanks for developing the nice tool Spot. I am a researcher at National University of Singapore using Spot in my research.
I have a question about translating LTL to buechi automata using spot.
My LTL properties are constraints over input/output sequences of a program, e.g.,
output W, output P always responds to input B (false R (! iB | (true U (oW & X (true U oP))))) where iB indicates that input B and oP indicates output P.
The buechi automata of the negation of above formula given by Spot is in the following: [image: image.png]
Here is a input/output trace to be evaluated: iH oZ iH oR iC oR iH oX iC oR iH oX iD oZ iJ oT iD oT iF oR iH oP iH oR iH oP iH oR iH oP iH oR iH oP iH oR iH oP iH oR iH oP iH oR iH oP iH
*What I do not understand is that the proposition on the transition from state 0 to state 2 is iB & oW. How can I interpret it?*
Given the input/output trace, there is no element that is iB and at the same time is oW. I assume the verification feeds element in the trace to the automata one by one.
Do I miss something e.g., wrong configuration on the translation or some basic knowledge about verification? Can you give me some advice on this issue?
Thank you very much.
Best regards Zhen
Dear Zhen,
On Thu, Sep 24, 2020 at 8:58 AM Zhen Dong zhen.dong@comp.nus.edu.sg wrote:
What I do not understand is that the proposition on the transition from state 0 to state 2 is iB & oW. How can I interpret it?
Spot uses LTL over atomic propositions, not letters. It thinks of iH, oZ, iH, oR, etc. as electric signals, or system properties, but not letters. At each step of the execution of the system, each signal is either true or false: they are not mutually exclusive. The iB&oW transition should be used when both signals are true.
In the case where you want iH, oZ, iH, oR, etc. to be interpreted as mutually exclusive events, you could encode this constraint into the formula. Spot has some tools to automate this, although it requires some manual work:
1. Add the mutually exclusive constraint to the formula:
% ltlfilt -f '(0 R(!iB|(1 U (oW&X(1 U oP)))))' --exclusive-ap=iB,oW,oP (0 R(!iB|(1 U (oW&X(1 U oP)))))&G(!(iB&oW)&!(iB&oP)&!(oP&oW))
2. Convert it into Büchi, and then (optionally) simplify the labels of the resulting automaton by removing unnecessary checks.
% ltl2tgba -B '(0 R(!iB|(1 U (oW&X(1 U oP)))))&G(!(iB&oW)&!(iB&oP)&!(oP&oW))' | autfilt -B --exclusive-ap=iB,oW,oP --simplify-exclusive-ap
this gives the attached automaton, which I hope will will more natural for your use case.
For more information about those two steps, you can look at https://www.lrde.epita.fr/~adl/dl/adl/blahoudek.15.spin.pdf The first step of the above example corresponds to r_κ() and the second to ls().
Dear Alexandre,
Thank you very much for the prompt reply. Your solution works well!
Best regards Zhen
On Thu, Sep 24, 2020 at 3:44 PM Alexandre Duret-Lutz adl@lrde.epita.fr wrote:
Dear Zhen,
On Thu, Sep 24, 2020 at 8:58 AM Zhen Dong zhen.dong@comp.nus.edu.sg wrote:
What I do not understand is that the proposition on the transition from
state 0 to state 2 is iB & oW. How can I interpret it?
Spot uses LTL over atomic propositions, not letters. It thinks of iH, oZ, iH, oR, etc. as electric signals, or system properties, but not letters. At each step of the execution of the system, each signal is either true or false: they are not mutually exclusive. The iB&oW transition should be used when both signals are true.
In the case where you want iH, oZ, iH, oR, etc. to be interpreted as mutually exclusive events, you could encode this constraint into the formula. Spot has some tools to automate this, although it requires some manual work:
- Add the mutually exclusive constraint to the formula:
% ltlfilt -f '(0 R(!iB|(1 U (oW&X(1 U oP)))))' --exclusive-ap=iB,oW,oP (0 R(!iB|(1 U (oW&X(1 U oP)))))&G(!(iB&oW)&!(iB&oP)&!(oP&oW))
- Convert it into Büchi, and then (optionally) simplify the labels of
the resulting automaton by removing unnecessary checks.
% ltl2tgba -B '(0 R(!iB|(1 U (oW&X(1 U oP)))))&G(!(iB&oW)&!(iB&oP)&!(oP&oW))' | autfilt -B --exclusive-ap=iB,oW,oP --simplify-exclusive-ap
this gives the attached automaton, which I hope will will more natural for your use case.
For more information about those two steps, you can look at https://www.lrde.epita.fr/~adl/dl/adl/blahoudek.15.spin.pdf The first step of the above example corresponds to r_κ() and the second to ls().
-- Alexandre Duret-Lutz
-
Alexandre Duret-Lutz -
Zhen Dong