This module implements functions for working with automata, in particular, determinizing them by the subset and the breakpoint constructions, as well as converting omega-automata to other acceptance conditions. Automata are represented in either a fully explicit enumeration of their states and transitions, a fully symbolic representation, or a semi-symbolic one.

This module implements BDDs where nodes of the BDD refer directly to boolean expressions. To use the module, the local data structures must first be initialized with a sequence of boolean expressions using the Initialize function. The given sequence of boolean expressions determines the set of variables and the variable order by mapping the listed expressions to BDD variables (of type BDDIndex) in the given order. After that, the typical BDD functions can be used. From time to time, the user should call the GarbageCollect function to collect garbage nodes that can be reused later. Note that garbage collection resets the computed table, so garbage collection should not be called too often, otherwise performance will decrease. The order is stored in Index2BoolExpr and can be changed with the SwapVar function. If the variable order is changed, the computed table must be reset.

Functions of this model deal with the theory of equality of uninterpreted functions (EUF). To this end, reductions are provided that endow given EUF formulas with additional constraints so that the satisfiability or validity can be decided by means of a propositional SAT solver. In particular, constraints are added to ensure the congruence of functions, i.e. x1=x2 must imply f(x1)=f(x2), and the transitivity of equations. The generated assumptions are added as conjunctions asm&phi for checking the satisfiability, and as an implication asm->phi for checking the validity of an EUF formula phi.

This module implements algorithms for logic minimization

This module implements algorithms for matrices on rational numbers. To this end, it first implements a type for rational and complex numbers, and based on these, algorithms for inverting a matrix, for solving linear (in)equation systems, and for computing eigenvalues (e.g. to solve linear differential equation systems) are provided.

This module implements functions for checking the satisfiability of boolean expressions. The SAT checking procedures are based on Shannon graphs which are unreduced unordered binary decision diagrams. This has the advantage that one can construct an equivalent Shannon graph for a given BoolExpr in linear time.

The functions of this module provide translations from temporal logics to symbolically encoded omega automata. In general, these translations replace an elementary subformula (one that starts with a temporal operator) by a new state variable of the automaton and according state transitions and contraints so that the new state variable becomes equivalent to the elementary subformula it abbreviates. To this end, one usually makes use of GF-constraints which however are harder to check than others. They cannot always be avoided, but the translators presented here may try to use F-constraints whenever possible which then usually generates a cascade of F-constraints, i.e. formulas of the following form where phi is propositional: CF ::= F phi | F(phi&CF) | X CF | CF & CF. The use of F or CF-constraints is controlled with option tryConstrF of the translators. In addition to the use of GF or F-constraints, the translators differ also in the acceptance condition they finally produce: LTL2Omega will just have these constraints while LTL2OmegaCTL will rather use a CTL formula (equivalent to an LeftCTL*-LTL formula) with potential GF-constraints. In case F-constraints should be used LTL2OmegaCTL incorporates them to the CTL formula.