LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals

Bernd Becker, Christian Dax, Jochen Eisinger, and Felix Klaedtke

We present the tool LIRA that implements decision procedures based on automata-theoretic techniques for first-order logics with linear arithmetic over the integers and the reals. LIRA also provides an efficient automata library, which is accessible through a high-level and low-level API.

On this webpage we report on our experimental setting and present the results.

Table of Contents

• Tool paper
• Download
  • Sources
  • Binaries
• Benchmark Results
  1. Random Formulas
  2. Formulas from the First-order Model Checker
  3. FASTer/GENEPI benchmarks
• Tool Usage
• Compiling

Tool paper

• B. Becker, C. Dax, J. Eisinger, and F. Klaedtke, LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals, 19th International Conference on Computer Aided Verification. LNCS 4590. pp 312-315. Springer-Verlag, 2007. [PDF] [BibTex]

Download

Sources:

The sources of LIRA are licensed under the terms of the GNU General Public License Version 2. LIRA includes third party sources, which are copyrighted by their respective owners.

• LIRA 1.1.0 used for benchmarking: LIRA-1.1.0.tar.gz
• LASH v0.92 incl. linarith tool: lash-v0.92+linarith.tar.gz
• PresTAF 1.2 incl. modified parser: prestaf-1-2-parser.tar.gz
• FASTer snapshot: faster-snapshot.tar.gz
• Haskell tool for generating random formulas: randPrsb.hs

Binaries:

• GNU/Linux 2.6, i386 arch, g++ 4.1.2:
  • LIRA-1.1.0-gnu-linux-i386-static
  • lash-linarith-0.92-gnu-linux-i386-static
  • lash-presburger-0.9.2-gnu-linux-i386-static
  • prestaf-1.2-gnu-linux-i386-static
  • dijo-snapshot-gnu-linux-i386
    GENEPI Plugins:
    • liblira2fast-gnu-linux-i386.so
    • libmona2fast-gnu-linux-i386.so
    • liblash2fast-gnu-linux-i386.so
    • libomega2fast-gnu-linux-i386.so
    • libprestaf2fast-gnu-linux-i386.so
    • libprestaf-cache2fast-gnu-linux-i386.so
  • randPrsb-gnu-linux-i386-static
• GNU/Linux 2.6, amd64 arch, g++ 4.1.2:
  • LIRA-1.1.0-gnu-linux-amd64-static

Benchmarks

We carried out three different types of tests: (1) randomly generated formulas, (2) formulas from the domain of hybrid system verification, and (3) verification of integer-counter systems.

For the experiments, we used a dual AMD64 (Opteron 252 2.6GHz) machine with 16GB RAM running Debian GNU/Linux etch. Moreover, we used the GNU C++ Compiler 4.1.2 to compile the tools. We used 32-bit binaries for benchmarking to ensure comparability between the different tools.

All graphs below also link to a high-resolution version.

Random Formulas

We carried out benchmarks for constructing automata representing sets defined by random formulas. We used LIRA and LASH for FO(ℝ,ℤ,+,<) and FO(ℤ,+,<), and LIRA and PresTAF for FO(ℕ,+).

We have applied the tools to 100 randomly generated formulas with 4 variables, each involving about 10 disjunctions and conjunctions. The formulas are available here: random.tar.gz.

For all three logics three graphs are shown, where the first graph depicts the construction time of the automata for the quantifier-free formulas. The second and third graph shows the construction times for the formulas with quantifier prefix ∃ and ∀∃ respectively.

 

Fig. 1. Required runtime to construct minimal weak deterministic Büchi automata for formulas in FO(ℝ,ℤ,+,<)

In Figure 1 a red cross on the 1000s timeout line corresponds to a timeout.

 

Fig. 2. Required runtime to construct minimal deterministic finite automata from formulas in FO(ℤ,+,<)

 

Fig. 3. Required runtime to construct minimal deterministic finite automata from formulas in FO(ℕ,+)

In the experiments to Figure 2 and Figure 3, LASH and PresTAF ran out of memory for some formulas. These cases are marked with a red cross that is above the 20s timeout line. A red cross on the 20s timeout line corresponds to a timeout.

Formulas from the First-order Model Checker

The following formulas stem form the domain of hybrid systems. They are automatically generated by the First-order Model Checker when accelerating the reachability computations of a hybrid system. We extracted the formulas from 4 different hybrid systems and from different acceleration steps. The formulas have a ∀∃ quantifier prefix and contain variables that range over the reals and the booleans. We used LIRA's decision procedure for FO(ℝ,ℤ,+,<) to the build the minimal weak deterministic Büchi automata for these formulas. More details about the First-order Model Checker and the formulas can be found in [Damm et al., 2006a] and [Damm et al. 2006b]. These benchmarks were executed using the 64-bit binary of LIRA.

FASTer/GENEPI Benchmarks

We used the model checker FASTer for integer-counter systems. We compared the running times of our LIRA plugin for FASTer to the running times of other plugins based on MONA, LASH, PresTAF, and the Omega library.

The generated benchmarks can be executed using the tool dijo for the different plugins. The input files for the tool dijo were generated by FASTer with the MONA plugin. The running times of the different plugins are listet in Figure 5.

The dijo trace files are available here: dijo.tar.gz.

Note that benchmarks in which all plugins require less than 20 seconds are not listed in the table. Also note that LASH does not provide special support for the natural numbers. Hence, the LASH plugin uses a set representation that produces some overhead.

The PresTAF plugin has a built-in cache for storing and reusing intermediate results. We turned this cache off since, in principle, every FASTer plugin can be equipped with such a cache. In our experiments, we wanted to test the underlying libraries for representing and manipulating sets definable in Presburger arithmetic. The intention of our tests was not to evaluate the maturity of the implementations of different FASTer plugins. Nevertheless, the last column shows the running times of the PresTAF plugin where the cache was enabled. We want to point out that PresTAF itself has a cache, which was not disabled.

Usage

Frontend

The frontend to LIRA called 'LIRA' is a parser for first-order formulas. It uses the decision procedures implemented in the LIRA library to check whether a given formula is satisfiable with respect to a selected logic.

When you run LIRA with the parameter --help, you get an overview of the available options:

LIRA - a solver for first-order logic of the mixed linear arithmetic
over the integers and reals.

Usage: LIRA [options ..]

options:
  --parser [parser]     select parser (default is 'mixlinarith')
  --planner [planner]   select planner (default is 'simple')
  --logic [logic]       select logic (default is 'reals')
  --solver [solver]     select solver (default is 'wdba')
  --file file           input file
  --dump                dump the last set constructed
  --output file         send output to file instead of stdout
  --verbose             increase verbosity
  --help                show this help

parsers:        mixlinarith
planners:       simple
logics:         reals, ints, presburger
solvers:        wdba, dontcares, dfa

Homepage: http://lira.gforge.avacs.org/

The syntax of the formulas is as follows:

formula                 : <quantifier> ( <variable> : <formula> )
                        | <quantifier> ( <boolean> : <formula> )
                        | <formula> <binary-connective> <formula>
                        | <unary-connective> <formula>
                        | <term> <relation> <term>
                        | ( <formula> )
                        | <boolean>

term                    : <term> <binary-function> <term>
                        | <unary-function> <term>
                        | ( <term> )
                        | <variable>
                        | <constant>

quantifier              : exists | forall

binary-connective       : and | or | xor | iff | implies | minus

unary-connective        : not

relation                : < | <= | = | != | >= | =

binary-function         : + | - | * | /

unary-function          : -

constant                : [0-9]+

variable                : [a-zA-Z][a-zA-Z0-9'_]*

boolean                 : TRUE | FALSE | $<variable>

Advanced Usage

For advanced usage please refer to the LIRA 1.x Handbook.

Compiling

Compile and install LIRA using the following commands:

./configure
make
make install

If you have CppUnit installed on your system, you can also run a set of unit tests to verify the installation:

make check

Last update: 2007-07-01
Copyright © The LIRA Project. Valid XHTML 1.1.