@inproceedings{21411, abstract = {To achieve fast recovery from link failures, most modern communication networks feature fully decentralized fast re-routing mechanisms. These re-routing mechanisms rely on pre-installed static re-routing rules at the nodes (the routers), which depend only on local failure information, namely on the failed links incident to the node. Ideally, a network is perfectly resilient: the re-routing rules ensure that packets are always successfully routed to their destinations as long as the source and the destination are still physically connected in the underlying network after the failures. Unfortunately, there are examples where achieving perfect resilience is not possible. Surprisingly, only very little is known about the algorithmic aspect of when and how perfect resilience can be achieved. We investigate the computational complexity of analyzing such local fast re-routing mechanisms. Our main result is a negative one: we show that even checking whether a given set of static re-routing rules ensures perfect resilience is coNP-complete. Additionally, we investigate other fundamental variations of the problem. In particular, we show that our coNP-completeness proof also applies to scenarios where the re-routing rules have specific patterns (known as skipping in the literature). On the positive side, for scenarios where nodes do not have information about the link from which a packet arrived (the so-called in-port), we present a linear-time algorithm to realize perfect resilience whenever possible (which we show can also be determined in linear time). }, author = {Bentert, Matthias and Ceylan, Esra and Hübner, Valentin and Schmid, Stefan and Srba, Jiří}, booktitle = {29th International Conference on Principles of Distributed Systems}, isbn = {9783959774093}, issn = {1868-8969}, location = {Iaşi, Romania}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Fast re-routing in networks: On the complexity of perfect resilience}}, doi = {10.4230/LIPIcs.OPODIS.2025.31}, volume = {361}, year = {2026}, } @article{21661, abstract = {Model checking undiscounted reachability and expected-reward properties on Markov decision processes (MDPs) are key for the verification of systems that act under uncertainty. Popular algorithms are policy iteration and variants of value iteration; in tool competitions, most participants rely on the latter. These algorithms generally need worst-case exponential time. However, the problem can equally be formulated as a linear programme, solvable in polynomial time. In this paper, we give a detailed overview of today’s state-of-the-art algorithms for MDP model checking with a focus on performance and correctness. We highlight their fundamental differences, and describe various optimizations and implementation variants. We experimentally compare floating-point and exact-arithmetic implementations of all algorithms on three benchmark sets using two probabilistic model checkers. Our results show that (optimistic) value iteration is a sensible default, but other algorithms are preferable in specific settings. This paper thereby provides a guide for MDP verification practitioners—tool builders and users alike.}, author = {Hartmanns, Arnd and Junges, Sebastian and Quatmann, Tim and Weininger, Maximilian}, issn = {1433-2787}, journal = {International Journal on Software Tools for Technology Transfer}, keywords = {Quantitative model checking, Markov decision process, Linear programming, Value iteration, Policy iteration}, publisher = {Springer Nature}, title = {{The revised practitioner’s guide to MDP model checking algorithms}}, doi = {10.1007/s10009-026-00848-y}, year = {2026}, } @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}, } @inproceedings{21722, abstract = {Partially observable Markov decision processes (POMDPs) are a central model for uncertainty in sequential decision making. The most basic objective is the reachability objective, where a target set must be eventually visited, and the more general parity objectives can model all omega-regular specifications. For such objectives, the computational analysis problems are the following: (a) qualitative analysis that asks whether the objective can be satisfied with probability 1 (almost-sure winning) or probability arbitrarily close to 1 (limit-sure winning); and (b) quantitative analysis that asks for the approximation of the optimal probability of satisfying the objective. For general POMDPs, almost-sure analysis for reachability objectives is EXPTIME-complete, but limit-sure and quantitative analyses for reachability objectives are undecidable; almost-sure, limit-sure, and quantitative analyses for parity objectives are all undecidable. A special class of POMDPs, called revealing POMDPs, has been studied recently in several works, and for this subclass the almost-sure analysis for parity objectives was shown to be EXPTIME-complete. In this work, we show that for revealing POMDPs the limit-sure analysis for parity objectives is EXPTIME-complete, and even the quantitative analysis for parity objectives can be achieved in EXPTIME.}, author = {Asadi, Ali and Chatterjee, Krishnendu and Lurie, David and Saona Urmeneta, Raimundo J}, booktitle = {Proceedings of the AAAI Conference on Artificial Intelligence}, issn = {2374-3468}, location = {Singapore, Singapore}, number = {43}, pages = {36146--36154}, publisher = {Association for the Advancement of Artificial Intelligence}, title = {{Revealing POMDPs: Qualitative and quantitative analysis for parity objectives}}, doi = {10.1609/aaai.v40i43.40932}, volume = {40}, year = {2026}, } @article{18529, abstract = {Temporal networks are obtained from time-dependent interactions among individuals, whereas the interactions can be emails, phone calls, face-to-face meetings, or work collaboration. In this article, a temporal game framework is established, in which interactions among rational individuals are embedded into two-player games in a time-dependent manner. This allows studying the time-dependent complexity and variability of interactions, and the way they affect prosocial behaviors. Based on this simple mathematical model, it is found that the level of cooperation is promoted when the time of collaboration is equally limited for every individual. This observation is confirmed by a series of systematic human experiments on over 1,400 subjects, forming a foundation for comprehensively describing human temporal interactions in collaboration. The research results reveal an important incentive for human cooperation, leading to a better understanding of a fascinating aspect of human nature in society.}, author = {Zhang, Yichao and Wang, Jiasheng and Wen, Guanghui and Guan, Jihong and Zhou, Shuigeng and Chen, Guanrong and Chatterjee, Krishnendu and Perc, Matjaz}, issn = {2327-4697}, journal = {IEEE Transactions on Network Science and Engineering}, number = {1}, pages = {4--12}, publisher = {IEEE}, title = {{Limitation of time promotes cooperation in structured collaboration systems}}, doi = {10.1109/TNSE.2024.3481434}, volume = {12}, year = {2025}, } @article{19965, abstract = {Multiagent learning is challenging when agents face mixed-motivation interactions, where conflicts of interest arise as agents independently try to optimize their respective outcomes. Recent advancements in evolutionary game theory have identified a class of “zero-determinant” strategies, which confer an agent with significant unilateral control over outcomes in repeated games. Building on these insights, we present a comprehensive generalization of zero-determinant strategies to stochastic games, encompassing dynamic environments. We propose an algorithm that allows an agent to discover strategies enforcing predetermined linear (or approximately linear) payoff relationships. Of particular interest is the relationship in which both payoffs are equal, which serves as a proxy for fairness in symmetric games. We demonstrate that an agent can discover strategies enforcing such relationships through experience alone, without coordinating with an opponent. In finding and using such a strategy, an agent (“enforcer”) can incentivize optimal and equitable outcomes, circumventing potential exploitation. In particular, from the opponent’s viewpoint, the enforcer transforms a mixed-motivation problem into a cooperative problem, paving the way for more collaboration and fairness in multiagent systems.}, author = {Mcavoy, Alex and Sehwag, Udari Madhushani and Hilbe, Christian and Chatterjee, Krishnendu and Barfuss, Wolfram and Su, Qi and Leonard, Naomi Ehrich and Plotkin, Joshua B.}, issn = {1091-6490}, journal = {Proceedings of the National Academy of Sciences}, number = {25}, publisher = {National Academy of Sciences}, title = {{Unilateral incentive alignment in two-agent stochastic games}}, doi = {10.1073/pnas.2319927121}, volume = {122}, year = {2025}, } @inproceedings{20053, abstract = {Liquid democracy is a transitive vote delegation mechanism over voting graphs. It enables each voter to delegate their vote(s) to another better-informed voter, with the goal of collectively making a better decision. The question of whether liquid democracy outperforms direct voting has been previously studied in the context of local delegation mechanisms (where voters can only delegate to someone in their neighbourhood) and binary decision problems. It has previously been shown that it is impossible for local delegation mechanisms to outperform direct voting in general graphs. This raises the question: for which classes of graphs do local delegation mechanisms yield good results? In this work, we analyse (1) properties of specific graphs and (2) properties of local delegation mechanisms on these graphs, determining where local delegation actually outperforms direct voting. We show that a critical graph property enabling liquid democracy is that the voting outcome of local delegation mechanisms preserves a sufficient amount of variance, thereby avoiding situations where delegation falls behind direct voting1. These insights allow us to prove our main results, namely that there exist local delegation mechanisms that perform no worse and in fact quantitatively better than direct voting in natural graph topologies like complete, random d-regular, and bounded degree graphs, lending a more nuanced perspective to previous impossibility results.}, author = {Chatterjee, Krishnendu and Gilbert, Seth and Schmid, Stefan and Svoboda, Jakub and Yeo, Michelle X}, booktitle = {Proceedings of the ACM Symposium on Principles of Distributed Computing}, isbn = {9798400718854}, location = {Huatulco, Mexico}, pages = {241--251}, publisher = {Association for Computing Machinery}, title = {{When is liquid democracy possible?: On the manipulation of variance}}, doi = {10.1145/3732772.3733544}, year = {2025}, } @inproceedings{20297, abstract = {A standard model that arises in several applications in sequential decision-making is partially observable Markov decision processes (POMDPs) where a decision-making agent interacts with an uncertain environment. A basic objective in POMDPs is the reachability objective, where given a target set of states, the goal is to eventually arrive at one of them. The limit-sure problem asks whether reachability can be ensured with probability arbitrarily close to 1. In general, the limit-sure reachability problem for POMDPs is undecidable. However, in many practical cases, the most relevant question is the existence of policies with a small amount of memory. In this work, we study the limit-sure reachability problem for POMDPs with a fixed amount of memory. We establish that the computational complexity of the problem is NP-complete.}, author = {Asadi, Ali and Chatterjee, Krishnendu and Saona Urmeneta, Raimundo J and Shafiee, Ali}, booktitle = {The 41st Conference on Uncertainty in Artificial Intelligence}, issn = {2640-3498}, location = {Rio de Janeiro, Brazil}, pages = {238--247}, publisher = {ML Research Press}, title = {{Limit-sure reachability for small memory policies in POMDPs is NP-complete}}, volume = {286}, year = {2025}, } @inproceedings{20299, abstract = {Deterministic Markov Decision Processes (DMDPs) are a mathematical framework for decision-making where the outcomes and future possible actions are deterministically determined by the current action taken. DMDPs can be viewed as a finite directed weighted graph, where in each step, the controller chooses an outgoing edge. An objective is a measurable function on runs (or infinite trajectories) of the DMDP, and the value for an objective is the maximal cumulative reward (or weight) that the controller can guarantee. We consider the classical mean-payoff (aka limit-average) objective, which is a basic and fundamental objective. Howard's policy iteration algorithm is a popular method for solving DMDPs with mean-payoff objectives. Although Howard's algorithm performs well in practice, as experimental studies suggested, the best known upper bound is exponential and the current known lower bound is as follows: For the input size I, the algorithm requires (math formular) iterations, where (math formular) hides the poly-logarithmic factors, i.e., the current lower bound on iterations is sub-linear with respect to the input size. Our main result is an improved lower bound for this fundamental algorithm where we show that for the input size I, the algorithm requires (math formular) iterations.}, author = {Asadi, Ali and Chatterjee, Krishnendu and De Raaij, Jakob}, booktitle = {The 41st Conference on Uncertainty in Artificial Intelligence}, issn = {2640-3498}, location = {Rio de Janeiro, Brazil}, pages = {223--232}, publisher = {ML Research Press}, title = {{Lower bound on Howard policy iteration for deterministic Markov Decision Processes}}, volume = {286}, year = {2025}, } @inproceedings{20302, abstract = {LocalSGD and SCAFFOLD are widely used methods in distributed stochastic optimization, with numerous applications in machine learning, large-scale data processing, and federated learning. However, rigorously establishing their theoretical advantages over simpler methods, such as minibatch SGD (MbSGD), has proven challenging, as existing analyses often rely on strong assumptions, unrealistic premises, or overly restrictive scenarios. In this work, we revisit the convergence properties of LocalSGD and SCAFFOLD under a variety of existing or weaker conditions, including gradient similarity, Hessian similarity, weak convexity, and Lipschitz continuity of the Hessian. Our analysis shows that (i) LocalSGD achieves faster convergence compared to MbSGD for weakly convex functions without requiring stronger gradient similarity assumptions; (ii) LocalSGD benefits significantly from higher-order similarity and smoothness; and (iii) SCAFFOLD demonstrates faster convergence than MbSGD for a broader class of non-quadratic functions. These theoretical insights provide a clearer understanding of the conditions under which LocalSGD and SCAFFOLD outperform MbSGD.}, author = {Luo, Ruichen and Stich, Sebastian U. and Horváth, Samuel and Takáč, Martin}, booktitle = {The 28th International Conference on Artificial Intelligence and Statistics}, issn = {2640-3498}, location = {Mai Khao, Thailand}, pages = {2539--2547}, publisher = {ML Research Press}, title = {{Revisiting LocalSGD and SCAFFOLD: Improved rates and missing analysis}}, volume = {258}, year = {2025}, } @inproceedings{20610, abstract = {Markov decision processes (MDPs) are a fundamental model of decision making which exhibit non-deterministic choice as well as probabilistic uncertainty. Traditionally, verification assumes exact knowledge of the probabilities that govern the behaviour of an MDP. However, this assumption often is unrealistic, e.g. when modelling cyber-physical systems or biological processes. There, we can employ statistical model checking (SMC) to obtain an estimate of the MDP’s value (e.g. the maximal probability of reaching a goal state) that is close to the true value with high confidence (probably approximately correct). Model-based SMC algorithms sample the MDP and build a model of it by estimating all transition probabilities, essentially for every transition answering the question: “What are the odds?” However, so far the statistical methods employed by state-of-the-art SMC verification algorithms are quite naive or even compromise the correctness guarantees. Our first contribution is to survey, categorize, and analyse statistical methods, identifying those few that are most efficient and that provide suitable guarantees for the verification setting. Secondly, we propose improvements that exploit structural knowledge of the MDP. Both contributions generalize to many types of problem statements as they are largely independent of the setting. Moreover, our experimental evaluation shows that they lead to significant gains, reducing the number of samples that an SMC algorithm has to collect by up to two orders of magnitude.}, author = {Meggendorfer, Tobias and Weininger, Maximilian and Wienhöft, Patrick}, booktitle = {Second International Joint Conference on QEST+FORMATS}, isbn = {9783032057914}, issn = {1611-3349}, location = {Aarhus, Denmark}, pages = {195--218}, publisher = {Springer Nature}, title = {{What are the odds? Improving statistical model checking of Markov decision processes}}, doi = {10.1007/978-3-032-05792-1_11}, volume = {16143}, 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{20688, abstract = {We consider two-player zero-sum concurrent stochastic games (CSGs) played on graphs with reachability and safety objectives. These include degenerate classes such as Markov decision processes or turn-based stochastic games, which can be solved by linear or quadratic programming; however, in practice, value iteration (VI) outperforms the other approaches and is the most implemented method. Similarly, for CSGs, this practical performance makes VI an attractive alternative to the standard theoretical solution via the existential theory of reals.VI starts with an under-approximation of the sought values for each state and iteratively updates them, traditionally terminating once two consecutive approximations are ϵ-close. However, this stopping criterion lacks guarantees on the precision of the approximation, which is the goal of this work. We provide bounded (a.k.a. interval) VI for CSGs: it complements standard VI with a converging sequence of over-approximations and terminates once the over- and under-approximations are ϵ-close.}, author = {Grobelna, Marta and Kretinsky, Jan and Weininger, Maximilian}, booktitle = {2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science}, location = {Singapore, Singapore}, pages = {568--580}, publisher = {IEEE}, title = {{Stopping criteria for value iteration on concurrent stochastic reachability and safety games}}, doi = {10.1109/lics65433.2025.00049}, year = {2025}, } @inproceedings{20689, abstract = {This paper studies the expected value of multiplicative rewards, where rewards obtained in each step are multiplied (instead of the usual addition), in Markov chains (MCs) and Markov decision processes (MDPs). One of the key differences to additive rewards is that the expected value may diverge to ∞ not only due to recurrent, but also due to transient states.For MCs, computing the value is shown to be possible in polynomial time given an oracle for the comparison of succinctly represented integers (CSRI), which is only known to be solvable in polynomial time subject to number-theoretic conjectures. Interestingly, distinguishing whether the value is ∞ or 0 is at least as hard as CSRI, while determining if it is one of these two can be done in polynomial time. In MDPs, the optimal value can be computed in polynomial space. Further refined complexity results and results on the complexity of optimal schedulers are presented. The techniques developed for MDPs additionally allow to solve the multiplicative variant of the stochastic shortest path problem. Finally, for MCs and MDPs where an absorbing state is reached almost surely, all considered problems are solvable in polynomial time.}, author = {Baier, Christel and Chatterjee, Krishnendu and Meggendorfer, Tobias and Piribauer, Jakob}, booktitle = {2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science}, location = {Singapore, Singapore}, pages = {499--512}, publisher = {IEEE}, title = {{Multiplicative rewards in Markovian models}}, doi = {10.1109/lics65433.2025.00044}, year = {2025}, } @inproceedings{20690, abstract = {Cumulative prospect theory (CPT) is the first theory for decision-making under uncertainty that combines full theoretical soundness and empirically realistic features [1], [Page 2]. While CPT was originally considered in one-shot settings for risk-aware decision-making, we consider CPT in sequential decision-making. The most fundamental and well-studied models for sequential decision-making are Markov chains (MCs), and their generalization Markov decision processes (MDPs). The complexity theoretic study of MCs and MDPs with CPT is a fundamental problem that has not been addressed in the literature.Our contributions are as follows: First, we present an alternative viewpoint for the CPT-value of MCs and MDPs. This allows us to establish a connection with multi-objective reachability analysis and conclude the strategy complexity result that memoryless randomized strategies are necessary and sufficient for optimality. Second, based on this connection, we provide an algorithm for computing the CPT-value in MDPs with infinite-horizon objectives. We show that the problem is in EXPTIME and fixed-parameter tractable. Moreover, we provide a polynomial-time algorithm for the special case of MCs.}, author = {Brihaye, Thomas and Chatterjee, Krishnendu and Mohr, Stefanie and Weininger, Maximilian}, booktitle = {2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science}, location = {Singapore, Singapore}, pages = {458--471}, publisher = {IEEE}, title = {{Risk-aware Markov decision processes using cumulative prospect theory}}, doi = {10.1109/lics65433.2025.00041}, year = {2025}, } @inproceedings{19375, abstract = {Despite the advances in probabilistic model checking, the scalability of the verification methods remains limited. In particular, the state space often becomes extremely large when instantiating parameterized Markov decision processes (MDPs) even with moderate values. Synthesizing policies for such huge MDPs is beyond the reach of available tools. We propose a learning-based approach to obtain a reasonable policy for such huge MDPs. The idea is to generalize optimal policies obtained by model-checking small instances to larger ones using decision-tree learning. Consequently, our method bypasses the need for explicit state-space exploration of large models, providing a practical solution to the state-space explosion problem. We demonstrate the efficacy of our approach by performing extensive experimentation on the relevant models from the quantitative verification benchmark set. The experimental results indicate that our policies perform well, even when the size of the model is orders of magnitude beyond the reach of state-of-the-art analysis tools.}, author = {Azeem, Muqsit and Chakraborty, Debraj and Kanav, Sudeep and Kretinsky, Jan and Mohagheghi, Mohammadsadegh and Mohr, Stefanie and Weininger, Maximilian}, booktitle = {26th International Conference on Verification, Model Checking, and Abstract Interpretation}, isbn = {9783031827020}, issn = {1611-3349}, location = {Denver, CO, United States}, pages = {97--120}, publisher = {Springer Nature}, title = {{1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization}}, doi = {10.1007/978-3-031-82703-7_5}, volume = {15530}, year = {2025}, } @inproceedings{19445, abstract = {In reconfiguration, we are given two solutions to a graph problem, such as Vertex Cover or Dominating Set, with each solution represented by a placement of tokens on vertices of the graph. Our task is to reconfigure one into the other using small steps while ensuring the intermediate configurations of tokens are also valid solutions. The two commonly studied settings are Token Jumping and Token Sliding, which allows moving a single token to an arbitrary or an adjacent vertex, respectively. We introduce new rules that generalize Token Jumping, parameterized by the number of tokens allowed to move at once and by the maximum distance of each move. Our main contribution is identifying minimal rules that allow reconfiguring any possible given solution into any other for Independent Set, Vertex Cover, and Dominating Set. For each minimal rule, we also provide an efficient algorithm that finds a corresponding reconfiguration sequence. We further focus on the rule that allows each token to move to an adjacent vertex in a single step. This natural variant turns out to be the minimal rule that guarantees reconfigurability for Vertex Cover. We determine the computational complexity of deciding whether a (shortest) reconfiguration sequence exists under this rule for the three studied problems. While reachability for Vertex Cover is shown to be in P, finding a shortest sequence is shown to be NP-complete. For Independent Set and Dominating Set, even reachability is shown to be PSPACE-complete.}, author = {Křišťan, Jan Matyáš and Svoboda, Jakub}, booktitle = {19th International Conference and Workshops on Algorithms and Computation}, isbn = {9789819628445}, issn = {1611-3349}, location = {Chengdu, China}, pages = {244--265}, publisher = {Springer Nature}, title = {{Reconfiguration using generalized token jumping}}, doi = {10.1007/978-981-96-2845-2_16}, volume = {15411}, year = {2025}, } @inproceedings{19600, abstract = {In this work, we explore route discovery in private payment channel networks. We first determine what “ideal" privacy for a routing protocol means in this setting. We observe that protocols achieving this strong privacy definition exist by leveraging Multi-Party Computation but they are inherently inefficient as they must involve the entire network. We then present protocols with weaker privacy guarantees but much better efficiency (involving only a small fraction of the nodes). The core idea is that both sender and receiver gossip a message which propagates through the network, and the moment any node in the network receives both messages, a path is found. In our first protocol the message is always sent to all neighbouring nodes with a delay proportional to the fees of that edge. In our second protocol the message is only sent to one neighbour chosen randomly with a probability proportional to its degree. We additionally propose a more realistic notion of privacy in order to measure the privacy leakage of our protocols in practice. Our realistic notion of privacy challenges an adversary that join the network with a fixed budget to create channels to guess the sender and receiver of a transaction upon receiving messages from our protocols. Simulations of our protocols on the Lightning network topology (for random transactions and uniform fees) show that 1) forming edges with high degree nodes is a more effective attack strategy for the adversary, 2) there is a tradeoff between the number of nodes involved in our protocols (privacy) and the optimality of the discovered path, and 3) our protocols involve a very small fraction of the network on average.}, author = {Avarikioti, Zeta and Bastankhah, Mahsa and Maddah-Ali, Mohammad Ali and Pietrzak, Krzysztof Z and Svoboda, Jakub and Yeo, Michelle X}, booktitle = {Computer Security. ESORICS 2024 International Workshops}, isbn = {9783031823480}, issn = {1611-3349}, location = {Bydgoszcz, Poland}, pages = {207--223}, publisher = {Springer Nature}, title = {{Route discovery in private payment channel networks}}, doi = {10.1007/978-3-031-82349-7_15}, volume = {15263}, year = {2025}, } @inproceedings{19666, abstract = {Markov decision processes (MDP) are a well-established model for sequential decision-making in the presence of probabilities. In *robust* MDP (RMDP), every action is associated with an *uncertainty set* of probability distributions, modelling that transition probabilities are not known precisely. Based on the known theoretical connection to stochastic games, we provide a framework for solving RMDPs that is generic, reliable, and efficient. It is *generic* both with respect to the model, allowing for a wide range of uncertainty sets, including but not limited to intervals, L1- or L2-balls, and polytopes; and with respect to the objective, including long-run average reward, undiscounted total reward, and stochastic shortest path. It is *reliable*, as our approach not only converges in the limit, but provides precision guarantees at any time during the computation. It is *efficient* because -- in contrast to state-of-the-art approaches -- it avoids explicitly constructing the underlying stochastic game. Consequently, our prototype implementation outperforms existing tools by several orders of magnitude and can solve RMDPs with a million states in under a minute.}, author = {Meggendorfer, Tobias and Weininger, Maximilian and Wienhöft, Patrick}, booktitle = {Proceedings of the 39th AAAI Conference on Artificial Intelligence}, issn = {2374-3468}, location = {Philadelphia, PA, United States}, number = {25}, pages = {26631--26641}, publisher = {Association for the Advancement of Artificial Intelligence}, title = {{Solving robust Markov decision processes: Generic, reliable, efficient}}, doi = {10.1609/aaai.v39i25.34865}, volume = {39}, 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}, }