[SPOT Question] Little Question about LTL/PSL Fragment
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
Hi Willy, On Mon, Sep 5, 2016 at 4:56 PM, Willy Chang <r03725007@ntu.edu.tw> wrote:
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?
ltl2tgba -D formula will *prefer* deterministic output whenever possible, but does not offer any guarantee about the determinism of the output (even when a deterministic TGBA exists, as in your case). If you really insist on a deterministic output, you could allow ltl2tgba to use any acceptance condition: ltl2tgba -G -D formula on your example formula, that would produce a 5-state deterministic automaton with parity acceptance. This is not optimal, since a 3-state deterministic Büchi automaton exists for this formula (you can obtain it using the SAT-based minimization techniques presented on the website if you are curious). (There is no equivalent for the -G option on the on-line page; rewriting this page the use an interface similar to the command-line tool has been on a TODO list for a while.)
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?
Not all PSL can be converted to LTL, so the translator has to be aware of PSL operators anyway. One reason Spot translates some patterns to LTL is that is has a lot of simplification rules for LTL that may help. Unfortunately, I have not yet published the technique I use to translate PSL into TGBA, so you haven't really missed anything.
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.
Since Goal has past operator and support for alternating automata, I think you could go with http://www.daxc.de/eth/paper/10acta.pdf Also, if you are about to add a syntax for PSL in Goal, be aware that I made a mistake in Spot. As mentioned in the last paragraph of section 2.6.1 of https://spot.lrde.epita.fr/tl.pdf, the semantic for {SERE} used in Spot is the semantic of cl(SERE) used by Dax et al. For some reason when I implemented the PSL operator I thought their cl() operator was one of the PSL standard. However I plan to correct that in the future so that the present {SERE} operator will be written cl(SERE), so that I can introduce the real semantic for {SERE}. Then we will have cl(SERE) = {SERE} | {SERE}!. But that's messy. Best regards,
participants (2)
-
Alexandre Duret-Lutz -
Willy Chang