Deciding first-order logic with real and integer addition: an automata-based approach

Jochen Eisinger

Formal verification of complex systems requires efficient decision procedures for logics. In this thesis, we analyze an automata-based approach to decide first-order logic with real and integer addition using a variant of Büchi automata to represent solutions of formulas in the above mentioned logic. We leverage binary decision diagram techniques for representing the automata, and analyze algorithms for the product and the power set construction exposing possible improvements. An implementation was developed based on this and was evaluated against the Liége Automata-based Symbolic Handler (LASH). Our experiments show that the optimizations we suggested in this thesis lead to an overall speed-up in runtime of more than one order of magnitude. Finally, we present a demonstration application application for our solver by automatically verifying safety properties for linear hybrid automata.

back