@inproceedings{21717, abstract = {Robust Markov Decision Processes (RMDPs) generalize classical MDPs that consider uncertainties in transition probabilities by defining a set of possible transition functions. An objective is a set of runs (or infinite trajectories) of the RMDP, and the value for an objective is the maximal probability that the agent can guarantee against the adversarial environment. We consider (a) reachability objectives, where given a target set of states, the goal is to eventually arrive at one of them; and (b) parity objectives, which are a canonical representation for ω-regular objectives. The qualitative analysis problem asks whether the objective can be ensured with probability 1. In this work, we study the qualitative problem for reachability and parity objectives on RMDPs without making any assumption over the structures of the RMDPs, e.g., unichain or aperiodic. Our contributions are twofold. We first present efficient algorithms with oracle access to uncertainty sets that solve qualitative problems of reachability and parity objectives. We then report experimental results demonstrating the effectiveness of our oracle-based approach on classical RMDP examples from the literature scaling up to thousands of states.}, author = {Asadi, Ali and Chatterjee, Krishnendu and Kafshdar Goharshadi, Ehsan and Karrabi, Mehrdad and Shafiee, Ali}, booktitle = {Proceedings of the 40th AAAI Conference on Artificial Intelligence}, issn = {2374-3468}, location = {Singapore, Singapore}, number = {43}, pages = {36137--36145}, publisher = {Association for the Advancement of Artificial Intelligence}, title = {{Qualitative analysis of ω-regular objectives on robust MDPs}}, doi = {10.1609/aaai.v40i43.40931}, volume = {40}, year = {2026}, } @article{22102, abstract = {Differential privacy (DP) has established itself as one of the standards for ensuring privacy of individual data. However, reasoning about DP is a challenging and error-prone task, hence methods for formal verification and refutation of DP properties have received significant interest in recent years. In this work, we present a novel method for automated formal refutation of є-DP. Our method refutes є-DP by searching for a pair of inputs together with a non-negative function over outputs whose expected value on these two inputs differs by a significant amount. The two inputs and the non-negative function over outputs are computed simultaneously, by utilizing upper expectation supermartingales and lower expectation submartingales from probabilistic program analysis, which we leverage to introduce a sound and complete proof rule for є-DP refutation. To the best of our knowledge, our method is the first method for є-DP refutation to offer the following four desirable features: (1) it is fully automated, (2) it is applicable to stochastic mechanisms with sampling instructions from both discrete and continuous distributions, (3) it provides soundness guarantees, and (4) it provides semi-completeness guarantees. Our experiments show that our prototype tool SuperDP achieves superior performance compared to the state of the art and manages to refute є-DP for a number of challenging examples collected from the literature, including ones that were out of the reach of prior methods.}, author = {Chatterjee, Krishnendu and Kafshdar Goharshadi, Ehsan and Zikelic, Dorde}, issn = {2475-1421}, journal = {Proceedings of the ACM on Programming Languages}, keywords = {Static Program Analysis, Differential Privacy, Probabilistic Programming, Martingales}, number = {PLDI}, publisher = {ACM}, title = {{SuperDP: Differential privacy refutation via supermartingales}}, doi = {10.1145/3808296}, volume = {10}, year = {2026}, } @misc{22134, abstract = {This artifact provides the source code, benchmarks, and scripts necessary to build and reproduce the experimental results for `SuperDP` (Accepted at PLDI 2026). It also includes instructions for running the tool on user-provided inputs.}, author = {Chatterjee, Krishnendu and Kafshdar Goharshadi, Ehsan and Zikelic, Dorde}, publisher = {Zenodo}, title = {{SuperDP: Differential Privacy Refutation via Supermartingales}}, doi = {10.5281/ZENODO.18930113}, year = {2026}, } @inproceedings{22920, abstract = {Two-player games on graphs are a classical framework for analyzing strategic decision making. In turn-based games, two players move a token along the edges of the graph, and the right to move the token is determined by the current vertex. In traditional bidding games - referred to as pure bidding games - the right to move the token is determined at each step through bidding; here we consider Richman bidding, where the winning player of a bid pays the losing player. The winner is decided based on a temporal or quantitative specification evaluated over the resulting infinite play. In this work, we combine turn-based games and pure bidding games into generalized bidding games, with player-1 vertices, player-2 vertices, and bidding vertices. This natural and simple generalization of bidding games has far-reaching consequences. First, we show that, as a model, generalized bidding games are more expressive than pure bidding games, and we provide several applications. Second, and most importantly, we show that generalized Richman bidding games are structurally equivalent to simple stochastic games, a well-studied model: they are linearly interreducible to each other. As was previously known, the special case of pure Richman bidding games corresponds to random-turn games. In other words, generalized bidding games extend pure bidding games in the same way that simple stochastic games extend random-turn games. We use this connection to solve generalized Richman bidding games for temporal (parity) and quantitative (mean-payoff and discounted-sum) specifications. From a computational perspective, we establish that generalized bidding games with parity and mean-payoff specifications retain the best known upper bounds for turn-based games and pure bidding games, namely NP∩coNP. Finally, we study a repair problem that asks whether bidding vertices can be assigned "owners" so as to bring the threshold budget required to win the game below a given target. This problem has direct applications in compositional policy synthesis for multi-objective settings, and we show it to be NP-complete.}, author = {Asadi, Ali and Henzinger, Thomas A and Kafshdar Goharshadi, Ehsan and Kebis, Pavol and Mallik, Kaushik}, booktitle = {37th International Conference on Concurrency Theory}, isbn = {9783959774475}, issn = {1868-8969}, keywords = {Bidding Games, Stochastic Games}, location = {Liverpool, United Kingdom}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Generalized bidding games: Where bidding and stochastic games meet}}, doi = {10.4230/LIPIcs.CONCUR.2026.13}, volume = {391}, year = {2026}, } @inproceedings{19744, abstract = {We consider the problem of refuting equivalence of probabilistic programs, i.e., the problem of proving that two probabilistic programs induce different output distributions. We study this problem in the context of programs with conditioning (i.e., with observe and score statements), where the output distribution is conditioned by the event that all the observe statements along a run evaluate to true, and where the probability densities of different runs may be updated via the score statements. Building on a recent work on programs without conditioning, we present a new equivalence refutation method for programs with conditioning. Our method is based on weighted restarting, a novel transformation of probabilistic programs with conditioning to the output equivalent probabilistic programs without conditioning that we introduce in this work. Our method is the first to be both a) fully automated, and b) providing provably correct answers. We demonstrate the applicability of our method on a set of programs from the probabilistic inference literature.}, author = {Chatterjee, Krishnendu and Kafshdar Goharshadi, Ehsan and Novotný, Petr and Zikelic, Dorde}, booktitle = {31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, isbn = {9783031906527}, issn = {1611-3349}, location = {Hamilton, ON, Canada}, pages = {279--300}, publisher = {Springer Nature}, title = {{Refuting equivalence in probabilistic programs with conditioning}}, doi = {10.1007/978-3-031-90653-4_14}, volume = {15697}, year = {2025}, } @inproceedings{19667, abstract = {The problem of checking satisfiability of linear real arithmetic (LRA) and non-linear real arithmetic (NRA) formulas has broad applications, in particular, they are at the heart of logic-related applications such as logic for artificial intelligence, program analysis, etc. While there has been much work on checking satisfiability of unquantified LRA and NRA formulas, the problem of checking satisfiability of quantified LRA and NRA formulas remains a significant challenge. The main bottleneck in the existing methods is a computationally expensive quantifier elimination step. In this work, we propose a novel method for efficient quantifier elimination in quantified LRA and NRA formulas. We propose a template-based Skolemization approach, where we automatically synthesize linear/polynomial Skolem functions in order to eliminate quantifiers in the formula. The key technical ingredient in our approach are Positivstellensätze theorems from algebraic geometry, which allow for an efficient manipulation of polynomial inequalities. Our method offers a range of appealing theoretical properties combined with a strong practical performance. On the theory side, our method is sound, semi-complete, and runs in subexponential time and polynomial space, as opposed to existing sound and complete quantifier elimination methods that run in doubly-exponential time and at least exponential space. On the practical side, our experiments show superior performance compared to state of the art SMT solvers in terms of the number of solved instances and runtime, both on LRA and on NRA benchmarks.}, author = {Chatterjee, Krishnendu and Kafshdar Goharshadi, Ehsan and Karrabi, Mehrdad and Motwani, Harshit J. and Seeliger, Maximilian and Zikelic, Dorde}, booktitle = {Proceedings of the 39th AAAI Conference on Artificial Intelligence}, issn = {2374-3468}, location = {Philadelphia, PA, United States}, number = {11}, pages = {11158--11166}, publisher = {Association for the Advancement of Artificial Intelligence}, title = {{Quantified linear and polynomial arithmetic satisfiability via template-based skolemization}}, doi = {10.1609/aaai.v39i11.33213}, volume = {39}, year = {2025}, } @inproceedings{20648, abstract = {Polynomial quantified entailments with existentially and universally quantified variables arise in many problems of verification and program analysis. We present PolyQEnt which is a tool for solving polynomial quantified entailments in which variables on both sides of the implication are real valued or unbounded integers. Our tool provides a unified framework for polynomial quantified entailment problems that arise in several papers in the literature. Our experimental evaluation over a wide range of benchmarks shows the applicability of the tool as well as its benefits as opposed to simply using existing SMT solvers to solve such constraints.}, author = {Chatterjee, Krishnendu and Goharshady, Amir Kafshdar and Kafshdar Goharshadi, Ehsan and Karrabi, Mehrdad and Saadat, Milad and Seeliger, Maximilian and Zikelic, Dorde}, booktitle = {23rd International Symposium on Automated Technology for Verification and Analysis}, isbn = {9783032087065}, issn = {1611-3349}, location = {Bengaluru, India}, pages = {411--424}, publisher = {Springer Nature}, title = {{PolyQEnt: A polynomial quantified entailment solver}}, doi = {10.1007/978-3-032-08707-2_19}, volume = {16145}, year = {2025}, } @inproceedings{18160, abstract = {Markov decision processes (MDPs) provide a standard framework for sequential decision making under uncertainty. However, MDPs do not take uncertainty in transition probabilities into account. Robust Markov decision processes (RMDPs) address this shortcoming of MDPs by assigning to each transition an uncertainty set rather than a single probability value. In this work, we consider polytopic RMDPs in which all uncertainty sets are polytopes and study the problem of solving long-run average reward polytopic RMDPs. We present a novel perspective on this problem and show that it can be reduced to solving long-run average reward turn-based stochastic games with finite state and action spaces. This reduction allows us to derive several important consequences that were hitherto not known to hold for polytopic RMDPs. First, we derive new computational complexity bounds for solving long-run average reward polytopic RMDPs, showing for the first time that the threshold decision problem for them is in NP∩CONP and that they admit a randomized algorithm with sub-exponential expected runtime. Second, we present Robust Polytopic Policy Iteration (RPPI), a novel policy iteration algorithm for solving long-run average reward polytopic RMDPs. Our experimental evaluation shows that RPPI is much more efficient in solving long-run average reward polytopic RMDPs compared to state-of-the-art methods based on value iteration. }, author = {Chatterjee, Krishnendu and Kafshdar Goharshadi, Ehsan and Karrabi, Mehrdad and Novotný, Petr and Zikelic, Dorde}, booktitle = {33rd International Joint Conference on Artificial Intelligence}, isbn = {9781956792041}, issn = {1045-0823}, location = {Jeju, South Korea}, pages = {6707--6715}, publisher = {International Joint Conferences on Artificial Intelligence}, title = {{Solving long-run average reward robust MDPs via stochastic games}}, doi = {10.24963/ijcai.2024/741}, year = {2024}, } @article{17283, abstract = {We consider the problems of statically refuting equivalence and similarity of output distributions defined by a pair of probabilistic programs. Equivalence and similarity are two fundamental relational properties of probabilistic programs that are essential for their correctness both in implementation and in compilation. In this work, we present a new method for static equivalence and similarity refutation. Our method refutes equivalence and similarity by computing a function over program outputs whose expected value with respect to the output distributions of two programs is different. The function is computed simultaneously with an upper expectation supermartingale and a lower expectation submartingale for the two programs, which we show to together provide a formal certificate for refuting equivalence and similarity. To the best of our knowledge, our method is the first approach to relational program analysis to offer the combination of the following desirable features: (1) it is fully automated, (2) it is applicable to infinite-state probabilistic programs, and (3) it provides formal guarantees on the correctness of its results. We implement a prototype of our method and our experiments demonstrate the effectiveness of our method to refute equivalence and similarity for a number of examples collected from the literature.}, author = {Chatterjee, Krishnendu and Kafshdar Goharshadi, Ehsan and Novotný, Petr and Zikelic, Dorde}, issn = {2475-1421}, journal = {Proceedings of the ACM on Programming Languages}, publisher = {Association for Computing Machinery}, title = {{Equivalence and similarity refutation for probabilistic programs}}, doi = {10.1145/3656462}, volume = {8}, year = {2024}, } @inproceedings{10414, abstract = {We consider the almost-sure (a.s.) termination problem for probabilistic programs, which are a stochastic extension of classical imperative programs. Lexicographic ranking functions provide a sound and practical approach for termination of non-probabilistic programs, and their extension to probabilistic programs is achieved via lexicographic ranking supermartingales (LexRSMs). However, LexRSMs introduced in the previous work have a limitation that impedes their automation: all of their components have to be non-negative in all reachable states. This might result in LexRSM not existing even for simple terminating programs. Our contributions are twofold: First, we introduce a generalization of LexRSMs which allows for some components to be negative. This standard feature of non-probabilistic termination proofs was hitherto not known to be sound in the probabilistic setting, as the soundness proof requires a careful analysis of the underlying stochastic process. Second, we present polynomial-time algorithms using our generalized LexRSMs for proving a.s. termination in broad classes of linear-arithmetic programs.}, author = {Chatterjee, Krishnendu and Kafshdar Goharshadi, Ehsan and Novotný, Petr and Zárevúcky, Jiří and Zikelic, Dorde}, booktitle = {24th International Symposium on Formal Methods}, isbn = {9-783-0309-0869-0}, issn = {1611-3349}, location = {Virtual}, pages = {619--639}, publisher = {Springer Nature}, title = {{On lexicographic proof rules for probabilistic termination}}, doi = {10.1007/978-3-030-90870-6_33}, volume = {13047}, year = {2021}, }