Publications
2026
- Automata-Theoretic Verification of Interval Markov Decision ProcessesSarvin Bahmani, Soumyajit Paul, Sven Schewe, and 2 more authorsIn IEEE Conference on Decision and Control, 2026
Interval Markov decision processes (IMDPs) provide a natural framework for modeling stochastic systems with uncertain transition probabilities, represented by probability intervals and resolved adversarially. Such uncertainty arises naturally, for example, when the transition model is learned from finite data or obtained through model-based reinforcement learning. In this paper, we study the automata-theoretic verification of IMDPs against rich temporal specifications, including all LTL specifications, by considering the broader class of ω-regular objectives. We show that classical automata-theoretic verification techniques extend to IMDPs, but with a sharp distinction determined by the structure of the transition intervals. For stable IMDPs, where interval bounds exclude zero, verification reduces to ordinary MDP analysis and can be carried out using the standard automata used in that setting (good-for-MDP automata). For unstable IMDPs, where intervals may include zero, verification becomes game-like and requires automata whose nondeterminism can be resolved online (good-for-games automata). Building on these insights, we develop algorithms for verifying ω-regular specifications over IMDPs and derive probabilistic guarantees when the interval model is learned from sampled data. The resulting framework enables principled verification of stochastic systems under probabilistic model uncertainty, connecting automata-based verification with data-driven stochastic modeling.
@inproceedings{bpst2026imdp, title = {Automata-Theoretic Verification of Interval Markov Decision Processes}, author = {Bahmani, Sarvin and Paul, Soumyajit and Schewe, Sven and Soudjani, Sadegh and Trivedi, Ashutosh}, booktitle = {IEEE Conference on Decision and Control}, year = {2026}, } - Asymmetrically-Discounted Stochastic GamesSarvin Bahmani, Soumyajit Paul, Sven Schewe, and 2 more authorsIn International Conference on Concurrency Theory, 2026
We study asymmetrically discounted stochastic games, in which players use distinct and reasonably apart discount factors. We show that optimal strategies in these games may require both memory and randomisation, in contrast to the classical symmetrically discounted setting. Our main technical contribution establishes that computing incentive Stackelberg equilibria—a variant of Stackelberg equilibria in which one player, called Player Max, can offer payments to the other player, called Player Min—is no harder than solving classical discounted games. We further show that optimal strategies in this setting can be realised by finite counting strategies, whereas restricting players to stationary strategies makes the problem computationally intractable. Finally, we establish that computing classical Stackelberg equilibria in these games under the constraint of memoryless strategies is NP-complete and remains NP-hard even when general or counting strategies are allowed.
@inproceedings{bpst2026asymmetric, title = {Asymmetrically-Discounted Stochastic Games}, author = {Bahmani, Sarvin and Paul, Soumyajit and Schewe, Sven and Tasdighi Kalat, Shadi and Trivedi, Ashutosh}, booktitle = {International Conference on Concurrency Theory}, year = {2026}, } - Social Welfare under Heterogeneous Time PreferencesSarvin Bahmani, Soumyajit Paul, Sven Schewe, and 2 more authorsIn International Joint Conference on Artificial Intelligence, 2026
In several socioeconomic-critical decision-making settings, such as fair resource allocation, climate policy, or AI alignment, multiple principals interact within a common arena. While it is well established that these principals may have differing preferences, decision-making under heterogeneous time preferences remains relatively unexplored. In particular, principals may weigh future outcomes differently and may derive distinct utilities from the same decisions. Motivated by such scenarios, we introduce the notion of heterogeneous time preferences in MDPs, where multiple principals possess distinct reward functions and apply different discount factors to future rewards. To compute meaningful decisions in such settings, an AI agent must rely on a notion of optimality that accounts for the preferences of all principals. We adopt a utilitarian notion of social welfare, defined as the sum of utilities accrued to all principals, and study the synthesis of agent strategies that maximise this welfare. Under heterogeneous time preferences, we show that optimal strategies are no longer positional, even when all principals receive identical rewards. Nevertheless, optimal strategies remain structurally simple: they can be realized as pure finite-memory counting strategies, require only polynomial memory in the system size, and can be synthesized in polynomial time. On the other hand, we show that deciding threshold questions for optimal positional strategies is NP-hard, exposing a poor trade-off: insisting on positional simplicity neither makes synthesis tractable nor preserves social welfare.
@inproceedings{bpst2026welfare, title = {Social Welfare under Heterogeneous Time Preferences}, author = {Bahmani, Sarvin and Paul, Soumyajit and Schewe, Sven and Tasdighi Kalat, Shadi and Trivedi, Ashutosh}, booktitle = {International Joint Conference on Artificial Intelligence}, year = {2026}, } - The Complexity of Games with Randomised ControlSarvin Bahmani, Rasmus Ibsen-Jensen, Soumyajit Paul, and 5 more authorsIn Foundations of Software Science and Computation Structures, 2026
In several socioeconomic-critical decision-making settings, such as fair resource allocation, climate policy, or AI alignment, multiple principals interact within a common arena. While it is well established that these principals may have differing preferences, decision-making under heterogeneous time preferences remains relatively unexplored. In particular, principals may weigh future outcomes differently and may derive distinct utilities from the same decisions. Motivated by such scenarios, we introduce the notion of heterogeneous time preferences in MDPs, where multiple principals possess distinct reward functions and apply different discount factors to future rewards. To compute meaningful decisions in such settings, an AI agent must rely on a notion of optimality that accounts for the preferences of all principals. We adopt a utilitarian notion of social welfare, defined as the sum of utilities accrued to all principals, and study the synthesis of agent strategies that maximise this welfare. Under heterogeneous time preferences, we show that optimal strategies are no longer positional, even when all principals receive identical rewards. Nevertheless, optimal strategies remain structurally simple: they can be realized as pure finite-memory counting strategies, require only polynomial memory in the system size, and can be synthesized in polynomial time. On the other hand, we show that deciding threshold questions for optimal positional strategies is NP-hard, exposing a poor trade-off: insisting on positional simplicity neither makes synthesis tractable nor preserves social welfare.
@inproceedings{schewe2026randomised, title = {The Complexity of Games with Randomised Control}, author = {Bahmani, Sarvin and Ibsen-Jensen, Rasmus and Paul, Soumyajit and Schewe, Sven and Slivovsky, Friedrich and Tang, Qiyi and Wojtczak, Dominik and Zhu, Shufang}, booktitle = {Foundations of Software Science and Computation Structures}, year = {2026}, doi = {10.1007/978-3-032-22730-0_3}, }
2022
- Convolutional Neural Networks for Very Low-dimensional LPV Approximations of Incompressible Navier-Stokes EquationsJan Heiland, Peter Benner, and Rezvan BahmaniFrontiers in Applied Mathematics and Statistics, 2022
@article{heiland2022cnn, title = {Convolutional Neural Networks for Very Low-dimensional LPV Approximations of Incompressible Navier-Stokes Equations}, author = {Heiland, Jan and Benner, Peter and Bahmani, Rezvan}, journal = {Frontiers in Applied Mathematics and Statistics}, year = {2022}, }