Don't Care Words with an Application to the Automata-based Approach for Real Addition

Jochen Eisinger and Felix Klaedtke

Automata are a useful tool in infinite state model checking, since they can represent infinite sets of integers and reals. However, analogous to BDDs to represent finite sets, an obstacle of an automata-based set representation is the sizes of the automata. In this paper, we generalize the notion of "don't cares" for BDDs to word languages as a means to reduce the automata sizes. A general result in this paper shows that the minimal weak deterministic Büchi automaton (WDBA) with respect to a given don't care set with certain restrictions is uniquely determined and can be efficiently constructed. We apply don't cares to mechanize a more effective decision procedure for the first-order logic over the mixed linear arithmetic over the integers and the reals based on WDBAs.

Technical report

• J. Eisinger and F. Klaedtke, Don't care words with an application to the automata-based approach for real addition, Tech. Rep. 223, Institut für Informatik, Universität Freiburg, 2006. [pdf] [BibTex]

Download

Sources:

Please note that the sources of mixlinarith are licensed under the terms of the GNU General Public License Version 2.

• Snapshot used for benchmarking: rva-20060510.tar.gz
• LASH v0.92 incl. linarith tool: lash-v0.92+linarith.tar.gz
• Haskell tool for generating random formulas: randPrsb.hs

Binaries:

• GNU/Linux 2.6, i386 arch, g++ 4.0.3, static:
  • mixlinarith-20060510-gnu-linux-i386-static
  • linarith-lash-v0.92-gnu-linux-i386-static
  • randPrsb-gnu-linux-i386-static
• GNU/Linux 2.6, amd64 arch, g++ 4.0.3, static:
  • mixlinarith-20060510-gnu-linux-amd64-static
  • linarith-lash-v0.92-gnu-linux-amd64-static

Benchmarks:

• Random formulas with 4 variables (with and without quantifiers): random.tar.gz
• Fischer's protocol: fischer.tar.gz
• Railroad crossing: railroad.tar.gz
• Bakery protocol: bakery.tar.gz

Benchmarks

We have carried out tests on two different types of classes: (1) randomly generated formulas and (2) the iterative computation of the reachable states of infinite state systems. In the later case, we mainly focus on the sizes of the automata, as our prototype is not intended to compete with optimized tools for solving the reachability problem.

The benchmarks were run on a dual AMD64 (Opteron 252 2.6GHz) machine with 16GB RAM running Debian GNU/Linux etch. The program was compiled with the Intel C++ Compiler 9.1.038. Note that most benchmarks (especially when using don't care sets) will not use more than 4GB RAM.

All graphs shown here link to a high-res version.

Random formulas:

We have applied our prototype implementation to 100 randomly generated formulas with 4 variables, each involving about 10 disjunctions and conjunctions. The graphs in this section compare the performance of our prototype implementation against an implementation based on LASH. The LASH based implementation uses the (faster) serialized automata constructions, however, in order to compare automata sizes, we first unserialized the automata. Note that we did not include the time required to unserialize the final automata in our statistics.

While carrying out the tests for LASH we observed that the automata construction for handling the logical OR was unexpected slow. We changed its implementation by using the auto_product_union instead of the auto_product function in the file auto-operations.c. This change improved the LASH running times. For the following benchmarks, the improved version was used.

The following graphs show the sizes of the automata encountered during the construction of quantifier free formulas, the sizes of the final automata (representing the sets defined by each formula), and the construction times for mixlinarith and the LASH based linarith.

 

Fig. 1. Automata sizes (peak and final) encountered during the construction of the automata for 100 randomly generated quantifier free formulas. The red lines correspond to our prototype implementation, while the green lines correspond to the LASH based implementation.

Next, we existentially quantify one variable of each formula, i.e. for a quantifier free formula φ we now use ∃ x₁ φ. As expected, the new construction for the quantification takes longer (which we partly attribute to its prototypical implementation) and generates potentially larger automata (which become smaller again after normalization and minimization). Note that our prototype outperforms the LASH based implementation.

 

Fig. 2. Automata sizes (peak and final) encountered during the construction of the automata for 100 randomly generated formulas with quantification. The red lines correspond to our prototype implementation, while the green lines correspond to the LASH based implementation. Note that there is no data point available for the cases #78 and #86 due to exceeding the available memory (our implementation) or the time limit of 5h (LASH based).

Last, we benchmarked our implementation using the --presb option which restricts the automata to the integer domain using the Z predicate. Here the gap between the automata with and without a don't care set becomes large, which can be explained by the fact that all integers can be encoded by a don't care word, and thus there is more potential for savings. Note that when executing these benchmarks, you will have to preceed each formula with the statement ORDER x1,x2,x3,x4 :.

 

Fig. 3. Automata sizes (peak and final) encountered when restricting all variables to the integer domain. Here, both graphs are generated from our implementation, once with the optimized construction (red lines), and once with the straight-forward construction (green lines).

Linear Hybrid Automata

Infinite state systems, like systems with unbounded integers or linear hybrid automata can be analyzed symbolically in the first-order logic over ℜ. We have analyzed the Bakery protocol, Fischer's protocol, and the railroad crossing example. Using don't care words, the automata constructed during the iterative computation of the reachable states become smaller by up to several orders of magnitude. This saving can be explained by the two observations. First, the formulas that describe the transitions of a system contain many variables (the formulas for Fischer's protocol with 5 processes have 34 variables). Note that the don't care sets contain more words if the formula contains many free variables. Second, the construction of the reachable state set requires a large number of automata constructions. Although the saving at a single automata construction might be small, the overall saving grows with the number of automata constructions.

The following table summarizes the results of those benchmarks. The positive effect of our optimized encoding is clearly visible. Note that the automata constructed with and without don't care sets represent the same sets. This can easily be verified by turning the automaton constructed using the straight-forward construction in D-normal form. For example, load the automaton describing the reachable state set of Fischer 5 (after unpacking the file) into mixlinarith and apply the function RESTRICT to it:

RESTRICT ( "fischer5.dot" [x0, x1, x2, x3, ..., x32, x33] )

The resulting automaton will have the same size as the automaton constructed when using don't care sets.

Fig. 4. Number of iterations required to reach the fixpoint (except for Bakery) of the reachable state set for several infinite state systems, including automata construction times, and peak and final automata sizes. Note that the fixpoint for Bakery cannot be reached using simple naive iteration.

The following figures show the automata sizes encountered during the computation of the reachable state sets. The peak sizes show the maximal sizes of the automata encountered in each step, the sizes after minimization correspond to the automata at the end of each (intermediate) step.

We compute the reachable state set as follows. Starting from the initial state, we iteratively add states reachable from the current state set by the flows and jumps of the linear hybrid automata, until the current state set has reached a fixpoint. In the case of Fischer's protocol with 5 processes, we used an alternative approach and only considered the newly reached states for the next iteration. Note that for the Bakery protocol, it is not possible to reach the fixpoint using this simple naive algorithm. Therefore, we aborted the computation after 30 steps.

 

Fig. 5. Automata sizes (peak and final) encountered during the computation for Fischer's protocol with 2 processes. The red (green) lines correspond to the optimized (straight-forward) encoding. The intermediate construction steps correspond to the flows and jumps of the processes in Fischer's protocol.

 

Fig. 6. Automata sizes (peak and final) encountered during the computation for Fischer's protocol with 3 processes.

 

Fig. 7. Automata sizes (peak and final) encountered during the computation for Fischer's protocol with 4 processes.

 

Fig. 8. Automata sizes (peak and final) encountered during the computation for Fischer's protocol with 5 processes. Note that here an alternative algorithm for computing the reachable state set was used, which results in smaller automata sizes during the end of the computation.

 

Fig. 9. Automata sizes (peak and final) encountered during the computation for the railroad crossing example.

 

Fig. 10. Automata sizes (peak and final) encountered during the computation for the Bakery protocol with 2 processes.

 

Fig. 11. Automata sizes (peak and final) encountered during the computation for the Bakery protocol with 3 processes.

 

Fig. 12. Automata sizes (peak and final) encountered during the computation for the Bakery protocol with 4 processes.

Usage

Syntax:

The script mixlinarith reads a formula matching the following syntax from stdin:

formula		: ordering condition

ordering	: ORDER vars ':'
		| /* empty */

condition	: condition AND condition
		| condition OR condition
		| NOT condition
		| INT '(' NAME ')'
		| FORALL '(' vars ':' condition ')'
		| EXISTS '(' vars ':' condition ')'
		| FORALL2 '(' NAME ':' condition ')'
		| EXISTS2 '(' NAME ':' condition ')'
		| RESTRICT condition
		| '(' condition ')'
		| expression COMPARISON expression
		| STRING '[' vars ']'
		| '(' condition ')' '[' varmap ']'

varmap		: NAME '->' NAME ',' varmap
		| NAME '->' NAME

vars		: NAME ',' vars
		| NAME

expression	: expression '+' expression
		| expression '-' expression
		| '(' expression ')'
		| NAME
		| CONSTANT '*' NAME
		| '-' CONSTANT '*' NAME
		| CONSTANT
		| '-' CONSTANT

• The optional keyword ORDER defines a variable ordering for the BDDs. It is mandatory when using the --presb option (see below).
• The keywords EXISTS2 and FORALL2 refer to the new quantification construction. When the option --dontcares is given, the keywords EXISTS and FORALL are refering to the new quantification as well.
• The keyword RESTRICT turns the condition in D-normal form
• The keyword INT implements the predicate symbol Z
• The syntax "file.dot" [ var1, ..., varN ] loads an automaton stored as graphviz file file.dot, as created by mixlinarith or LASH, interpreting the variables 1 ... N of the automaton as variables var1 ... varN.
• The syntax condition [ var1 -> var1', ..., varN -> varN' ] permutes the variables in the automaton construction for the condition, replacing var1 with var1' and so on.

When ommitting then keywords ORDER, INT, FORALL2, EXISTS2, and RESTRICT, as well as the syntax for loading automata and swapping variables, the formulas are compatibel with the format parsed by the LASH based tool linarith.

Options:

The program mixlinarith takes the following command line parameters:

--stats

Displays detailed statistics about every single operation

--dot file

Dumps the automaton to file file

--times

Displays runtime statistics after constructing the automaton

--dontcares

Use the optimized construction with a don't care set

--presb

Construct automata that only accept integers

--vars

Dumps the variable order after constructing the automaton

--dump #op

Dumps the automaton constructed in step #op before normalization and minimization

Compiling

Compiling the sources requires CuDD 2.4.1 or better, a C++ compiler, the GNU Standard C++ Library v3, and flex & bison. Compilers confirmed to work are the GNU C++ compiler version 4.0.3 and the Intel C++ Compiler 9.1.038. The program is written for GNU/Linux 2.6 running on i386 and amd64 architectures.

Please note that this patch to CuDD 2.4.1 is required. This patch was submitted to the author of CuDD and will be included in the next release. Apply the patch like this:

~/cudd-2.4.1 $ patch -p1 < cudd.cuddLCache.c.patch
Patching file cudd/cuddLCache.c
~/cudd-2.4.1 $

Compile the sources by issuing make in the directory you have unpacked the sources to:

~/rva-20060510 $ make

The compiled CuDD sources are expected to reside in the directory ~/cudd-2.4.1. You can change the default location, by pointing the make variable CUDD at the new location. Similarly, it is possible to use another compiler. For example, issue this command to compile the program using the Intel C++ Compiler on amd64 architecture, where CuDD resides in /usr/local/cudd/2.4.1:

~/rva-20060510 $ make CC=icc CXX=icpc \
    CFLAGS="-O3 -g -static-libcxa -xW -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8" \
    XCFLAGS="-xW -ansi -align -ip -DBSD -DHAVE_IEEE_754 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8" \
    CUDD=/usr/local/cudd/2.4.1

The binary mixlinarith used for the benchmarks should be created in the subdirectory mixlinarith/.

Last update: 2006-05-10
Copyright © Jochen Eisinger & Felix Klaedtke. Valid XHTML 1.1.