Research

Automata-based Verification

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 (ℝ, ℤ, +, <).

to the FOL(ℝ, ℤ, +, <) library