psl2ba

Translator from property specification language (PSL) formulas to Büchi automata.

What is it?

The psl2ba tool translates formulas of the IEEE standard "Property Specification Language" (PSL) into Büchi automata. These automata are used in the model checkers NuSMV, SMV, or SPIN.

Features

  • The translator supports the linear-time logics LTL and PSL with past operators.
  • The output of psl2ba can be used in the symblic model checker NuSMV.

For further information see the README.TXT file in the package.