3 papers
cs.LO2026
NEXP-Completeness of 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…
cs.LO2024
Continuous Pushdown VASS in One Dimension are Easy
Guillermo A. Perez, Shrisha Rao
A pushdown vector addition system with states (PVASS) extends the model of vector addition systems with a pushdown stack. The algorithmic analysis of PVASS has applications such as…