LIRA

| project staff | description | publications |

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. Deciding this logic can be done 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. LIRA is a toolkit for efficiently representing and manipulating such automata.

LIRA is not maintained anymore. More details can be found at http://lira.gforge.avacs.org/