Working Seminar on Formal Models, Discrete Structures, and Algorithms

From PSL to Transition-based Generalized Büchi Automata

Alexandre Duret-Lutz (EPITA Research and Development Laboratory)

When: May 14, 2pm

Where: room G2.91b


Couvreur [FM'99] has introduced a simple yet efficient algorithm to translate LTL formulas into Generalized Büchi Automata with Transition-based acceptance (TGBA), based on a tableau construction. These TGBA can then be used directly for model checking.

We show how to extend this algorithm to create TGBA from formulas expressed in the linear fragment of PSL, which basically are LTL formulas over regular expressions. Translating PSL formulas is typically done using alternating-automata (not 1-weak, as in the case of LTL). Here we mix some ideas of the Miyano-Hayashi construction for alternation removal with the tableau construction of Couvreur, in order to avoid constructing an alternating-automaton.