Averest.Analysis Namespace
Modules | Description |
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 symbolic model checking of mu-calculus and temporal logics. The model checking algorithms are mainly implemented by means of BDDs. There is also a function for symbolic computation of predecessor and successor states using quantifier elimination. |
|
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, i.e., essentially alternating 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 be avoided in general, but the translators presented here try to use F-constraints or FG-constraints whenever possible so that automata with safety, liveness, co-Büchi and Büchi conditions (see Averest.Core.Specifications.AcceptanceType) are obtained. The main functions are as follows:
|