2 citations · 3 across the 4 of their papers we have counts for
Showing cs.LOShow all
3 papers · 1 filter
cs.LO2021★ 1 cited
Presburger arithmetic with threshold counting quantifiers is easy
Dmitry Chistikov, Christoph Haase, Alessio Mansutti
We give a quantifier elimination procedures for the extension of Presburger arithmetic with a unary threshold counting quantifier that determines whether the nu…
cs.LO2020
Directed Reachability for Infinite-State Systems
Michael Blondin, Christoph Haase, Philip Offtermatt
Numerous tasks in program analysis and synthesis reduce to deciding reachability in possibly infinite graphs such as those induced by Petri nets. However, the Petri net reachabilit…
cs.LO2020
On the Expressiveness of Büchi Arithmetic
Christoph Haase, Jakub Różycki
We show that the existential fragment of Büchi arithmetic is strictly less expressive than full Büchi arithmetic of any base, and moreover establish that its -fragment is alre…