LIRA

Linear Integer/Real Arithmetic Solver

There are many classes of system which can be described using first-order logic over mixed integer/real addition, i.e., over the structure (ℝ, ℤ, +, <). One class of such systems are linear hybrid automata, that is, systems consisting of digital and analog parts. An efficient decision procedure for this logic is required to analyze this class of systems.

We decide this logic using automata. We construct automata that represent all satisfying variable assignments. Since the binary encoding for reals is of infinite length, we use automata over so-called ω-words. It has been shown that weak deterministic Büchi automata suffice to represent subsets of ℝⁿ that are definable in the first-order logic over (ℝ, ℤ, +, <).

LIRA consists of a toolkit for efficiently representing and manipulating such automata. Our aim is to establish new theoretical results that allow for analyzing larger systems, and to put those results into use.