[{"publication":"38th Conference on Neural Information Processing Systems","title":"MICROADAM: Accurate adaptive optimization with low space overhead and provable convergence","alternative_title":["Advances in Neural Information Processing Systems"],"day":"20","date_published":"2024-12-20T00:00:00Z","fulldoi":"https://doi.org/10.52202/079017-0001","oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":"1","publication_identifier":{"issn":["1049-5258"]},"related_material":{"link":[{"url":"https://github.com/IST-DASLab/MicroAdam","relation":"software"}]},"corr_author":"1","arxiv":1,"year":"2024","_id":"19510","oa_version":"Preprint","language":[{"iso":"eng"}],"acknowledged_ssus":[{"_id":"CampIT"}],"acknowledgement":"The authors thank Razvan Pascanu, Mahdi Nikdan and Soroush Tabesh for their valuable feedback, the IT department from Institute of Science and Technology Austria for the hardware support and Weights and Biases for the infrastructure to track all our experiments. Mher Safaryan has received funding from the European Union’s Horizon 2020 research and innovation program under the Marie Sklodowska-Curie grant agreement No 101034413.","volume":37,"type":"conference","external_id":{"arxiv":["2405.15593"]},"quality_controlled":"1","status":"public","OA_place":"repository","OA_type":"green","date_created":"2025-04-06T22:01:32Z","date_updated":"2026-10-15T09:49:27Z","publication_status":"published","month":"12","ec_funded":1,"project":[{"call_identifier":"H2020","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program"}],"publisher":"Neural Information Processing Systems Foundation","department":[{"_id":"DaAl"}],"article_processing_charge":"No","abstract":[{"lang":"eng","text":"We propose a new variant of the Adam optimizer [Kingma and Ba, 2014] called\r\nMICROADAM that specifically minimizes memory overheads, while maintaining\r\ntheoretical convergence guarantees. We achieve this by compressing the gradient\r\ninformation before it is fed into the optimizer state, thereby reducing its memory\r\nfootprint significantly. We control the resulting compression error via a novel\r\ninstance of the classical error feedback mechanism from distributed optimization [Seide et al., 2014, Alistarh et al., 2018, Karimireddy et al., 2019] in which\r\nthe error correction information is itself compressed to allow for practical memory\r\ngains. We prove that the resulting approach maintains theoretical convergence\r\nguarantees competitive to those of AMSGrad, while providing good practical performance. Specifically, we show that MICROADAM can be implemented efficiently\r\non GPUs: on both million-scale (BERT) and billion-scale (LLaMA) models, MICROADAM provides practical convergence competitive to that of the uncompressed\r\nAdam baseline, with lower memory usage and similar running time. Our code is\r\navailable at https://github.com/IST-DASLab/MicroAdam."}],"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2405.15593"}],"citation":{"ista":"Modoranu I-V, Safaryan M, Malinovsky G, Kurtic E, Robert T, Richtárik P, Alistarh D-A. 2024. MICROADAM: Accurate adaptive optimization with low space overhead and provable convergence. 38th Conference on Neural Information Processing Systems. , Advances in Neural Information Processing Systems, vol. 37.","short":"I.-V. Modoranu, M. Safaryan, G. Malinovsky, E. Kurtic, T. Robert, P. Richtárik, D.-A. Alistarh, in:, 38th Conference on Neural Information Processing Systems, Neural Information Processing Systems Foundation, 2024.","chicago":"Modoranu, Ionut-Vlad, Mher Safaryan, Grigory Malinovsky, Eldar Kurtic, Thomas Robert, Peter Richtárik, and Dan-Adrian Alistarh. “MICROADAM: Accurate Adaptive Optimization with Low Space Overhead and Provable Convergence.” In 38th Conference on Neural Information Processing Systems, Vol. 37. Neural Information Processing Systems Foundation, 2024. https://doi.org/10.52202/079017-0001.","ama":"Modoranu I-V, Safaryan M, Malinovsky G, et al. MICROADAM: Accurate adaptive optimization with low space overhead and provable convergence. In: 38th Conference on Neural Information Processing Systems. Vol 37. Neural Information Processing Systems Foundation; 2024. doi:10.52202/079017-0001","apa":"Modoranu, I.-V., Safaryan, M., Malinovsky, G., Kurtic, E., Robert, T., Richtárik, P., & Alistarh, D.-A. (2024). MICROADAM: Accurate adaptive optimization with low space overhead and provable convergence. In 38th Conference on Neural Information Processing Systems (Vol. 37). Neural Information Processing Systems Foundation. https://doi.org/10.52202/079017-0001","ieee":"I.-V. Modoranu et al., “MICROADAM: Accurate adaptive optimization with low space overhead and provable convergence,” in 38th Conference on Neural Information Processing Systems, 2024, vol. 37.","mla":"Modoranu, Ionut-Vlad, et al. “MICROADAM: Accurate Adaptive Optimization with Low Space Overhead and Provable Convergence.” 38th Conference on Neural Information Processing Systems, vol. 37, Neural Information Processing Systems Foundation, 2024, doi:10.52202/079017-0001."},"doi":"10.52202/079017-0001","intvolume":" 37","author":[{"id":"449f7a18-f128-11eb-9611-9b430c0c6333","last_name":"Modoranu","first_name":"Ionut-Vlad","full_name":"Modoranu, Ionut-Vlad"},{"first_name":"Mher","full_name":"Safaryan, Mher","id":"dd546b39-0804-11ed-9c55-ef075c39778d","last_name":"Safaryan"},{"last_name":"Malinovsky","full_name":"Malinovsky, Grigory","first_name":"Grigory"},{"last_name":"Kurtic","id":"47beb3a5-07b5-11eb-9b87-b108ec578218","first_name":"Eldar","full_name":"Kurtic, Eldar"},{"full_name":"Robert, Thomas","first_name":"Thomas","id":"de632733-1457-11f0-ae22-b5914b8c1c41","last_name":"Robert"},{"last_name":"Richtárik","first_name":"Peter","full_name":"Richtárik, Peter"},{"first_name":"Dan-Adrian","full_name":"Alistarh, Dan-Adrian","orcid":"0000-0003-3650-940X","id":"4A899BFC-F248-11E8-B48F-1D18A9856A87","last_name":"Alistarh"}]},{"publication_status":"published","date_updated":"2026-10-15T09:50:59Z","issue":"20","project":[{"name":"Center for Correlated Quantum Materials and Solid State Quantum Systems: Scale- invariance in entangled quantum spin systems","grant_number":"F8607","_id":"34ac8b51-11ca-11ed-8bc3-86c15daa9f8f"}],"month":"11","quality_controlled":"1","supplementarymaterial":"yes","external_id":{"arxiv":["2312.03080"],"isi":["001447562900001"]},"OA_type":"green","das_tickbox":"0","date_created":"2024-12-15T23:01:50Z","OA_place":"repository","status":"public","citation":{"ista":"Sato T, Ramshaw BJ, Modic KA, Assaad FF. 2024. Scale-invariant magnetic anisotropy in α-RuCl3: A quantum Monte Carlo study. Physical Review B. 110(20), L201114.","short":"T. Sato, B.J. Ramshaw, K.A. Modic, F.F. Assaad, Physical Review B 110 (2024).","apa":"Sato, T., Ramshaw, B. J., Modic, K. A., & Assaad, F. F. (2024). Scale-invariant magnetic anisotropy in α-RuCl3: A quantum Monte Carlo study. Physical Review B. American Physical Society. https://doi.org/10.1103/PhysRevB.110.L201114","ama":"Sato T, Ramshaw BJ, Modic KA, Assaad FF. Scale-invariant magnetic anisotropy in α-RuCl3: A quantum Monte Carlo study. Physical Review B. 2024;110(20). doi:10.1103/PhysRevB.110.L201114","ieee":"T. Sato, B. J. Ramshaw, K. A. Modic, and F. F. Assaad, “Scale-invariant magnetic anisotropy in α-RuCl3: A quantum Monte Carlo study,” Physical Review B, vol. 110, no. 20. American Physical Society, 2024.","chicago":"Sato, Toshihiro, B. J. Ramshaw, Kimberly A Modic, and Fakher F. Assaad. “Scale-Invariant Magnetic Anisotropy in α-RuCl3: A Quantum Monte Carlo Study.” Physical Review B. American Physical Society, 2024. https://doi.org/10.1103/PhysRevB.110.L201114.","mla":"Sato, Toshihiro, et al. “Scale-Invariant Magnetic Anisotropy in α-RuCl3: A Quantum Monte Carlo Study.” Physical Review B, vol. 110, no. 20, L201114, American Physical Society, 2024, doi:10.1103/PhysRevB.110.L201114."},"author":[{"first_name":"Toshihiro","full_name":"Sato, Toshihiro","last_name":"Sato"},{"full_name":"Ramshaw, B. J.","first_name":"B. J.","last_name":"Ramshaw"},{"last_name":"Modic","id":"13C26AC0-EB69-11E9-87C6-5F3BE6697425","orcid":"0000-0001-9760-3147","full_name":"Modic, Kimberly A","first_name":"Kimberly A"},{"first_name":"Fakher F.","full_name":"Assaad, Fakher F.","last_name":"Assaad"}],"doi":"10.1103/PhysRevB.110.L201114","intvolume":" 110","publisher":"American Physical Society","abstract":[{"lang":"eng","text":"We compute the rotational anisotropy of the free energy of 𝛼−RuCl3 in an external magnetic field. This quantity, known as the magnetotropic susceptibility, 𝑘, relates to the second derivative of the free energy with respect to the angle of rotation. We have used approximation-free, auxiliary-field quantum Monte Carlo simulations for a realistic model of 𝛼−RuCl3 and optimized the path integral to alleviate the negative sign problem. This allows us to reach temperatures down to 30K—an energy scale below the dominant Kitaev coupling. We demonstrate that the magnetotropic spin susceptibility in this model of 𝛼−RuCl3 displays scaling behavior 𝑘=𝑇𝑓(𝐵/𝑇) at high temperatures. Once the uniform susceptibility departs from the Curie law (i.e., at the energy scale of the exchange interactions), it appears to transition to an emergent scalinglike behavior, characterized by a different function 𝑓 at lower temperatures, stemming from the locality of torque fluctuations. We observe a remarkable numerical match between experiment and simulations and we also find qualitative agreement with the pure Kitaev model. In comparison, for the XXZ Heisenberg Hamiltonian, the scaling 𝑘=𝑇𝑓(𝐵/𝑇) breaks down at a temperature scale where the uniform spin susceptibility deviates from the Curie law and never reemerges at low temperatures."}],"article_processing_charge":"No","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2312.03080"}],"department":[{"_id":"KiMo"}],"isi":1,"oa":1,"date_published":"2024-11-15T00:00:00Z","fulldoi":"https://doi.org/10.1103/PhysRevB.110.L201114","scopus_import":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publication_identifier":{"eissn":["2469-9969"],"issn":["2469-9950"]},"publication":"Physical Review B","researchdata_availability":"no","day":"15","title":"Scale-invariant magnetic anisotropy in α-RuCl3: A quantum Monte Carlo study","article_number":"L201114","acknowledgement":"We gratefully acknowledge the Gauss Centre for Supercomputing e.V. for funding this project by providing computing time on the GCS Supercomputer SUPERMUC-NG at the Leibniz Supercomputing Centre (Project No. pn73xu) as well as the scientific support and HPC resources provided by the Erlangen National High Performance Computing Center (NHR@FAU) of the Friedrich-Alexander-Universität Erlangen-Nürnberg (FAU) under the NHR Project b133ae. NHR funding is provided by federal and Bavarian state authorities. NHR@FAU hardware is partially funded by the German Research Foundation (DFG) – 440719683. T.S. thanks funding from the Deutsche Forschungsgemeinschaft under Grant No. SA 3986/1-1 as well as the Würzburg-Dresden Cluster of Excellence on Complexity and Topology in Quantum Matter ct.qmat (EXC 2147, Project ID 390858490). F.F.A. acknowledges financial support from the German Research Foundation (DFG) under the Grant AS 120/16-1 (Project No. 493886309) that is part of the collaborative research project SFB Q-M&S funded by the Austrian Science Fund (FWF) F 86. K.A.M. thanks financial support from the Austrian Science Fund, SFB F 86, Q-M&S.","language":[{"iso":"eng"}],"type":"journal_article","volume":110,"article_type":"letter_note","arxiv":1,"year":"2024","oa_version":"Preprint","_id":"18654"},{"conference":{"name":"NeurIPS: Neural Information Processing Systems","start_date":"2024-12-09","end_date":"2024-12-15","location":"Vancouver, Canada"},"external_id":{"arxiv":["2404.00456"]},"quality_controlled":"1","status":"public","OA_place":"repository","date_created":"2025-04-06T22:01:32Z","OA_type":"green","date_updated":"2026-10-15T09:50:27Z","publication_status":"published","month":"12","publisher":"Neural Information Processing Systems Foundation","department":[{"_id":"DaAl"}],"abstract":[{"text":"We introduce QuaRot, a new Quantization scheme based on Rotations, which is able to quantize LLMs end-to-end, including all weights, activations, and KV cache in 4 bits. QuaRot rotates LLMs in a way that removes outliers from the hidden state without changing the output, making quantization easier. This computational invariance is applied to the hidden state (residual) of the LLM, as well as to the activations of the feed-forward components, aspects of the attention mechanism, and to the KV cache. The result is a quantized model where all matrix multiplications are performed in 4 bits, without any channels identified for retention in higher precision. Our 4-bit quantized LLAMA2-70B model has losses of at most 0.47 WikiText-2 perplexity and retains 99% of the zero-shot performance. We also show that QuaRot can provide lossless 6 and 8 bit LLAMA-2 models without any calibration data using round-to-nearest quantization. Code is available at github.com/spcl/QuaRot.","lang":"eng"}],"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2404.00456"}],"article_processing_charge":"No","citation":{"short":"S. Ashkboos, A. Mohtashami, M.L. Croci, B. Li, P. Cameron, M. Jaggi, D.-A. Alistarh, T. Hoefler, J. Hensman, in:, 38th Conference on Neural Information Processing Systems, Neural Information Processing Systems Foundation, 2024.","ista":"Ashkboos S, Mohtashami A, Croci ML, Li B, Cameron P, Jaggi M, Alistarh D-A, Hoefler T, Hensman J. 2024. QuaRot: Outlier-free 4-bit inference in rotated LLMs. 38th Conference on Neural Information Processing Systems. NeurIPS: Neural Information Processing Systems, Advances in Neural Information Processing Systems, vol. 37.","chicago":"Ashkboos, Saleh, Amirkeivan Mohtashami, Maximilian L. Croci, Bo Li, Pashmina Cameron, Martin Jaggi, Dan-Adrian Alistarh, Torsten Hoefler, and James Hensman. “QuaRot: Outlier-Free 4-Bit Inference in Rotated LLMs.” In 38th Conference on Neural Information Processing Systems, Vol. 37. Neural Information Processing Systems Foundation, 2024. https://doi.org/10.52202/079017-3180.","ama":"Ashkboos S, Mohtashami A, Croci ML, et al. QuaRot: Outlier-free 4-bit inference in rotated LLMs. In: 38th Conference on Neural Information Processing Systems. Vol 37. Neural Information Processing Systems Foundation; 2024. doi:10.52202/079017-3180","apa":"Ashkboos, S., Mohtashami, A., Croci, M. L., Li, B., Cameron, P., Jaggi, M., … Hensman, J. (2024). QuaRot: Outlier-free 4-bit inference in rotated LLMs. In 38th Conference on Neural Information Processing Systems (Vol. 37). Vancouver, Canada: Neural Information Processing Systems Foundation. https://doi.org/10.52202/079017-3180","ieee":"S. Ashkboos et al., “QuaRot: Outlier-free 4-bit inference in rotated LLMs,” in 38th Conference on Neural Information Processing Systems, Vancouver, Canada, 2024, vol. 37.","mla":"Ashkboos, Saleh, et al. “QuaRot: Outlier-Free 4-Bit Inference in Rotated LLMs.” 38th Conference on Neural Information Processing Systems, vol. 37, Neural Information Processing Systems Foundation, 2024, doi:10.52202/079017-3180."},"intvolume":" 37","doi":"10.52202/079017-3180","author":[{"last_name":"Ashkboos","full_name":"Ashkboos, Saleh","first_name":"Saleh"},{"full_name":"Mohtashami, Amirkeivan","first_name":"Amirkeivan","last_name":"Mohtashami"},{"last_name":"Croci","full_name":"Croci, Maximilian L.","first_name":"Maximilian L."},{"full_name":"Li, Bo","first_name":"Bo","last_name":"Li"},{"first_name":"Pashmina","full_name":"Cameron, Pashmina","last_name":"Cameron"},{"full_name":"Jaggi, Martin","first_name":"Martin","last_name":"Jaggi"},{"full_name":"Alistarh, Dan-Adrian","first_name":"Dan-Adrian","id":"4A899BFC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-3650-940X","last_name":"Alistarh"},{"full_name":"Hoefler, Torsten","first_name":"Torsten","last_name":"Hoefler"},{"full_name":"Hensman, James","first_name":"James","last_name":"Hensman"}],"publication":"38th Conference on Neural Information Processing Systems","title":"QuaRot: Outlier-free 4-bit inference in rotated LLMs","day":"20","alternative_title":["Advances in Neural Information Processing Systems"],"fulldoi":"https://doi.org/10.52202/079017-3180","date_published":"2024-12-20T00:00:00Z","oa":1,"scopus_import":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_identifier":{"issn":["1049-5258"]},"related_material":{"link":[{"relation":"software","url":"https://github.com/spcl/QuaRot"}]},"oa_version":"Preprint","_id":"19511","year":"2024","arxiv":1,"language":[{"iso":"eng"}],"volume":37,"type":"conference"},{"publisher":"American Physical Society","department":[{"_id":"KiMo"}],"article_processing_charge":"No","abstract":[{"text":"Magnetic frustration allows to access novel and intriguing properties of magnetic systems and has been explored mainly in planar triangular-like arrays of magnetic ions. In this work, we describe the phosphide Ce6Ni6P17, where the Ce+3 ions accommodate in a body-centered cubic lattice of Ce6 regular octahedra. From measurements of magnetization, specific heat, and resistivity, we determine a rich phase diagram as a function of temperature and magnetic field in which different magnetic phases are found. Besides clear evidence of magnetic frustration is obtained from entropy analysis. At zero field, a second-order antiferromagnetic transition occurs at TN1≈1 K followed by a first-order transition at TN2≈0.45 K. With magnetic field new magnetic phases appear, including a weakly first-order transition which ends in a classical critical point and a third magnetic phase. We also study the exact solution of the spin-1/2 Heisenberg model in an octahedron which allows us a qualitative understanding of the phase diagram and compare with the experimental results.","lang":"eng"}],"citation":{"apa":"Franco, D. G., Avalos, R., Hafner, D., Modic, K. A., Prots, Y., Stockert, O., … Geibel, C. (2024). Frustrated magnetism in octahedra-based Ce6 Ni6 P17. Physical Review B. American Physical Society. https://doi.org/10.1103/PhysRevB.109.054405","ieee":"D. G. Franco et al., “Frustrated magnetism in octahedra-based Ce6 Ni6 P17,” Physical Review B, vol. 109, no. 5. American Physical Society, 2024.","ama":"Franco DG, Avalos R, Hafner D, et al. Frustrated magnetism in octahedra-based Ce6 Ni6 P17. Physical Review B. 2024;109(5). doi:10.1103/PhysRevB.109.054405","chicago":"Franco, D. G., R. Avalos, D. Hafner, Kimberly A Modic, Yu Prots, O. Stockert, A. Hoser, et al. “Frustrated Magnetism in Octahedra-Based Ce6 Ni6 P17.” Physical Review B. American Physical Society, 2024. https://doi.org/10.1103/PhysRevB.109.054405.","mla":"Franco, D. G., et al. “Frustrated Magnetism in Octahedra-Based Ce6 Ni6 P17.” Physical Review B, vol. 109, no. 5, 054405, American Physical Society, 2024, doi:10.1103/PhysRevB.109.054405.","short":"D.G. Franco, R. Avalos, D. Hafner, K.A. Modic, Y. Prots, O. Stockert, A. Hoser, P.J.W. Moll, M. Brando, A.A. Aligia, C. Geibel, Physical Review B 109 (2024).","ista":"Franco DG, Avalos R, Hafner D, Modic KA, Prots Y, Stockert O, Hoser A, Moll PJW, Brando M, Aligia AA, Geibel C. 2024. Frustrated magnetism in octahedra-based Ce6 Ni6 P17. Physical Review B. 109(5), 054405."},"doi":"10.1103/PhysRevB.109.054405","intvolume":" 109","author":[{"first_name":"D. G.","full_name":"Franco, D. G.","last_name":"Franco"},{"last_name":"Avalos","first_name":"R.","full_name":"Avalos, R."},{"first_name":"D.","full_name":"Hafner, D.","last_name":"Hafner"},{"orcid":"0000-0001-9760-3147","id":"13C26AC0-EB69-11E9-87C6-5F3BE6697425","last_name":"Modic","first_name":"Kimberly A","full_name":"Modic, Kimberly A"},{"last_name":"Prots","first_name":"Yu","full_name":"Prots, Yu"},{"last_name":"Stockert","full_name":"Stockert, O.","first_name":"O."},{"last_name":"Hoser","full_name":"Hoser, A.","first_name":"A."},{"full_name":"Moll, P. J.W.","first_name":"P. J.W.","last_name":"Moll"},{"first_name":"M.","full_name":"Brando, M.","last_name":"Brando"},{"full_name":"Aligia, A. A.","first_name":"A. A.","last_name":"Aligia"},{"first_name":"C.","full_name":"Geibel, C.","last_name":"Geibel"}],"external_id":{"isi":["001198571800008"]},"supplementarymaterial":"yes","quality_controlled":"1","status":"public","date_created":"2024-02-18T23:01:01Z","das_tickbox":"0","date_updated":"2026-10-15T09:50:31Z","issue":"5","publication_status":"published","month":"02","article_type":"original","year":"2024","_id":"15003","oa_version":"None","language":[{"iso":"eng"}],"acknowledgement":"The authors thank Bernardo Pentke for the SEM micrographs (Departamento Fisicoquímica de Materiales CABCNEA). We are indebted to Julián Sereni for useful discussions. D. G. F. acknowledges financial support provided by Agencia I+D+i, Argentina, Grant No. PICT-2021-I-INVI00852 and Universidad Nacional de Cuyo (SIIP) Grant No. 06/C018-T1. A. A. A. acknowledges financial support provided by PICT 2018-01546 and PICT 2020A-03661 of the\r\nAgencia I+D+i. ","volume":109,"type":"journal_article","publication":"Physical Review B","researchdata_availability":"no","title":"Frustrated magnetism in octahedra-based Ce6 Ni6 P17","article_number":"054405","day":"01","date_published":"2024-02-01T00:00:00Z","fulldoi":"https://doi.org/10.1103/PhysRevB.109.054405","isi":1,"scopus_import":"1","publication_identifier":{"eissn":["2469-9969"],"issn":["2469-9950"]},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345"},{"author":[{"full_name":"Hensel, Sebastian","first_name":"Sebastian","id":"4D23B7DA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-7252-8072","last_name":"Hensel"},{"full_name":"Laux, Tim","first_name":"Tim","last_name":"Laux"}],"intvolume":" 73","doi":"10.1512/iumj.2024.73.9701","citation":{"chicago":"Hensel, Sebastian, and Tim Laux. “BV Solutions for Mean Curvature Flow with Constant Angle: Allen-Cahn Approximation and Weak-Strong Uniqueness.” Indiana University Mathematics Journal. Indiana University Mathematics Journal, 2024. https://doi.org/10.1512/iumj.2024.73.9701.","ieee":"S. Hensel and T. Laux, “BV solutions for mean curvature flow with constant angle: Allen-Cahn approximation and weak-strong uniqueness,” Indiana University Mathematics Journal, vol. 73, no. 1. Indiana University Mathematics Journal, pp. 111–148, 2024.","apa":"Hensel, S., & Laux, T. (2024). BV solutions for mean curvature flow with constant angle: Allen-Cahn approximation and weak-strong uniqueness. Indiana University Mathematics Journal. Indiana University Mathematics Journal. https://doi.org/10.1512/iumj.2024.73.9701","ama":"Hensel S, Laux T. BV solutions for mean curvature flow with constant angle: Allen-Cahn approximation and weak-strong uniqueness. Indiana University Mathematics Journal. 2024;73(1):111-148. doi:10.1512/iumj.2024.73.9701","mla":"Hensel, Sebastian, and Tim Laux. “BV Solutions for Mean Curvature Flow with Constant Angle: Allen-Cahn Approximation and Weak-Strong Uniqueness.” Indiana University Mathematics Journal, vol. 73, no. 1, Indiana University Mathematics Journal, 2024, pp. 111–48, doi:10.1512/iumj.2024.73.9701.","ista":"Hensel S, Laux T. 2024. BV solutions for mean curvature flow with constant angle: Allen-Cahn approximation and weak-strong uniqueness. Indiana University Mathematics Journal. 73(1), 111–148.","short":"S. Hensel, T. Laux, Indiana University Mathematics Journal 73 (2024) 111–148."},"abstract":[{"lang":"eng","text":"We study weak solutions to mean curvature flow satisfying Young’s angle condition for general contact angles α ∈ (0, π). First, we construct BV solutions by using the Allen-Cahn approximation with boundary contact energy as proposed by Owen and Sternberg. Second, we prove the weak-strong uniqueness and stability for this solution concept. The main ingredient for both results is a relative energy, which can also be interpreted as a tilt excess. "}],"article_processing_charge":"No","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2112.11150"}],"department":[{"_id":"JuFi"}],"publisher":"Indiana University Mathematics Journal","month":"01","publication_status":"published","issue":"1","date_updated":"2026-10-15T09:49:54Z","date_created":"2025-01-27T15:20:19Z","OA_type":"green","OA_place":"repository","status":"public","quality_controlled":"1","external_id":{"arxiv":["2112.11150"]},"supplementarymaterial":"unclear","type":"journal_article","volume":73,"language":[{"iso":"eng"}],"oa_version":"Preprint","_id":"18926","year":"2024","arxiv":1,"article_type":"original","page":"111-148","corr_author":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","scopus_import":"1","publication_identifier":{"issn":["0022-2518"]},"oa":1,"fulldoi":"https://doi.org/10.1512/iumj.2024.73.9701","date_published":"2024-01-01T00:00:00Z","day":"01","title":"BV solutions for mean curvature flow with constant angle: Allen-Cahn approximation and weak-strong uniqueness","researchdata_availability":"unclear","publication":"Indiana University Mathematics Journal"},{"doi":"10.48550/arXiv.2401.16252","author":[{"last_name":"Attia","full_name":"Attia, Luc","first_name":"Luc"},{"last_name":"Lichev","first_name":"Lyuben","full_name":"Lichev, Lyuben"},{"last_name":"Mitsche","full_name":"Mitsche, Dieter","first_name":"Dieter"},{"first_name":"Raimundo J","full_name":"Saona Urmeneta, Raimundo J","last_name":"Saona Urmeneta","orcid":"0000-0001-5103-038X","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425"},{"first_name":"Bruno","full_name":"Ziliotto, Bruno","last_name":"Ziliotto"}],"citation":{"ista":"Attia L, Lichev L, Mitsche D, Saona Urmeneta RJ, Ziliotto B. Zero-sum random games on directed graphs. arXiv, 2401.16252.","short":"L. Attia, L. Lichev, D. Mitsche, R.J. Saona Urmeneta, B. Ziliotto, ArXiv (n.d.).","mla":"Attia, Luc, et al. “Zero-Sum Random Games on Directed Graphs.” ArXiv, 2401.16252, doi:10.48550/arXiv.2401.16252.","chicago":"Attia, Luc, Lyuben Lichev, Dieter Mitsche, Raimundo J Saona Urmeneta, and Bruno Ziliotto. “Zero-Sum Random Games on Directed Graphs.” ArXiv, n.d. https://doi.org/10.48550/arXiv.2401.16252.","ama":"Attia L, Lichev L, Mitsche D, Saona Urmeneta RJ, Ziliotto B. Zero-sum random games on directed graphs. arXiv. doi:10.48550/arXiv.2401.16252","apa":"Attia, L., Lichev, L., Mitsche, D., Saona Urmeneta, R. J., & Ziliotto, B. (n.d.). Zero-sum random games on directed graphs. arXiv. https://doi.org/10.48550/arXiv.2401.16252","ieee":"L. Attia, L. Lichev, D. Mitsche, R. J. Saona Urmeneta, and B. Ziliotto, “Zero-sum random games on directed graphs,” arXiv. ."},"department":[{"_id":"KrCh"}],"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2401.16252"}],"article_processing_charge":"No","abstract":[{"lang":"eng","text":"This paper considers a class of two-player zero-sum games on directed graphs whose vertices are equipped with random payoffs of bounded support known by both players.\r\nStarting from a fixed vertex, players take turns to move a token along the edges of the graph.\r\nOn the one hand, for acyclic directed graphs of bounded degree and sub-exponential expansion, we show that the value of the game converges almost surely to a constant at an exponential rate dominated in terms of the expansion.\r\nOn the other hand, for the infinite d-ary tree that does not fall into the previous class of graphs, we show convergence at a double-exponential rate in terms of the expansion."}],"month":"01","date_updated":"2026-10-15T09:51:45Z","publication_status":"submitted","status":"public","das_tickbox":"0","date_created":"2024-06-03T07:45:22Z","supplementarymaterial":"no","external_id":{"arxiv":["2401.16252"]},"type":"preprint","language":[{"iso":"eng"}],"acknowledgement":"This work was supported by the French Agence Nationale de la Recherche (ANR) under references ANR-21-CE40-0020 (CONVERGENCE project) and ANR-20-CE40-0002 (GrHyDy), and by Fondecyt grant 1220174. This collaboration was mainly conducted during a 1-year visit of Bruno Ziliotto to the Center for Mathematical Modeling (CMM) at University of Chile in 2023,\r\nunder the IRL program of CNRS.","_id":"17101","oa_version":"Preprint","arxiv":1,"year":"2024","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","fulldoi":"https://doi.org/10.48550/arXiv.2401.16252","date_published":"2024-01-29T00:00:00Z","oa":1,"title":"Zero-sum random games on directed graphs","article_number":"2401.16252","day":"29","publication":"arXiv","researchdata_availability":"no"},{"language":[{"iso":"eng"}],"acknowledgement":"This work was partially funded by the Academy of Finland, grant 314888, the European Research Council CoG 863818 (ForM-SMArt), and the Austrian Science Fund (FWF) project I 4800-N (ADVISE). LS was supported by the Stochastic Analysis and Application Research Center (SAARC) under National Research Foundation of Korea grant NRF-2019R1A5A1028324.","volume":286,"file":[{"date_created":"2024-02-26T09:04:58Z","success":1,"creator":"dernst","file_size":867363,"content_type":"application/pdf","checksum":"4fc7eea6e4ba140b904781fc7df868ec","access_level":"open_access","file_id":"15028","date_updated":"2024-02-26T09:04:58Z","file_name":"2024_LIPICs_Hirvonen.pdf","relation":"main_file"}],"type":"conference","_id":"15006","oa_version":"Published Version","arxiv":1,"year":"2024","fulldoi":"https://doi.org/10.4230/LIPIcs.OPODIS.2023.11","date_published":"2024-01-18T00:00:00Z","oa":1,"isi":1,"scopus_import":"1","publication_identifier":{"issn":["1868-8969"],"isbn":["9783959773089"]},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"corr_author":"1","researchdata_availability":"no","publication":"27th International Conference on Principles of Distributed Systems","title":"On the convergence time in graphical games: A locality-sensitive approach","article_number":"11","day":"18","alternative_title":["LIPIcs"],"ddc":["000"],"citation":{"short":"J. Hirvonen, L. Schmid, K. Chatterjee, S. Schmid, in:, 27th International Conference on Principles of Distributed Systems, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.","ista":"Hirvonen J, Schmid L, Chatterjee K, Schmid S. 2024. On the convergence time in graphical games: A locality-sensitive approach. 27th International Conference on Principles of Distributed Systems. OPODIS: Conference on Principles of Distributed Systems, LIPIcs, vol. 286, 11.","mla":"Hirvonen, Juho, et al. “On the Convergence Time in Graphical Games: A Locality-Sensitive Approach.” 27th International Conference on Principles of Distributed Systems, vol. 286, 11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:10.4230/LIPIcs.OPODIS.2023.11.","chicago":"Hirvonen, Juho, Laura Schmid, Krishnendu Chatterjee, and Stefan Schmid. “On the Convergence Time in Graphical Games: A Locality-Sensitive Approach.” In 27th International Conference on Principles of Distributed Systems, Vol. 286. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. https://doi.org/10.4230/LIPIcs.OPODIS.2023.11.","ieee":"J. Hirvonen, L. Schmid, K. Chatterjee, and S. Schmid, “On the convergence time in graphical games: A locality-sensitive approach,” in 27th International Conference on Principles of Distributed Systems, Tokyo, Japan, 2024, vol. 286.","ama":"Hirvonen J, Schmid L, Chatterjee K, Schmid S. On the convergence time in graphical games: A locality-sensitive approach. In: 27th International Conference on Principles of Distributed Systems. Vol 286. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:10.4230/LIPIcs.OPODIS.2023.11","apa":"Hirvonen, J., Schmid, L., Chatterjee, K., & Schmid, S. (2024). On the convergence time in graphical games: A locality-sensitive approach. In 27th International Conference on Principles of Distributed Systems (Vol. 286). Tokyo, Japan: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.OPODIS.2023.11"},"intvolume":" 286","doi":"10.4230/LIPIcs.OPODIS.2023.11","author":[{"full_name":"Hirvonen, Juho","first_name":"Juho","last_name":"Hirvonen"},{"first_name":"Laura","full_name":"Schmid, Laura","last_name":"Schmid","orcid":"0000-0002-6978-7329","id":"38B437DE-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Schmid","full_name":"Schmid, Stefan","first_name":"Stefan"}],"has_accepted_license":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"KrCh"}],"file_date_updated":"2024-02-26T09:04:58Z","article_processing_charge":"No","abstract":[{"text":"Graphical games are a useful framework for modeling the interactions of (selfish) agents who are connected via an underlying topology and whose behaviors influence each other. They have wide applications ranging from computer science to economics and biology. Yet, even though an agent’s payoff only depends on the actions of their direct neighbors in graphical games, computing the Nash equilibria and making statements about the convergence time of \"natural\" local dynamics in particular can be highly challenging. In this work, we present a novel approach for classifying complexity of Nash equilibria in graphical games by establishing a connection to local graph algorithms, a subfield of distributed computing. In particular, we make the observation that the equilibria of graphical games are equivalent to locally verifiable labelings (LVL) in graphs; vertex labelings which are verifiable with constant-round local algorithms. This connection allows us to derive novel lower bounds on the convergence time to equilibrium of best-response dynamics in graphical games. Since we establish that distributed convergence can sometimes be provably slow, we also introduce and give bounds on an intuitive notion of \"time-constrained\" inefficiency of best responses. We exemplify how our results can be used in the implementation of mechanisms that ensure convergence of best responses to a Nash equilibrium. Our results thus also give insight into the convergence of strategy-proof algorithms for graphical games, which is still not well understood.","lang":"eng"}],"date_updated":"2026-10-15T10:07:37Z","publication_status":"published","ec_funded":1,"month":"01","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"}],"conference":{"location":"Tokyo, Japan","end_date":"2023-12-08","start_date":"2023-12-06","name":"OPODIS: Conference on Principles of Distributed Systems"},"supplementarymaterial":"no","external_id":{"arxiv":["2102.13457"],"isi":["001585185800011"]},"quality_controlled":"1","status":"public","das_tickbox":"0","date_created":"2024-02-18T23:01:01Z"},{"has_accepted_license":"1","publisher":"Springer Nature","file_date_updated":"2024-08-12T08:39:12Z","department":[{"_id":"KrCh"}],"abstract":[{"text":"We present version 2.0 of the Partial Exploration Tool (PET), a tool for verification of probabilistic systems. We extend the previous version by adding support for stochastic games, based on a recent unified framework for sound value iteration algorithms. Thereby, PET2 is the first tool implementing a sound and efficient approach for solving stochastic games with objectives of the type reachability/safety and mean payoff. We complement this approach by developing and implementing a partial-exploration based variant for all three objectives. Our experimental evaluation shows that PET2 offers the most efficient partial-exploration based algorithm and is the most viable tool on SGs, even outperforming unsound tools.","lang":"eng"}],"article_processing_charge":"Yes (in subscription journal)","citation":{"ista":"Meggendorfer T, Weininger M. 2024. Playing games with your PET: Extending the Partial Exploration Tool to stochastic games. 36th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 14683, 359–372.","short":"T. Meggendorfer, M. Weininger, in:, 36th International Conference on Computer Aided Verification, Springer Nature, 2024, pp. 359–372.","chicago":"Meggendorfer, Tobias, and Maximilian Weininger. “Playing Games with Your PET: Extending the Partial Exploration Tool to Stochastic Games.” In 36th International Conference on Computer Aided Verification, 14683:359–72. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-65633-0_16.","ieee":"T. Meggendorfer and M. Weininger, “Playing games with your PET: Extending the Partial Exploration Tool to stochastic games,” in 36th International Conference on Computer Aided Verification, Montreal, Canada, 2024, vol. 14683, pp. 359–372.","ama":"Meggendorfer T, Weininger M. Playing games with your PET: Extending the Partial Exploration Tool to stochastic games. In: 36th International Conference on Computer Aided Verification. Vol 14683. Springer Nature; 2024:359-372. doi:10.1007/978-3-031-65633-0_16","apa":"Meggendorfer, T., & Weininger, M. (2024). Playing games with your PET: Extending the Partial Exploration Tool to stochastic games. In 36th International Conference on Computer Aided Verification (Vol. 14683, pp. 359–372). Montreal, Canada: Springer Nature. https://doi.org/10.1007/978-3-031-65633-0_16","mla":"Meggendorfer, Tobias, and Maximilian Weininger. “Playing Games with Your PET: Extending the Partial Exploration Tool to Stochastic Games.” 36th International Conference on Computer Aided Verification, vol. 14683, Springer Nature, 2024, pp. 359–72, doi:10.1007/978-3-031-65633-0_16."},"ddc":["000"],"intvolume":" 14683","doi":"10.1007/978-3-031-65633-0_16","author":[{"first_name":"Tobias","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","last_name":"Meggendorfer"},{"orcid":"0000-0002-0163-2152","id":"02ab0197-cc70-11ed-ab61-918e71f56881","last_name":"Weininger","first_name":"Maximilian","full_name":"Weininger, Maximilian"}],"conference":{"end_date":"2024-07-27","name":"CAV: Computer Aided Verification","start_date":"2024-07-24","location":"Montreal, Canada"},"supplementarymaterial":"no","external_id":{"arxiv":["2405.03885"],"isi":["001307897000016"]},"quality_controlled":"1","status":"public","date_created":"2024-08-09T11:24:54Z","das_tickbox":"1","date_updated":"2026-10-15T10:06:48Z","publication_status":"published","ec_funded":1,"month":"07","project":[{"call_identifier":"H2020","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","name":"IST-BRIDGE: International postdoctoral program","grant_number":"101034413"}],"oa_version":"Published Version","_id":"17402","arxiv":1,"year":"2024","language":[{"iso":"eng"}],"acknowledgement":"M. Weininger has received funding from the EU’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 101034413.","dataavailabilitystatement":"We refer to the artefact with the exact code used for the submission and all logs [31], and the gitlab with the continually developed source code [30].","volume":14683,"type":"conference","file":[{"date_created":"2024-08-12T08:39:12Z","success":1,"content_type":"application/pdf","access_level":"open_access","checksum":"c888231d0a47b55786b7b4c0f02216bb","creator":"dernst","file_size":368487,"file_name":"2024_CAV_Meggendorfer.pdf","relation":"main_file","file_id":"17419","date_updated":"2024-08-12T08:39:12Z"}],"publication":"36th International Conference on Computer Aided Verification","researchdata_availability":"yes","title":"Playing games with your PET: Extending the Partial Exploration Tool to stochastic games","alternative_title":["LNCS"],"day":"01","fulldoi":"https://doi.org/10.1007/978-3-031-65633-0_16","date_published":"2024-07-01T00:00:00Z","oa":1,"isi":1,"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publication_identifier":{"issn":["0302-9743"],"eisbn":["9783031656330"],"eissn":["1611-3349"],"isbn":["9783031656323"]},"scopus_import":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"page":"359-372","corr_author":"1"},{"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"related_material":{"record":[{"id":"23140","relation":"research_data","status":"public"}]},"publication_identifier":{"eissn":["2475-1421"]},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","scopus_import":"1","oa":1,"fulldoi":"https://doi.org/10.1145/3649824","date_published":"2024-04-29T00:00:00Z","day":"29","article_number":"107","title":"Quantitative bounds on resource usage of probabilistic programs","publication":"Proceedings of the ACM on Programming Languages","researchdata_availability":"yes","file":[{"content_type":"application/pdf","access_level":"open_access","checksum":"9243ded966f71df1572be5466019be5c","creator":"dernst","file_size":413096,"relation":"main_file","file_name":"2024_ProcACMProgLanguage_Chatterjee.pdf","file_id":"17182","date_updated":"2024-06-27T07:48:16Z","date_created":"2024-06-27T07:48:16Z","success":1}],"type":"journal_article","volume":8,"acknowledgement":"This work was supported in part by the European Research Council (ERC) under Grant No. 863818\r\n(ForM-SMArt) and the Hong Kong Research Grants Council under ECS Project No. 26208122.","dataavailabilitystatement":"The software that supports Section 8 is available on Zenodo [Meggendorfer and Žikelić 2024]. https://doi.org/10.5281/zenodo.10457566","language":[{"iso":"eng"}],"_id":"17162","oa_version":"Published Version","year":"2024","article_type":"original","project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"ec_funded":1,"month":"04","publication_status":"published","issue":"OOPSLA1","date_updated":"2026-10-15T10:02:32Z","date_created":"2024-06-23T22:01:02Z","das_tickbox":"1","status":"public","quality_controlled":"1","supplementarymaterial":"no","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"first_name":"Amir Kafshdar","full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87","last_name":"Goharshady"},{"first_name":"Tobias","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","last_name":"Meggendorfer"},{"full_name":"Zikelic, Dorde","first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","last_name":"Zikelic"}],"intvolume":" 8","doi":"10.1145/3649824","citation":{"short":"K. Chatterjee, A.K. Goharshady, T. Meggendorfer, D. Zikelic, Proceedings of the ACM on Programming Languages 8 (2024).","ista":"Chatterjee K, Goharshady AK, Meggendorfer T, Zikelic D. 2024. Quantitative bounds on resource usage of probabilistic programs. Proceedings of the ACM on Programming Languages. 8(OOPSLA1), 107.","mla":"Chatterjee, Krishnendu, et al. “Quantitative Bounds on Resource Usage of Probabilistic Programs.” Proceedings of the ACM on Programming Languages, vol. 8, no. OOPSLA1, 107, Association for Computing Machinery, 2024, doi:10.1145/3649824.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Tobias Meggendorfer, and Dorde Zikelic. “Quantitative Bounds on Resource Usage of Probabilistic Programs.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2024. https://doi.org/10.1145/3649824.","apa":"Chatterjee, K., Goharshady, A. K., Meggendorfer, T., & Zikelic, D. (2024). Quantitative bounds on resource usage of probabilistic programs. Proceedings of the ACM on Programming Languages. Association for Computing Machinery. https://doi.org/10.1145/3649824","ama":"Chatterjee K, Goharshady AK, Meggendorfer T, Zikelic D. Quantitative bounds on resource usage of probabilistic programs. Proceedings of the ACM on Programming Languages. 2024;8(OOPSLA1). doi:10.1145/3649824","ieee":"K. Chatterjee, A. K. Goharshady, T. Meggendorfer, and D. Zikelic, “Quantitative bounds on resource usage of probabilistic programs,” Proceedings of the ACM on Programming Languages, vol. 8, no. OOPSLA1. Association for Computing Machinery, 2024."},"ddc":["000"],"article_processing_charge":"Yes (in subscription journal)","abstract":[{"text":"Cost analysis, also known as resource usage analysis, is the task of finding bounds on the total cost of a program and is a well-studied problem in static analysis. In this work, we consider two classical quantitative problems in cost analysis for probabilistic programs. The first problem is to find a bound on the expected total cost of the program. This is a natural measure for the resource usage of the program and can also be directly applied to average-case runtime analysis. The second problem asks for a tail bound, i.e. given a threshold t the goal is to find a probability bound p such that ℙ[total cost ≥ t] ≤ p. Intuitively, given a threshold t on the resource, the problem is to find the likelihood that the total cost exceeds this threshold.\r\nFirst, for expectation bounds, a major obstacle in previous works on cost analysis is that they can handle only non-negative costs or bounded variable updates. In contrast, we provide a new variant of the standard notion of cost martingales, that allows us to find expectation bounds for a class of programs with general positive or negative costs and no restriction on the variable updates. More specifically, our approach is applicable as long as there is a lower bound on the total cost incurred along every path.\r\nSecond, for tail bounds, all previous methods are limited to programs in which the expected total cost is finite. In contrast, we present a novel approach, based on a combination of our martingale-based method for expectation bounds with a quantitative safety analysis, to obtain a solution to the tail bound problem that is applicable even to programs with infinite expected cost. Specifically, this allows us to obtain runtime tail bounds for programs that do not terminate almost-surely.\r\nIn summary, we provide a novel combination of martingale-based cost analysis and quantitative safety analysis that is able to find expectation and tail cost bounds for probabilistic programs, without the restrictions of non-negative costs, bounded updates, or finiteness of the expected total cost. Finally, we provide experimental results showcasing that our approach can solve instances that were beyond the reach of previous methods.","lang":"eng"}],"file_date_updated":"2024-06-27T07:48:16Z","department":[{"_id":"KrCh"}],"publisher":"Association for Computing Machinery","has_accepted_license":"1"},{"publisher":"Neural Information Processing Systems Foundation","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2406.03802","open_access":"1"}],"abstract":[{"text":"Differential privacy with gradual expiration models the setting where data items\r\narrive in a stream and at a given time t the privacy loss guaranteed for a data item\r\nseen at time (t − d) is εg(d), where g is a monotonically non-decreasing function.\r\nWe study the fundamental continual (binary) counting problem where each data\r\nitem consists of a bit, and the algorithm needs to output at each time step the sum of\r\nall the bits streamed so far. For a stream of length T and privacy without expiration\r\ncontinual counting is possible with maximum (over all time steps) additive error\r\nO(log2\r\n(T)/ε) and the best known lower bound is Ω(log(T)/ε); closing this gap\r\nis a challenging open problem.\r\nWe show that the situation is very different for privacy with gradual expiration by\r\ngiving upper and lower bounds for a large set of expiration functions g. Specifically,\r\nour algorithm achieves an additive error of O(log(T)/ε) for a large set of privacy\r\nexpiration functions. We also give a lower bound that shows that if C is the additive\r\nerror of any ε-DP algorithm for this problem, then the product of C and the privacy\r\nexpiration function after 2C steps must be Ω(log(T)/ε). Our algorithm matches\r\nthis lower bound as its additive error is O(log(T)/ε), even when g(2C) = O(1).\r\nOur empirical evaluation shows that we achieve a slowly growing privacy loss\r\nwith significantly smaller empirical privacy loss for large values of d than a natural\r\nbaseline algorithm.","lang":"eng"}],"article_processing_charge":"No","department":[{"_id":"MoHe"}],"citation":{"chicago":"Andersson, Joel Daniel, Monika Henzinger, Rasmus Pagh, Teresa Anna Steiner, and Jalaj Upadhyay. “Continual Counting with Gradual Privacy Expiration.” In 38th Conference on Neural Information Processing Systems, Vol. 37. Neural Information Processing Systems Foundation, 2024. https://doi.org/10.52202/079017-0299.","ama":"Andersson JD, Henzinger M, Pagh R, Steiner TA, Upadhyay J. Continual counting with gradual privacy expiration. In: 38th Conference on Neural Information Processing Systems. Vol 37. Neural Information Processing Systems Foundation; 2024. doi:10.52202/079017-0299","ieee":"J. D. Andersson, M. Henzinger, R. Pagh, T. A. Steiner, and J. Upadhyay, “Continual counting with gradual privacy expiration,” in 38th Conference on Neural Information Processing Systems, Vancouver, Canada, 2024, vol. 37.","apa":"Andersson, J. D., Henzinger, M., Pagh, R., Steiner, T. A., & Upadhyay, J. (2024). Continual counting with gradual privacy expiration. In 38th Conference on Neural Information Processing Systems (Vol. 37). Vancouver, Canada: Neural Information Processing Systems Foundation. https://doi.org/10.52202/079017-0299","mla":"Andersson, Joel Daniel, et al. “Continual Counting with Gradual Privacy Expiration.” 38th Conference on Neural Information Processing Systems, vol. 37, Neural Information Processing Systems Foundation, 2024, doi:10.52202/079017-0299.","short":"J.D. Andersson, M. Henzinger, R. Pagh, T.A. Steiner, J. Upadhyay, in:, 38th Conference on Neural Information Processing Systems, Neural Information Processing Systems Foundation, 2024.","ista":"Andersson JD, Henzinger M, Pagh R, Steiner TA, Upadhyay J. 2024. Continual counting with gradual privacy expiration. 38th Conference on Neural Information Processing Systems. NeurIPS: Neural Information Processing Systems, Advances in Neural Information Processing Systems, vol. 37."},"author":[{"last_name":"Andersson","first_name":"Joel Daniel","full_name":"Andersson, Joel Daniel"},{"full_name":"Henzinger, Monika H","first_name":"Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530","last_name":"Henzinger"},{"first_name":"Rasmus","full_name":"Pagh, Rasmus","last_name":"Pagh"},{"first_name":"Teresa Anna","full_name":"Steiner, Teresa Anna","last_name":"Steiner"},{"last_name":"Upadhyay","full_name":"Upadhyay, Jalaj","first_name":"Jalaj"}],"doi":"10.52202/079017-0299","intvolume":" 37","quality_controlled":"1","external_id":{"arxiv":["2406.03802"]},"conference":{"start_date":"2024-12-09","name":"NeurIPS: Neural Information Processing Systems","end_date":"2024-12-15","location":"Vancouver, Canada"},"OA_type":"green","date_created":"2025-04-06T22:01:32Z","OA_place":"repository","status":"public","publication_status":"published","date_updated":"2026-10-15T09:52:07Z","project":[{"call_identifier":"H2020","name":"The design and evaluation of modern fully dynamic data structures","grant_number":"101019564","_id":"bd9ca328-d553-11ed-ba76-dc4f890cfe62"},{"name":"Efficient algorithms","grant_number":"Z00422","_id":"34def286-11ca-11ed-8bc3-da5948e1613c"},{"name":"Static and Dynamic Hierarchical Graph Decompositions","grant_number":"I05982","_id":"bda196b2-d553-11ed-ba76-8e8ee6c21103"},{"name":"Fast Algorithms for a Reactive Network Layer","grant_number":"P33775","_id":"bd9e3a2e-d553-11ed-ba76-8aa684ce17fe"}],"ec_funded":1,"month":"12","year":"2024","arxiv":1,"oa_version":"Preprint","_id":"19512","acknowledgement":"Monika Henzinger: This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (Grant agreement No. 101019564) and the Austrian Science Fund (FWF) grant DOI 10.55776/Z422, grant DOI 10.55776/I5982, and grant DOI 10.55776/P33775 with additional funding from the netidee SCIENCE Stiftung, 2020–2024. Joel Daniel Andersson and Rasmus Pagh are affiliated with Basic Algorithms Research Copenhagen (BARC), supported by the VILLUM Foundation grant 16582, and are also supported by Providentia, a Data Science Distinguished Investigator grant from Novo Nordisk Fonden. Teresa Anna Steiner is supported by a research grant (VIL51463) from VILLUM FONDEN. This work was done while Teresa Anna Steiner was a Postdoc at the Technical University of Denmark. Jalaj Upadhyay’s research was funded by the Rutgers Decanal Grant no. 302918 and an unrestricted gift from Google.","language":[{"iso":"eng"}],"type":"conference","volume":37,"publication":"38th Conference on Neural Information Processing Systems","day":"20","alternative_title":["Advances in Neural Information Processing Systems"],"title":"Continual counting with gradual privacy expiration","oa":1,"date_published":"2024-12-20T00:00:00Z","fulldoi":"https://doi.org/10.52202/079017-0299","corr_author":"1","publication_identifier":{"eissn":["1049-5258"]},"scopus_import":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"title":"Latent functional maps: A spectral framework for representation alignment","day":"20","alternative_title":["Advances in Neural Information Processing Systems"],"publication":"38th Conference on Neural Information Processing Systems","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_identifier":{"eissn":["1049-5258"]},"scopus_import":"1","corr_author":"1","date_published":"2024-12-20T00:00:00Z","fulldoi":"https://doi.org/10.52202/079017-2115","oa":1,"arxiv":1,"year":"2024","_id":"19515","oa_version":"Preprint","volume":37,"type":"conference","language":[{"iso":"eng"}],"acknowledgement":"MF is supported by the MSCA IST-Bridge fellowship which has received funding from the European Union’s Horizon 2020 research and innovation program under the Marie Skłodowska-Curie grant agreement No 101034413. ER and VM are supported by the PNRR MUR project PE0000013-FAIR. MP is supported by the Sapienza grant \"Predicting and Explaining Clinical Trial Outcomes\", prot. RG12218166FA3F13.","status":"public","OA_place":"repository","OA_type":"green","date_created":"2025-04-06T22:01:32Z","external_id":{"arxiv":["2406.14183"]},"conference":{"start_date":"2024-12-09","name":"NeurIPS: Neural Information Processing Systems","end_date":"2024-12-15","location":"Vancouver, Canada"},"quality_controlled":"1","month":"12","ec_funded":1,"project":[{"call_identifier":"H2020","grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c"}],"date_updated":"2026-10-15T09:52:55Z","publication_status":"published","department":[{"_id":"FrLo"}],"abstract":[{"lang":"eng","text":"Neural models learn data representations that lie on low-dimensional manifolds,\r\nyet modeling the relation between these representational spaces is an ongoing challenge. By integrating spectral geometry principles into neural modeling, we show\r\nthat this problem can be better addressed in the functional domain, mitigating complexity, while enhancing interpretability and performances on downstream tasks.\r\nTo this end, we introduce a multi-purpose framework to the representation learning\r\ncommunity, which allows to: (i) compare different spaces in an interpretable way\r\nand measure their intrinsic similarity; (ii) find correspondences between them, both\r\nin unsupervised and weakly supervised settings, and (iii) to effectively transfer\r\nrepresentations between distinct spaces. We validate our framework on various\r\napplications, ranging from stitching to retrieval tasks, and on multiple modalities,\r\ndemonstrating that Latent Functional Maps can serve as a swiss-army knife for\r\nrepresentation alignment"}],"article_processing_charge":"No","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2406.14183","open_access":"1"}],"publisher":"Neural Information Processing Systems Foundation","doi":"10.52202/079017-2115","intvolume":" 37","author":[{"last_name":"Fumero","id":"1c1593eb-393f-11ef-bb8e-ab4f1e979650","full_name":"Fumero, Marco","first_name":"Marco"},{"full_name":"Pegoraro, Marco","first_name":"Marco","last_name":"Pegoraro"},{"last_name":"Maiorca","full_name":"Maiorca, Valentino","first_name":"Valentino"},{"first_name":"Francesco","full_name":"Locatello, Francesco","last_name":"Locatello","orcid":"0000-0002-4850-0683","id":"26cfd52f-2483-11ee-8040-88983bcc06d4"},{"last_name":"Rodolà","first_name":"Emanuele","full_name":"Rodolà, Emanuele"}],"citation":{"short":"M. Fumero, M. Pegoraro, V. Maiorca, F. Locatello, E. Rodolà, in:, 38th Conference on Neural Information Processing Systems, Neural Information Processing Systems Foundation, 2024.","ista":"Fumero M, Pegoraro M, Maiorca V, Locatello F, Rodolà E. 2024. Latent functional maps: A spectral framework for representation alignment. 38th Conference on Neural Information Processing Systems. NeurIPS: Neural Information Processing Systems, Advances in Neural Information Processing Systems, vol. 37.","mla":"Fumero, Marco, et al. “Latent Functional Maps: A Spectral Framework for Representation Alignment.” 38th Conference on Neural Information Processing Systems, vol. 37, Neural Information Processing Systems Foundation, 2024, doi:10.52202/079017-2115.","chicago":"Fumero, Marco, Marco Pegoraro, Valentino Maiorca, Francesco Locatello, and Emanuele Rodolà. “Latent Functional Maps: A Spectral Framework for Representation Alignment.” In 38th Conference on Neural Information Processing Systems, Vol. 37. Neural Information Processing Systems Foundation, 2024. https://doi.org/10.52202/079017-2115.","ieee":"M. Fumero, M. Pegoraro, V. Maiorca, F. Locatello, and E. Rodolà, “Latent functional maps: A spectral framework for representation alignment,” in 38th Conference on Neural Information Processing Systems, Vancouver, Canada, 2024, vol. 37.","ama":"Fumero M, Pegoraro M, Maiorca V, Locatello F, Rodolà E. Latent functional maps: A spectral framework for representation alignment. In: 38th Conference on Neural Information Processing Systems. Vol 37. Neural Information Processing Systems Foundation; 2024. doi:10.52202/079017-2115","apa":"Fumero, M., Pegoraro, M., Maiorca, V., Locatello, F., & Rodolà, E. (2024). Latent functional maps: A spectral framework for representation alignment. In 38th Conference on Neural Information Processing Systems (Vol. 37). Vancouver, Canada: Neural Information Processing Systems Foundation. https://doi.org/10.52202/079017-2115"}},{"status":"public","OA_place":"repository","title":"Artefact for: Quantitative Bounds on Resource Usage of Probabilistic Programs","date_created":"2026-10-15T10:02:22Z","contributor":[{"first_name":"Tobias","last_name":"Meggendorfer","contributor_type":"contact_person"}],"day":"05","OA_type":"green","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","month":"03","related_material":{"record":[{"id":"17162","relation":"used_in_publication","status":"public"}]},"fulldoi":"https://doi.org/10.5281/zenodo.10457565","date_updated":"2026-10-15T10:02:33Z","date_published":"2024-03-05T00:00:00Z","oa":1,"department":[{"_id":"KrCh"}],"_id":"23140","abstract":[{"lang":"eng","text":"The artefact for the OOPSLA 2024 paper \"Quantitative Bounds on Resource Usage of Probabilistic Programs\".\r\n\r\n"}],"article_processing_charge":"No","main_file_link":[{"url":"https://doi.org/10.5281/zenodo.10457565","open_access":"1"}],"oa_version":"None","year":"2024","publisher":"Zenodo","doi":"10.5281/zenodo.10457565","author":[{"full_name":" Žikelić, Đorđe","first_name":"Đorđe","last_name":" Žikelić"}],"type":"research_data_reference","ddc":["000"],"citation":{"chicago":" Žikelić, Đorđe. “Artefact for: Quantitative Bounds on Resource Usage of Probabilistic Programs.” Zenodo, 2024. https://doi.org/10.5281/zenodo.10457565.","ama":" Žikelić Đ. Artefact for: Quantitative Bounds on Resource Usage of Probabilistic Programs. 2024. doi:10.5281/zenodo.10457565","apa":" Žikelić, Đ. (2024). Artefact for: Quantitative Bounds on Resource Usage of Probabilistic Programs. Zenodo. https://doi.org/10.5281/zenodo.10457565","ieee":"Đ. Žikelić, “Artefact for: Quantitative Bounds on Resource Usage of Probabilistic Programs.” Zenodo, 2024.","mla":" Žikelić, Đorđe. Artefact for: Quantitative Bounds on Resource Usage of Probabilistic Programs. Zenodo, 2024, doi:10.5281/zenodo.10457565.","short":"Đ. Žikelić, (2024).","ista":" Žikelić Đ. 2024. Artefact for: Quantitative Bounds on Resource Usage of Probabilistic Programs, Zenodo, 10.5281/zenodo.10457565."}},{"year":"2024","_id":"15083","oa_version":"Published Version","article_type":"original","file":[{"file_id":"15109","date_updated":"2024-03-12T13:12:22Z","file_name":"2024_PNAS_Huebner.pdf","relation":"main_file","creator":"dernst","file_size":2203220,"content_type":"application/pdf","checksum":"068520e3efd4d008bb9177e8aedb7d22","access_level":"open_access","success":1,"date_created":"2024-03-12T13:12:22Z"}],"type":"journal_article","volume":121,"pmid":1,"acknowledgement":"This work was supported by the European Research Council CoG 863818 (ForM-SMArt) (to K.C.) and the European Research Council Starting Grant 850529: E-DIRECT (to C.H.), the European Union’s Horizon 2020 research and innovation program under the Marie Skłodowska-Curie Grant Agreement #754411 and the French Agence Nationale de la Recherche (under the Investissement d’Avenir Programme, ANR-17-EURE-0010) (to M.K.).","dataavailabilitystatement":"Figures are based on simulation averages over many independent runs of the respective simulation. Results were analyzed and visualized with Python and Matlab R2023a. The computer code is published in (65). All other data are included in the manuscript and/or SI Appendix.","language":[{"iso":"eng"}],"day":"05","article_number":"e2315558121","title":"Efficiency and resilience of cooperation in asymmetric social dilemmas","researchdata_availability":"yes","publication":"Proceedings of the National Academy of Sciences of the United States of America","related_material":{"link":[{"relation":"press_release","description":"News on ISTA Website","url":"https://ista.ac.at/en/news/what-math-tells-us-about-social-dilemmas/"}],"record":[{"relation":"research_data","id":"15108","status":"public"},{"id":"19903","relation":"dissertation_contains","status":"public"}]},"corr_author":"1","tmp":{"short":"CC BY-NC-ND (4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","image":"/images/cc_by_nc_nd.png","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)"},"publication_identifier":{"eissn":["1091-6490"],"issn":["0027-8424"]},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","scopus_import":"1","isi":1,"oa":1,"date_published":"2024-03-05T00:00:00Z","fulldoi":"https://doi.org/10.1073/pnas.2315558121","abstract":[{"lang":"eng","text":"Direct reciprocity is a powerful mechanism for cooperation in social dilemmas. The very logic of reciprocity, however, seems to require that individuals are symmetric, and that everyone has the same means to influence each others’ payoffs. Yet in many applications, individuals are asymmetric. Herein, we study the effect of asymmetry in linear public good games. Individuals may differ in their endowments (their ability to contribute to a public good) and in their productivities (how effective their contributions are). Given the individuals’ productivities, we ask which allocation of endowments is optimal for cooperation. To this end, we consider two notions of optimality. The first notion focuses on the resilience of cooperation. The respective endowment distribution ensures that full cooperation is feasible even under the most adverse conditions. The second notion focuses on efficiency. The corresponding endowment distribution maximizes group welfare. Using analytical methods, we fully characterize these two endowment distributions. This analysis reveals that both optimality notions favor some endowment inequality: More productive players ought to get higher endowments. Yet the two notions disagree on how unequal endowments are supposed to be. A focus on resilience results in less inequality. With additional simulations, we show that the optimal endowment allocation needs to account for both the resilience and the efficiency of cooperation."}],"article_processing_charge":"Yes (in subscription journal)","file_date_updated":"2024-03-12T13:12:22Z","department":[{"_id":"KrCh"}],"publisher":"National Academy of Sciences","has_accepted_license":"1","author":[{"id":"2c8aa207-dc7d-11ea-9b2f-f22972ecd910","orcid":"0009-0001-5009-4987","last_name":"Hübner","full_name":"Hübner, Valentin","first_name":"Valentin"},{"first_name":"Manuel","full_name":"Staab, Manuel","last_name":"Staab"},{"id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5116-955X","last_name":"Hilbe","full_name":"Hilbe, Christian","first_name":"Christian"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"last_name":"Kleshnina","first_name":"Maria","full_name":"Kleshnina, Maria"}],"doi":"10.1073/pnas.2315558121","intvolume":" 121","citation":{"mla":"Hübner, Valentin, et al. “Efficiency and Resilience of Cooperation in Asymmetric Social Dilemmas.” Proceedings of the National Academy of Sciences of the United States of America, vol. 121, no. 10, e2315558121, National Academy of Sciences, 2024, doi:10.1073/pnas.2315558121.","chicago":"Hübner, Valentin, Manuel Staab, Christian Hilbe, Krishnendu Chatterjee, and Maria Kleshnina. “Efficiency and Resilience of Cooperation in Asymmetric Social Dilemmas.” Proceedings of the National Academy of Sciences of the United States of America. National Academy of Sciences, 2024. https://doi.org/10.1073/pnas.2315558121.","apa":"Hübner, V., Staab, M., Hilbe, C., Chatterjee, K., & Kleshnina, M. (2024). Efficiency and resilience of cooperation in asymmetric social dilemmas. Proceedings of the National Academy of Sciences of the United States of America. National Academy of Sciences. https://doi.org/10.1073/pnas.2315558121","ieee":"V. Hübner, M. Staab, C. Hilbe, K. Chatterjee, and M. Kleshnina, “Efficiency and resilience of cooperation in asymmetric social dilemmas,” Proceedings of the National Academy of Sciences of the United States of America, vol. 121, no. 10. National Academy of Sciences, 2024.","ama":"Hübner V, Staab M, Hilbe C, Chatterjee K, Kleshnina M. Efficiency and resilience of cooperation in asymmetric social dilemmas. Proceedings of the National Academy of Sciences of the United States of America. 2024;121(10). doi:10.1073/pnas.2315558121","short":"V. Hübner, M. Staab, C. Hilbe, K. Chatterjee, M. Kleshnina, Proceedings of the National Academy of Sciences of the United States of America 121 (2024).","ista":"Hübner V, Staab M, Hilbe C, Chatterjee K, Kleshnina M. 2024. Efficiency and resilience of cooperation in asymmetric social dilemmas. Proceedings of the National Academy of Sciences of the United States of America. 121(10), e2315558121."},"ddc":["000"],"OA_type":"hybrid","date_created":"2024-03-05T09:18:49Z","das_tickbox":"1","APC_amount":"3041,76 EUR","OA_place":"publisher","status":"public","quality_controlled":"1","supplementarymaterial":"yes","external_id":{"pmid":["38408249"],"isi":["001207786500004"]},"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"},{"call_identifier":"H2020","grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships","_id":"260C2330-B435-11E9-9278-68D0E5697425"}],"month":"03","ec_funded":1,"publication_status":"published","date_updated":"2026-10-15T10:10:26Z","issue":"10"},{"scopus_import":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publication_identifier":{"eissn":["1553-7358"],"issn":["1553-734X"]},"corr_author":"1","related_material":{"record":[{"status":"public","id":"20138","relation":"dissertation_contains"}]},"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"date_published":"2024-03-29T00:00:00Z","fulldoi":"https://doi.org/10.1371/journal.pcbi.1012008","isi":1,"oa":1,"title":"Amplifiers of selection for the Moran process with both Birth-death and death-Birth updating","article_number":"e1012008","day":"29","researchdata_availability":"yes","publication":"PLoS Computational Biology","volume":20,"DOAJ_listed":"1","type":"journal_article","file":[{"date_created":"2024-08-20T10:52:28Z","success":1,"access_level":"open_access","checksum":"a511cf369d9172beb123fe73f291b5cc","content_type":"application/pdf","file_size":1425292,"creator":"dernst","relation":"main_file","file_name":"2024_PloSComBio_Svoboda.pdf","date_updated":"2024-08-20T10:52:28Z","file_id":"17450"}],"language":[{"iso":"eng"}],"acknowledgement":"We thank Gavin Rees for helpful discussions. J.S., S.J., and K.C were supported by\r\nEuropean Research Council (ERC) CoG 863818 (ForM-SMArt). J.T was supported by Center for Foundations of Modern Computer Science (Charles University project UNCE/SCI/004) and by the project PRIMUS/24/SCI/012 from Charles University. ","dataavailabilitystatement":"Code for the figures and the computational experiments is available from the Figshare repository: https://figshare.com/s/4e08d78c892749f84201.","year":"2024","arxiv":1,"oa_version":"Published Version","_id":"15297","article_type":"original","ec_funded":1,"month":"03","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"date_updated":"2026-10-15T12:28:11Z","issue":"3","publication_status":"published","status":"public","OA_place":"publisher","OA_type":"gold","das_tickbox":"1","date_created":"2024-04-07T22:00:55Z","APC_amount":"3149,96 EUR","external_id":{"arxiv":["2401.14914"],"isi":["001194482400002"]},"supplementarymaterial":"yes","quality_controlled":"1","doi":"10.1371/journal.pcbi.1012008","intvolume":" 20","author":[{"id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","orcid":"0000-0002-1419-3267","last_name":"Svoboda","full_name":"Svoboda, Jakub","first_name":"Jakub"},{"full_name":"Joshi, Soham Shrikant","first_name":"Soham Shrikant","last_name":"Joshi","id":"f97aac0e-f57c-11ee-93d0-a5a82d8df168"},{"id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-1097-9684","last_name":"Tkadlec","full_name":"Tkadlec, Josef","first_name":"Josef"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"}],"ddc":["000"],"citation":{"ista":"Svoboda J, Joshi SS, Tkadlec J, Chatterjee K. 2024. Amplifiers of selection for the Moran process with both Birth-death and death-Birth updating. PLoS Computational Biology. 20(3), e1012008.","short":"J. Svoboda, S.S. Joshi, J. Tkadlec, K. Chatterjee, PLoS Computational Biology 20 (2024).","ieee":"J. Svoboda, S. S. Joshi, J. Tkadlec, and K. Chatterjee, “Amplifiers of selection for the Moran process with both Birth-death and death-Birth updating,” PLoS Computational Biology, vol. 20, no. 3. Public Library of Science, 2024.","ama":"Svoboda J, Joshi SS, Tkadlec J, Chatterjee K. Amplifiers of selection for the Moran process with both Birth-death and death-Birth updating. PLoS Computational Biology. 2024;20(3). doi:10.1371/journal.pcbi.1012008","apa":"Svoboda, J., Joshi, S. S., Tkadlec, J., & Chatterjee, K. (2024). Amplifiers of selection for the Moran process with both Birth-death and death-Birth updating. PLoS Computational Biology. Public Library of Science. https://doi.org/10.1371/journal.pcbi.1012008","chicago":"Svoboda, Jakub, Soham Shrikant Joshi, Josef Tkadlec, and Krishnendu Chatterjee. “Amplifiers of Selection for the Moran Process with Both Birth-Death and Death-Birth Updating.” PLoS Computational Biology. Public Library of Science, 2024. https://doi.org/10.1371/journal.pcbi.1012008.","mla":"Svoboda, Jakub, et al. “Amplifiers of Selection for the Moran Process with Both Birth-Death and Death-Birth Updating.” PLoS Computational Biology, vol. 20, no. 3, e1012008, Public Library of Science, 2024, doi:10.1371/journal.pcbi.1012008."},"department":[{"_id":"KrCh"}],"file_date_updated":"2024-08-20T10:52:28Z","abstract":[{"text":"Populations evolve by accumulating advantageous mutations. Every population has some spatial structure that can be modeled by an underlying network. The network then influences the probability that new advantageous mutations fixate. Amplifiers of selection are networks that increase the fixation probability of advantageous mutants, as compared to the unstructured fully-connected network. Whether or not a network is an amplifier depends on the choice of the random process that governs the evolutionary dynamics. Two popular choices are Moran process with Birth-death updating and Moran process with death-Birth updating. Interestingly, while some networks are amplifiers under Birth-death updating and other networks are amplifiers under death-Birth updating, so far no spatial structures have been found that function as an amplifier under both types of updating simultaneously. In this work, we identify networks that act as amplifiers of selection under both versions of the Moran process. The amplifiers are robust, modular, and increase fixation probability for any mutant fitness advantage in a range r ∈ (1, 1.2). To complement this positive result, we also prove that for certain quantities closely related to fixation probability, it is impossible to improve them simultaneously for both versions of the Moran process. Together, our results highlight how the two versions of the Moran process differ and what they have in common.","lang":"eng"}],"article_processing_charge":"Yes","has_accepted_license":"1","publisher":"Public Library of Science"},{"author":[{"last_name":"Hübner","id":"2c8aa207-dc7d-11ea-9b2f-f22972ecd910","orcid":"0009-0001-5009-4987","full_name":"Hübner, Valentin","first_name":"Valentin"},{"full_name":"Kleshnina, Maria","first_name":"Maria","last_name":"Kleshnina"}],"type":"research_data_reference","doi":"10.5281/ZENODO.10639167","ddc":["000"],"citation":{"mla":"Hübner, Valentin, and Maria Kleshnina. Computer Code for “Efficiency and Resilience of Cooperation in Asymmetric Social Dilemmas.” Zenodo, 2024, doi:10.5281/ZENODO.10639167.","ama":"Hübner V, Kleshnina M. Computer code for “Efficiency and resilience of cooperation in asymmetric social dilemmas.” 2024. doi:10.5281/ZENODO.10639167","ieee":"V. Hübner and M. Kleshnina, “Computer code for ‘Efficiency and resilience of cooperation in asymmetric social dilemmas.’” Zenodo, 2024.","apa":"Hübner, V., & Kleshnina, M. (2024). Computer code for “Efficiency and resilience of cooperation in asymmetric social dilemmas.” Zenodo. https://doi.org/10.5281/ZENODO.10639167","chicago":"Hübner, Valentin, and Maria Kleshnina. “Computer Code for ‘Efficiency and Resilience of Cooperation in Asymmetric Social Dilemmas.’” Zenodo, 2024. https://doi.org/10.5281/ZENODO.10639167.","short":"V. Hübner, M. Kleshnina, (2024).","ista":"Hübner V, Kleshnina M. 2024. Computer code for ‘Efficiency and resilience of cooperation in asymmetric social dilemmas’, Zenodo, 10.5281/ZENODO.10639167."},"_id":"15108","main_file_link":[{"url":"https://10.5281/zenodo.10639167","open_access":"1"}],"article_processing_charge":"No","oa_version":"Published Version","abstract":[{"text":"in the research article \"Efficiency and resilience of cooperation in asymmetric social dilemmas\" (by Valentin Hübner, Manuel Staab, Christian Hilbe, Krishnendu Chatterjee, and Maria Kleshnina).\r\n\r\nWe used different implementations for the case of two and three players, both described below.","lang":"eng"}],"year":"2024","department":[{"_id":"KrCh"}],"publisher":"Zenodo","has_accepted_license":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"corr_author":"1","related_material":{"record":[{"status":"public","relation":"used_in_publication","id":"15083"}]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"02","oa":1,"fulldoi":"https://doi.org/10.5281/ZENODO.10639167","date_published":"2024-02-09T00:00:00Z","date_updated":"2026-10-15T10:10:25Z","date_created":"2024-03-12T13:02:58Z","day":"09","status":"public","title":"Computer code for \"Efficiency and resilience of cooperation in asymmetric social dilemmas\""},{"date_published":"2024-09-11T00:00:00Z","fulldoi":"https://doi.org/10.1007/978-3-031-71162-6_31","isi":1,"oa":1,"publication_identifier":{"isbn":["9783031711619"],"eissn":["1611-3349"],"issn":["0302-9743"]},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","scopus_import":"1","corr_author":"1","related_material":{"record":[{"relation":"research_data","id":"22798","status":"public"}]},"page":"600-619","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"publication":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","researchdata_availability":"yes","title":"Sound and complete witnesses for template-based verification of LTL properties on polynomial programs","day":"11","alternative_title":["LNCS"],"language":[{"iso":"eng"}],"acknowledgement":"This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt) and the Hong Kong Research Grants Council ECS Project Number 26208122.","dataavailabilitystatement":"The implementations of the algorithms mentioned in the experiments section and the benchmarks are available at doi.org/10.5281/zenodo.12518217.","volume":14933,"file":[{"date_created":"2024-10-01T09:56:54Z","success":1,"creator":"dernst","file_size":650495,"content_type":"application/pdf","checksum":"223845be9e754681ee218866827c95e7","access_level":"open_access","file_id":"18165","date_updated":"2024-10-01T09:56:54Z","file_name":"2024_LNCS_Chatterjee.pdf","relation":"main_file"}],"type":"conference","year":"2024","arxiv":1,"_id":"18155","oa_version":"Published Version","date_updated":"2026-10-16T07:29:39Z","publication_status":"published","ec_funded":1,"month":"09","project":[{"call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"supplementarymaterial":"no","external_id":{"arxiv":["2403.05386"],"isi":["001336893300031"]},"conference":{"location":"Milan, Italy","end_date":"2024-09-13","start_date":"2024-09-09","name":"FM: Formal Methods"},"quality_controlled":"1","status":"public","date_created":"2024-09-29T22:01:37Z","das_tickbox":"1","citation":{"ieee":"K. Chatterjee, A. K. Goharshady, E. Goharshady, M. Karrabi, and D. Zikelic, “Sound and complete witnesses for template-based verification of LTL properties on polynomial programs,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Milan, Italy, 2024, vol. 14933, pp. 600–619.","ama":"Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Zikelic D. Sound and complete witnesses for template-based verification of LTL properties on polynomial programs. In: Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 14933. Springer Nature; 2024:600-619. doi:10.1007/978-3-031-71162-6_31","apa":"Chatterjee, K., Goharshady, A. K., Goharshady, E., Karrabi, M., & Zikelic, D. (2024). Sound and complete witnesses for template-based verification of LTL properties on polynomial programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 14933, pp. 600–619). Milan, Italy: Springer Nature. https://doi.org/10.1007/978-3-031-71162-6_31","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Ehsan Goharshady, Mehrdad Karrabi, and Dorde Zikelic. “Sound and Complete Witnesses for Template-Based Verification of LTL Properties on Polynomial Programs.” In Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 14933:600–619. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-71162-6_31.","mla":"Chatterjee, Krishnendu, et al. “Sound and Complete Witnesses for Template-Based Verification of LTL Properties on Polynomial Programs.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14933, Springer Nature, 2024, pp. 600–19, doi:10.1007/978-3-031-71162-6_31.","short":"K. Chatterjee, A.K. Goharshady, E. Goharshady, M. Karrabi, D. Zikelic, in:, Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Nature, 2024, pp. 600–619.","ista":"Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Zikelic D. 2024. Sound and complete witnesses for template-based verification of LTL properties on polynomial programs. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). FM: Formal Methods, LNCS, vol. 14933, 600–619."},"ddc":["000"],"doi":"10.1007/978-3-031-71162-6_31","intvolume":" 14933","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Amir Kafshdar","full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87","last_name":"Goharshady"},{"first_name":"Ehsan","full_name":"Goharshady, Ehsan","last_name":"Goharshady"},{"first_name":"Mehrdad","full_name":"Karrabi, Mehrdad","last_name":"Karrabi","orcid":"0009-0007-5253-9170","id":"67638922-f394-11eb-9cf6-f20423e08757"},{"first_name":"Dorde","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic"}],"has_accepted_license":"1","publisher":"Springer Nature","department":[{"_id":"KrCh"}],"file_date_updated":"2024-10-01T09:56:54Z","article_processing_charge":"Yes (in subscription journal)","abstract":[{"text":"We study the classical problem of verifying programs with respect to formal specifications given in the linear temporal logic (LTL). We first present novel sound and complete witnesses for LTL verification over imperative programs. Our witnesses are applicable to both verification (proving) and refutation (finding bugs) settings. We then consider LTL formulas in which atomic propositions can be polynomial constraints and turn our focus to polynomial arithmetic programs, i.e. programs in which every assignment and guard consists only of polynomial expressions. For this setting, we provide an efficient algorithm to automatically synthesize such LTL witnesses. Our synthesis procedure is both sound and semi-complete. Finally, we present experimental results demonstrating the effectiveness of our approach and that it can handle programs which were beyond the reach of previous state-of-the-art tools.","lang":"eng"}]},{"date_created":"2026-09-03T11:50:15Z","OA_type":"green","day":"24","OA_place":"repository","status":"public","title":"Data for Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs","oa":1,"fulldoi":"https://doi.org/10.5281/zenodo.12518216","date_updated":"2026-10-16T07:29:39Z","date_published":"2024-06-24T00:00:00Z","related_material":{"record":[{"id":"18155","relation":"used_in_publication","status":"public"}]},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","month":"06","publisher":"Repository","main_file_link":[{"url":"https://doi.org/10.5281/zenodo.12518216","open_access":"1"}],"_id":"22798","article_processing_charge":"No","oa_version":"None","abstract":[{"text":"This repository contains the artifact of the paper titled \"Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs\" accepted at FM 2024.\r\n\r\nThe task of verifying an LTL formula on a program can be reduced to verifying a Büchi specification on the product transition system. This tool takes a non-deterministic transition system together with a Büchi specification as input and based on user preferences tries to either (i) prove the existence of a run in the program that satisfies the Büchi condition or (ii) demonstrate that every run of the program satisfies the Büchi condition.\r\n \r\nThe tool is written in Java and works well with openjdk 11 on Ubuntu 22.04. Running all the experiments can take weeks to finish. We have provided a script for running the strongest configuration of our tool which solves most of the benchmarks and takes less than 48 hours. Detailed guidance is given in the readme file.","lang":"eng"}],"year":"2024","department":[{"_id":"KrCh"}],"citation":{"ista":"Chatterjee K, Kafshdar Goharshady A, Kafshdar Goharshady E, Karrabi M, Žikelić Ð. 2024. Data for Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs, Repository, 10.5281/zenodo.12518216.","short":"K. Chatterjee, A. Kafshdar Goharshady, E. Kafshdar Goharshady, M. Karrabi, Ð. Žikelić, (2024).","apa":"Chatterjee, K., Kafshdar Goharshady, A., Kafshdar Goharshady, E., Karrabi, M., & Žikelić, Ð. (2024). Data for Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs. Repository. https://doi.org/10.5281/zenodo.12518216","ieee":"K. Chatterjee, A. Kafshdar Goharshady, E. Kafshdar Goharshady, M. Karrabi, and Ð. Žikelić, “Data for Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs.” Repository, 2024.","ama":"Chatterjee K, Kafshdar Goharshady A, Kafshdar Goharshady E, Karrabi M, Žikelić Ð. Data for Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs. 2024. doi:10.5281/zenodo.12518216","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, and Ðorđe Žikelić. “Data for Sound and Complete Witnesses for Template-Based Verification of LTL Properties on Polynomial Programs.” Repository, 2024. https://doi.org/10.5281/zenodo.12518216.","mla":"Chatterjee, Krishnendu, et al. Data for Sound and Complete Witnesses for Template-Based Verification of LTL Properties on Polynomial Programs. Repository, 2024, doi:10.5281/zenodo.12518216."},"ddc":["000"],"author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"full_name":" Kafshdar Goharshady, Amir","first_name":"Amir","last_name":" Kafshdar Goharshady"},{"first_name":"Ehsan","full_name":"Kafshdar Goharshady, Ehsan","last_name":"Kafshdar Goharshady"},{"last_name":"Karrabi","full_name":"Karrabi, Mehrdad","first_name":"Mehrdad"},{"last_name":"Žikelić","full_name":"Žikelić, Ðorđe","first_name":"Ðorđe"}],"type":"research_data_reference","doi":"10.5281/zenodo.12518216"},{"OA_place":"publisher","status":"public","OA_type":"hybrid","APC_amount":"3143,76 EUR","das_tickbox":"1","date_created":"2024-12-22T23:01:47Z","supplementarymaterial":"yes","external_id":{"pmid":["39642209"],"isi":["001379596100014"]},"quality_controlled":"1","month":"12","ec_funded":1,"project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"date_updated":"2026-10-16T08:00:05Z","issue":"50","publication_status":"published","department":[{"_id":"KrCh"}],"file_date_updated":"2025-01-02T12:14:15Z","abstract":[{"lang":"eng","text":"Spatial games provide a simple and elegant mathematical model to study the evolution of cooperation in networks. In spatial games, individuals reside in vertices, adopt simple strategies, and interact with neighbors to receive a payoff. Depending on their own and neighbors’ payoffs, individuals can change their strategy. The payoff is determined by the Prisoners’ Dilemma, a classical matrix game, where players cooperate or defect. While cooperation is the desired behavior, defection provides a higher payoff for a selfish individual. There are many theoretical and empirical studies related to the role of the network in the evolution of cooperation. However, the fundamental question of whether there exist networks that for low initial cooperation rate ensure a high chance of fixation, i.e., cooperation spreads across the whole population, has remained elusive for spatial games with strong selection. In this work, we answer this fundamental question in the affirmative by presenting network structures that ensure high fixation probability for cooperators in the strong selection regime. Besides, our structures have many desirable properties: (a) they ensure the spread of cooperation even for a low initial density of cooperation and high temptation of defection, (b) they have constant degrees, and (c) the number of steps, until cooperation spreads, is at most quadratic in the size of the network."}],"article_processing_charge":"Yes","has_accepted_license":"1","publisher":"National Academy of Sciences","doi":"10.1073/pnas.2405605121","intvolume":" 121","author":[{"orcid":"0000-0002-1419-3267","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","last_name":"Svoboda","first_name":"Jakub","full_name":"Svoboda, Jakub"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"}],"citation":{"short":"J. Svoboda, K. Chatterjee, Proceedings of the National Academy of Sciences of the United States of America 121 (2024).","ista":"Svoboda J, Chatterjee K. 2024. Density amplifiers of cooperation for spatial games. Proceedings of the National Academy of Sciences of the United States of America. 121(50), e2405605121.","mla":"Svoboda, Jakub, and Krishnendu Chatterjee. “Density Amplifiers of Cooperation for Spatial Games.” Proceedings of the National Academy of Sciences of the United States of America, vol. 121, no. 50, e2405605121, National Academy of Sciences, 2024, doi:10.1073/pnas.2405605121.","apa":"Svoboda, J., & Chatterjee, K. (2024). Density amplifiers of cooperation for spatial games. Proceedings of the National Academy of Sciences of the United States of America. National Academy of Sciences. https://doi.org/10.1073/pnas.2405605121","ieee":"J. Svoboda and K. Chatterjee, “Density amplifiers of cooperation for spatial games,” Proceedings of the National Academy of Sciences of the United States of America, vol. 121, no. 50. National Academy of Sciences, 2024.","ama":"Svoboda J, Chatterjee K. Density amplifiers of cooperation for spatial games. Proceedings of the National Academy of Sciences of the United States of America. 2024;121(50). doi:10.1073/pnas.2405605121","chicago":"Svoboda, Jakub, and Krishnendu Chatterjee. “Density Amplifiers of Cooperation for Spatial Games.” Proceedings of the National Academy of Sciences of the United States of America. National Academy of Sciences, 2024. https://doi.org/10.1073/pnas.2405605121."},"ddc":["000"],"article_number":"e2405605121","title":"Density amplifiers of cooperation for spatial games","day":"10","publication":"Proceedings of the National Academy of Sciences of the United States of America","researchdata_availability":"yes","publication_identifier":{"eissn":["1091-6490"],"issn":["0027-8424"]},"scopus_import":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","corr_author":"1","related_material":{"record":[{"relation":"dissertation_contains","id":"20138","status":"public"}]},"tmp":{"short":"CC BY-NC-ND (4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","image":"/images/cc_by_nc_nd.png","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)"},"date_published":"2024-12-10T00:00:00Z","fulldoi":"https://doi.org/10.1073/pnas.2405605121","isi":1,"oa":1,"year":"2024","oa_version":"Published Version","_id":"18703","article_type":"original","volume":121,"type":"journal_article","file":[{"date_created":"2025-01-02T12:14:15Z","success":1,"checksum":"0115e9090b478e0644308c6dab58605b","access_level":"open_access","content_type":"application/pdf","file_size":2491151,"creator":"dernst","file_name":"2024_PNAS_Svoboda.pdf","relation":"main_file","date_updated":"2025-01-02T12:14:15Z","file_id":"18721"}],"language":[{"iso":"eng"}],"pmid":1,"dataavailabilitystatement":"Code data have been deposited in Code: Amplifiers of Cooperation (DOI: https://doi.org/10.5281/zenodo.10832535)","acknowledgement":"J.S. and K.C. were supported by the European Research Council CoG 863818 (ForM-SMArt) and Austrian Science Fund 10.55776/COE12."},{"issue":"4","date_updated":"2026-10-16T07:57:38Z","publication_status":"published","ec_funded":1,"month":"11","project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"supplementarymaterial":"no","external_id":{"isi":["001367316400002"],"arxiv":["2104.07278"]},"quality_controlled":"1","status":"public","OA_place":"publisher","date_created":"2024-12-08T23:01:56Z","das_tickbox":"0","OA_type":"gold","citation":{"ista":"Chatterjee K, Doyen L. 2024. Stochastic processes with expected stopping time. Logical Methods in Computer Science. 20(4), 11:1-11:34.","short":"K. Chatterjee, L. Doyen, Logical Methods in Computer Science 20 (2024) 11:1-11:34.","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Stochastic Processes with Expected Stopping Time.” Logical Methods in Computer Science. EPI Sciences, 2024. https://doi.org/10.46298/lmcs-20(4:11)2024.","apa":"Chatterjee, K., & Doyen, L. (2024). Stochastic processes with expected stopping time. Logical Methods in Computer Science. EPI Sciences. https://doi.org/10.46298/lmcs-20(4:11)2024","ieee":"K. Chatterjee and L. Doyen, “Stochastic processes with expected stopping time,” Logical Methods in Computer Science, vol. 20, no. 4. EPI Sciences, p. 11:1-11:34, 2024.","ama":"Chatterjee K, Doyen L. Stochastic processes with expected stopping time. Logical Methods in Computer Science. 2024;20(4):11:1-11:34. doi:10.46298/lmcs-20(4:11)2024","mla":"Chatterjee, Krishnendu, and Laurent Doyen. “Stochastic Processes with Expected Stopping Time.” Logical Methods in Computer Science, vol. 20, no. 4, EPI Sciences, 2024, p. 11:1-11:34, doi:10.46298/lmcs-20(4:11)2024."},"ddc":["000"],"intvolume":" 20","doi":"10.46298/lmcs-20(4:11)2024","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"first_name":"Laurent","full_name":"Doyen, Laurent","last_name":"Doyen"}],"has_accepted_license":"1","publisher":"EPI Sciences","department":[{"_id":"KrCh"}],"file_date_updated":"2024-12-09T08:38:48Z","abstract":[{"lang":"eng","text":"Markov chains are the de facto finite-state model for stochastic dynamical systems, and Markov decision processes (MDPs) extend Markov chains by incorporating non-deterministic behaviors. Given an MDP and rewards on states, a classical optimization criterion is the maximal expected total reward where the MDP stops after T steps, which can be computed by a simple dynamic programming algorithm. We consider a natural generalization of the problem where the stopping times can be chosen according to a probability distribution, such that the expected stopping time is T, to optimize the expected total reward. Quite surprisingly we establish inter-reducibility of the expected stopping-time problem for Markov chains with the Positivity problem (which is related to the well-known Skolem problem), for which establishing either decidability or undecidability would be a major breakthrough. Given the hardness of the exact problem, we consider the approximate version of the problem: we show that it can be solved in exponential time for Markov chains and in exponential space for MDPs."}],"article_processing_charge":"Yes","fulldoi":"https://doi.org/10.46298/lmcs-20(4:11)2024","date_published":"2024-11-12T00:00:00Z","oa":1,"isi":1,"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publication_identifier":{"eissn":["1860-5974"]},"scopus_import":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"corr_author":"1","related_material":{"record":[{"relation":"earlier_version","id":"10004","status":"public"}]},"page":"11:1-11:34","publication":"Logical Methods in Computer Science","researchdata_availability":"no","title":"Stochastic processes with expected stopping time","day":"12","alternative_title":["LMCS"],"language":[{"iso":"eng"}],"acknowledgement":"The authors are grateful to the anonymous reviewers of LICS 2021 and of a previous version of this paper for insightful comments that helped improving the presentation. The research presented in this paper was partially supported by the grant ERC CoG 863818 (ForM-SMArt).","DOAJ_listed":"1","volume":20,"type":"journal_article","file":[{"success":1,"date_created":"2024-12-09T08:38:48Z","file_id":"18633","date_updated":"2024-12-09T08:38:48Z","relation":"main_file","file_name":"2024_LMCS_Chatterjee.pdf","creator":"dernst","file_size":416814,"content_type":"application/pdf","access_level":"open_access","checksum":"b3315c74ce18ce0a30ed33d8c9972992"}],"article_type":"original","oa_version":"Published Version","_id":"18630","year":"2024","arxiv":1},{"_id":"18600","oa_version":"Preprint","arxiv":1,"year":"2024","acknowledgement":"The authors are ordered alphabetically. This work was supported by DFG RTG 2236/2 (UnRAVeL) and DFG project TRR 248 (CPEC, ID 389792660), by the EU under MSCA grant agreements 101008233 (MISSION), 101034413 (IST-BRIDGE), and 101067199 (ProSVED), by ERC Starting Grant 101077178 (DEUCE), ERC Consolidator Grant 864075 (CAESAR), and ERC Advanced Grant 834115 (FUN2MODEL), by GAČR grant GA23-06963S (VESCAA), by National Science Foundation grant 1856733, by NextGenerationEU project D53D23008400006 (SMARTITUDE), and by NWO VENI grant 639.021.754.","dataavailabilitystatement":"All model files used for the comparison, as well as the resulting log files, are available at DOI 10.5281/zenodo.8219191","language":[{"iso":"eng"}],"type":"conference","volume":14550,"publication":"TOOLympics Challenge 2023","researchdata_availability":"yes","alternative_title":["LNCS"],"day":"01","title":"Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report","oa":1,"isi":1,"fulldoi":"https://doi.org/10.1007/978-3-031-67695-6_4","date_published":"2024-11-01T00:00:00Z","page":"90-146","related_material":{"record":[{"status":"public","id":"23142","relation":"research_data"}]},"scopus_import":"1","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031676949"]},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publisher":"Springer Nature","main_file_link":[{"url":" https://doi.org/10.48550/arXiv.2405.13583","open_access":"1"}],"abstract":[{"text":"The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused on this setting. Many application scenarios, however, require more advanced property types such as LTL and parameter synthesis queries as well as advanced models like stochastic games and partially observable MDPs. For these, tool support is in its infancy today. This paper presents the outcomes of QComp 2023: a survey of the state of the art in quantitative verification tool support for advanced property types and models. With tools ranging from first research prototypes to well-supported integrations into established toolsets, this report highlights today’s active areas and tomorrow’s challenges in tool-focused research for quantitative verification.","lang":"eng"}],"article_processing_charge":"No","department":[{"_id":"KrCh"}],"citation":{"ista":"Andriushchenko R, Bork A, Budde CE, Češka M, Grover K, Hahn EM, Hartmanns A, Israelsen B, Jansen N, Jeppson J, Junges S, Köhl MA, Könighofer B, Kretinsky J, Meggendorfer T, Parker D, Pranger S, Quatmann T, Ruijters E, Taylor L, Volk M, Weininger M, Zhang Z. 2024. Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report. TOOLympics Challenge 2023. , LNCS, vol. 14550, 90–146.","short":"R. Andriushchenko, A. Bork, C.E. Budde, M. Češka, K. Grover, E.M. Hahn, A. Hartmanns, B. Israelsen, N. Jansen, J. Jeppson, S. Junges, M.A. Köhl, B. Könighofer, J. Kretinsky, T. Meggendorfer, D. Parker, S. Pranger, T. Quatmann, E. Ruijters, L. Taylor, M. Volk, M. Weininger, Z. Zhang, in:, TOOLympics Challenge 2023, Springer Nature, 2024, pp. 90–146.","ama":"Andriushchenko R, Bork A, Budde CE, et al. Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report. In: TOOLympics Challenge 2023. Vol 14550. Springer Nature; 2024:90-146. doi:10.1007/978-3-031-67695-6_4","apa":"Andriushchenko, R., Bork, A., Budde, C. E., Češka, M., Grover, K., Hahn, E. M., … Zhang, Z. (2024). Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report. In TOOLympics Challenge 2023 (Vol. 14550, pp. 90–146). Springer Nature. https://doi.org/10.1007/978-3-031-67695-6_4","ieee":"R. Andriushchenko et al., “Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report,” in TOOLympics Challenge 2023, 2024, vol. 14550, pp. 90–146.","chicago":"Andriushchenko, Roman, Alexander Bork, Carlos E. Budde, Milan Češka, Kush Grover, Ernst Moritz Hahn, Arnd Hartmanns, et al. “Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report.” In TOOLympics Challenge 2023, 14550:90–146. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-67695-6_4.","mla":"Andriushchenko, Roman, et al. “Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report.” TOOLympics Challenge 2023, vol. 14550, Springer Nature, 2024, pp. 90–146, doi:10.1007/978-3-031-67695-6_4."},"author":[{"last_name":"Andriushchenko","full_name":"Andriushchenko, Roman","first_name":"Roman"},{"full_name":"Bork, Alexander","first_name":"Alexander","last_name":"Bork"},{"first_name":"Carlos E.","full_name":"Budde, Carlos E.","last_name":"Budde"},{"full_name":"Češka, Milan","first_name":"Milan","last_name":"Češka"},{"full_name":"Grover, Kush","first_name":"Kush","last_name":"Grover"},{"first_name":"Ernst Moritz","full_name":"Hahn, Ernst Moritz","last_name":"Hahn"},{"full_name":"Hartmanns, Arnd","first_name":"Arnd","last_name":"Hartmanns"},{"full_name":"Israelsen, Bryant","first_name":"Bryant","last_name":"Israelsen"},{"full_name":"Jansen, Nils","first_name":"Nils","last_name":"Jansen"},{"last_name":"Jeppson","first_name":"Joshua","full_name":"Jeppson, Joshua"},{"last_name":"Junges","full_name":"Junges, Sebastian","first_name":"Sebastian"},{"last_name":"Köhl","first_name":"Maximilian A.","full_name":"Köhl, Maximilian A."},{"full_name":"Könighofer, Bettina","first_name":"Bettina","last_name":"Könighofer"},{"full_name":"Kretinsky, Jan","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","last_name":"Kretinsky"},{"orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","last_name":"Meggendorfer","first_name":"Tobias","full_name":"Meggendorfer, Tobias"},{"last_name":"Parker","first_name":"David","full_name":"Parker, David"},{"first_name":"Stefan","full_name":"Pranger, Stefan","last_name":"Pranger"},{"last_name":"Quatmann","first_name":"Tim","full_name":"Quatmann, Tim"},{"full_name":"Ruijters, Enno","first_name":"Enno","last_name":"Ruijters"},{"first_name":"Landon","full_name":"Taylor, Landon","last_name":"Taylor"},{"last_name":"Volk","full_name":"Volk, Matthias","first_name":"Matthias"},{"full_name":"Weininger, Maximilian","first_name":"Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","orcid":"0000-0002-0163-2152","last_name":"Weininger"},{"full_name":"Zhang, Zhen","first_name":"Zhen","last_name":"Zhang"}],"intvolume":" 14550","doi":"10.1007/978-3-031-67695-6_4","quality_controlled":"1","supplementarymaterial":"no","external_id":{"arxiv":["2405.13583"],"isi":["001434957500004"]},"date_created":"2024-12-01T23:01:53Z","das_tickbox":"1","OA_type":"green","status":"public","OA_place":"repository","publication_status":"published","date_updated":"2026-10-16T07:53:26Z","month":"11"}]