A sample of QPTL formulae to Büchi automata translation.
A sample of QPTL formulae to Büchi automata translation.

Step-by-Step Translation (from QPTL formulae to Büchi automata)

This function translates in steps a QPTL formula into a Büchi automaton. The translation algorithm combines an adaptation of the tableau construction described in [Manna and Pnueli, Temporal Verification of Reactive Systems, Springer, 1995] and the approach described in [Sistla, Vardi, and Wolper, TCS, 49:217-237, 1987] for quantification handling. The translation includes 4 steps:

  1. Convert the input QPTL formula into the prenex normal form. (All quantifiers are at the outer most level.)
  2. Translate the PTL formula inside quantifiers into a generalized Büchi automaton.
  3. Convert the generalized Büchi automaton into an equivalent Büchi automaton.
  4. Finally, process all quantifiers (by projection, complementation, etc.) to obtain the final result.