## 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.