The module on regular languages supports three flavors of models: Finite State Automata (deterministic, non-deterministic, on finite or on infinite words), regular expressions and linear temporal logic. Use the links below to learn more about their syntax or the analysis methods supported by the CMWB.