LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals (Tool Paper)

摘要

The mechanization of many verification tasks relies on efficient implementations of decision procedures for fragments of first-order logic. Interactive theorem provers like PVS also make use of such decision procedures to increase the level of automation. Our tool LIRA1 implements decision procedures based on automata-theoretic techniques for first-order logics with linear arithmetic, namely, for FO(N, +), FO(Z, +, ＜), and FO(M, Z, +, ＜). The theoretical foundations for using automata to decide logics like Presburger arithmetic, I.e., FO(N, +) were laid in the 1960s [4]: For Presburger arithmetic, the elements of the domain are represented by finite words, and for a given formula, one constructs recursively over the formula structure an automaton that accepts precisely the words that represent the natural numbers that satisfy the formula. Automata constructions handle the logical connectives and quantifiers. A similar approach works for FO(Z, +, ＜) and FO(K, Z, +. ＜). To represent reals, one uses infinite words. In [2], it is shown that weak deterministic Buchi automata (wdbas) suffice to decide FO(R, Z, +, ＜). Wdbas are a restricted class of Buechi automata, which can be handled algorithmically almost as efficiently as deterministic finite automata (dfas). LIRA also provides an automata library that efficiently represents and manipulates DFAs and WDBAs. Lira's automata library can be compared to a BDD library for representing and manipulating finite sets encoded by booleans. Instead of BDDs, LIRA uses DFAs to represent and manipulate sets that are definable in FO(N, +) and FO(Z, +, ＜), and uses wdbas for sets definable in FO(E, Z, +, ＜). Efficiently representing and manipulating such definable sets has applications beyond deciding these logics efficiently. For instance, in the safety verification of integer-counter systems and hybrid systems one has to cope with such sets. Furthermore, approaches like regular model checking rely on manipulating automata efficiently. Lira's automata library can be used in all these applications. Closely related to lira are lash [13], prestaf [5], and mona [12]. Like lira's automata library, LASH provides operations for automata over finite and infinite words. LIRA outperforms lash by several orders of magnitude. One reason for the speedup are novel automata constructions. PRESTAF's and MONA's automata libraries only support automata over finite words and can only handle Presburger definable sets. Moreover, MONA's automata library is not tailored to the representation and manipulation of Presburger definable sets. The OMEGA library [14] is related to LIRA since it allows one to represent and manipulate sets definable in FO(Z,+,＜). In contrast to LIRA, it does not support the reals and uses a formula-based set representation, which does not have a canonical form. Heuristics are used to simplify the set representations. SMT solvers like MATHSAT [3] and YICES [9] are also related to LIRA since they provide decision procedures for fragments of linear arithmetic over the integers and reals. However, these solvers do not handle quantifiers at all or only in a limited way. Note that most current SMT solvers also handle other fragments of first-order theories and combinations thereof. In the following, in §2, we give implementation details and list some features of LIRA, and in §3, we report on applications and performance.