Spot

A model checking library. Spot offers many algorithms and tools that manipulate LTL/PSL formulas and omega-automata with state-based or transition-based acceptance.