5 Sep
2016
5 Sep
'16
6:54 p.m.
Hi Willy,
On Mon, Sep 5, 2016 at 4:56 PM, Willy Chang <r03725007(a)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,