2 papers
cs.LO2026
NEXP-Completeness and Exponential Coefficient Growth for Existential Presburger Arithmetic with Divisibility
Ignacio Barros, Michaël Cadilhac, Guillermo A. Pérez
We prove that satisfiability for existential Presburger arithmetic with divisibility (EPAD) is NEXP-hard. Together with the known NEXP upper bound, this establishes NEXP-completene…
cs.LO2025
Analyzing Value Functions of States in Parametric Markov Chains
Kasper Engelen, Guillermo A. Pérez, Shrisha Rao
Parametric Markov chains (pMC) are used to model probabilistic systems with unknown or partially known probabilities. Although (universal) pMC verification for reachability propert…