Converting a TGBA into a PSL formula
The ForSpec Temporal Logic: A New Temporal Property-Specification Language gives a conversion from Büchi automata to PSL.
Here is my reinterpretation of their theorem.
Any omega regular language can be converted into a finite union of
the form $L_1.L_2$ where $L_1$ is a regular language, and $L_2$ can
be described by a deterministic automaton. An expression e
for $L_1$ can be computed easily using the classical state-elimination algorithm, so $L_1.L_2$ can be encoded by {e}!<>->f
where f
is a formula for $L_2$.
$L_2$ can be represented by disjunctions of the formulae of the form {e1;e2[*]}! && {e1;e2[*]}[]=> {e2[*]}!
where e1
is a word going to an accepting state, and e2[*]
is the loop language of that state (i.e., the language of all words that will come back to this state).
Running this construction on the Büchi automaton we produce for FGa
will give {1*;a}<>-> ({a;a*}! & {a;a*}[]=>{a*}!)
. The negation of this formula, on translated to TGBA and reduced by simulation, will give exactly the TGBA we want for GFa
.
The above algorithm works with Büchi automata as input. The
resulting formula would be translated to a TBA (i.e., a
transition-based non-generalized Büchi automaton) because in the
current PSL translation <>->
and {...}!
are all translated with
the same unique acceptance condition (this probably makes
complementation of Büchi automata via PSL uninteresting).
- Can we find a translation from TGBA to PSL that will work with transition-based generalized acceptance?
- Can we find a translation to PSL to relies on the
GF
operators instead pf[]=>
? The idea is that these would add generalized conditions, so that we obtain a TGBA when translating the formula back automata.