Hello,
I'm a graduate student at National Taiwan University (Taiwan), doing automatic verification related researches.
Currently I'm working on integration of PSL translation with other types of Büchi automata and formats with
our own tool (based on Java), which the linear fragment part is implemented by Spot (and ltl2tgba).
I appreciate this fantastic tool and all of your respectable work on this.
Upon using ltl2tgba, I'd like to ask some basic question regarding F formula and SERE sequences.
Take the following formula as example:
G ( {a;b} -> F q )
where a, b, q are all atomic Boolean expressions.
ltl2tgba would give me the result like the following:
https://spot.lrde.epita.fr/spotimg/af005ecb477ea78d3b55f538089ac0fce1fa99f7…
(This is captured from online Spot converter, but is the same as one output by command-line tools.)
As we can see, there are multiple transitions marked as "a & !q",
meaning this automaton is a non-deterministic one.
Is this intended to be so?
If yes, how could I specify Spot to get a deterministic output?
If no, would this be a bug or something ambiguous?
Also, I have been curious about the algorithm that Spot parses PSL fragment.
It seems like Spot first extracts PSL symbols to LTL compatible ones and then
apply LTL translation method to automata,
Is this right? Or did I miss some parts?
I'm new to PSL translations and reading related papers now (thanks for the SPOT citation page).
Please feel free to correct me or recommend me some must-read publications.
Currently I"m working on the IEEE Standard (2010) and the book Practical Introduction to PSL.
Thank you very much.
Sincerely,
Willy Chang
Dept. of Information Management
National Taiwan University
