| Autor: |
Scholl, Christoph, Disch, Stefan, Pigorsch, Florian, Kupferschmid, Stefan |
| Zdroj: |
Tools & Algorithms for the Construction & Analysis of Systems (9783642007675); 2009, p383-397, 15p |
| Abstrakt: |
We present a method which computes optimized representations for non-convex polyhedra. Our method detects so-called redundant linear constraints in these representations by using an incremental SMT (Satisfiability Modulo Theories) solver and then removes the redundant constraints based on Craig interpolation. The approach is motivated by applications in the context of model checking for Linear Hybrid Automata. Basically, it can be seen as an optimization method for formulas including arbitrary boolean combinations of linear constraints and boolean variables. We show that our method provides an essential step making quantifier elimination for linear arithmetic much more efficient. Experimental results clearly show the advantages of our approach in comparison to state-of-the-art solvers. [ABSTRACT FROM AUTHOR] |
| Databáze: |
Complementary Index |
| Externí odkaz: |
|
