Ramsey Quantifiers in First-Order Logic

The verification of software correctness is becoming increasingly important due to the widespread use of computers, particularly in safety-critical environments. Many complex systems (such as those involving numeric data types, recursion, or multithreading) naturally exhibit an unbounded number of program states (a.k.a. configurations). These are referred to as infinite-state systems and their verification is an active research area with numerous unresolved problems. A key focus in this field is the verification of safety and liveness properties. While safety verification can be reduced to reachability via finite paths, liveness verification involves reasoning about infinite executions, making it considerably more challenging. Most approaches for checking liveness properties are devised for specific classes of systems. We study so-called Ramsey quantifiers, which state the existence of infinite cliques in the graph defined by a formula, in various first-order theories. We show that over automatic structures, which is the class of first-order structures whose domain and relations are regular, Ramsey quantifiers can be evaluated in logarithmic space. For tree-regular relations we give a polynomial-time evaluation algorithm if a deterministic bottom-up tree automaton is provided or if the relation is transitive. We furthermore study Ramsey quantifiers in more specific theories. Linear arithmetics over integers/reals are prominent theories featured in SMT solvers. We show that the Ramsey quantifier can be eliminated from existential formulas in linear arithmetic over the integers, reals, and their mixture in polynomial time. This directly enables the use of highly optimized SMT solvers. As an application, we provide a general framework for liveness verification across a wide range of infinite-state systems. For example, we prove precise complexity results for recurrent reachability with generalized Büchi condition over (tree-)regular relations and linear liveness for succinct one-counter automata, reversal-bounded counter machines, continuous vector addition systems with states, and Parikh automata. As a second major application, we identify the problem of checking whether a given formula is monadically decomposable, i.e. equivalent to a Boolean combination of formulas, each depending only on a single free variable. Monadic decompositions can, for example, be used in constraint databases, string analysis, and quantifier elimination. We prove precise complexity results in the case of quantifier-free formulas in linear integer/real arithmetic. We additionally explore a related problem: checking whether a relation on words (resp. trees) is (tree-)recognizable, i.e. a finite union of Cartesian products of (tree-)regular languages.