23 citations · 34 across the 8 of their papers we have counts for
7 papers · 1 filter
Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic (Technical Report)
Peter Habermehl, Vojtěch Havlena, Michal Hečko +2
We present a new angle on solving quantified linear integer arithmetic based on combining the automata-based approach, where numbers are understood as bitvectors, with ideas from (…
On Presburger arithmetic extended with non-unary counting quantifiers
Peter Habermehl, Dietrich Kuske
We consider a first-order logic for the integers with addition. This logic extends classical first-order logic by modulo-counting, threshold-counting and exact-counting quantifiers…
Left-eigenvectors are certificates of the Orbit Problem
Steven de Oliveira, Virgile Prevosto, Peter Habermehl +1
This paper investigates the connexion between the Kannan-Lipton Orbit Problem and the polynomial invariant generator algorithm PILA based on eigenvectors computation. Namely, we re…
Model-checking Counting Temporal Logics on Flat Structures
Normann Decker, Peter Habermehl, Martin Leucker +2
We study several extensions of linear-time and computation-tree temporal logics with quantifiers that allow for counting how often certain properties hold. For most of these extens…
A Robust Class of Data Languages and an Application to Learning
Benedikt Bollig, Peter Habermehl, Martin Leucker +1
We introduce session automata, an automata model to process data words, i.e., words over an infinite alphabet. Session automata support the notion of fresh data values, which are w…
On the Path-Width of Integer Linear Programming
Constantin Enea, Peter Habermehl, Omar Inverso +1
We consider the feasibility problem of integer linear programming (ILP). We show that solutions of any ILP instance can be naturally represented by an FO-definable class of graphs.…
Ordered Navigation on Multi-attributed Data Words
Normann Decker, Peter Habermehl, Martin Leucker +1
We study temporal logics and automata on multi-attributed data words. Recently, BD-LTL was introduced as a temporal logic on data words extending LTL by navigation along positions…