Algorithms related to omega regular languages.
Project description
A package for automata-theoretic and symbolic algorithms that manipulate omega-regular languages. It contains:
parser of temporal logic
translation from past to future LTL, using temporal testers
classes for enumerated and semi-symbolic automata and transition systems
class for symbolic automata that includes compiling methods that take care for initializing and maintaining the underlying BDDs via bitblasting of first-order temporal logic
flattening of semi-symbolic transition systems to LTL
