--- _id: '14657' abstract: - lang: eng text: 'Natural selection is usually studied between mutants that differ in reproductive rate, but are subject to the same population structure. Here we explore how natural selection acts on mutants that have the same reproductive rate, but different population structures. In our framework, population structure is given by a graph that specifies where offspring can disperse. The invading mutant disperses offspring on a different graph than the resident wild-type. We find that more densely connected dispersal graphs tend to increase the invader’s fixation probability, but the exact relationship between structure and fixation probability is subtle. We present three main results. First, we prove that if both invader and resident are on complete dispersal graphs, then removing a single edge in the invader’s dispersal graph reduces its fixation probability. Second, we show that for certain island models higher invader’s connectivity increases its fixation probability, but the magnitude of the effect depends on the exact layout of the connections. Third, we show that for lattices the effect of different connectivity is comparable to that of different fitness: for large population size, the invader’s fixation probability is either constant or exponentially small, depending on whether it is more or less connected than the resident.' acknowledgement: K.C. acknowledges support from the ERC CoG 863818(ForM-SMArt). J.T. is supported by Center for Foundations ofModern Computer Science (Charles Univ. project UNCE/SCI/004). article_number: '20230355' article_processing_charge: Yes (in subscription journal) article_type: original author: - first_name: Josef full_name: Tkadlec, Josef id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87 last_name: Tkadlec orcid: 0000-0002-1097-9684 - first_name: Kamran full_name: Kaveh, Kamran last_name: Kaveh - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin A. full_name: Nowak, Martin A. last_name: Nowak citation: ama: Tkadlec J, Kaveh K, Chatterjee K, Nowak MA. Evolutionary dynamics of mutants that modify population structure. Journal of the Royal Society, Interface. 2023;20(208). doi:10.1098/rsif.2023.0355 apa: Tkadlec, J., Kaveh, K., Chatterjee, K., & Nowak, M. A. (2023). Evolutionary dynamics of mutants that modify population structure. Journal of the Royal Society, Interface. The Royal Society. https://doi.org/10.1098/rsif.2023.0355 chicago: Tkadlec, Josef, Kamran Kaveh, Krishnendu Chatterjee, and Martin A. Nowak. “Evolutionary Dynamics of Mutants That Modify Population Structure.” Journal of the Royal Society, Interface. The Royal Society, 2023. https://doi.org/10.1098/rsif.2023.0355. ieee: J. Tkadlec, K. Kaveh, K. Chatterjee, and M. A. Nowak, “Evolutionary dynamics of mutants that modify population structure,” Journal of the Royal Society, Interface, vol. 20, no. 208. The Royal Society, 2023. ista: Tkadlec J, Kaveh K, Chatterjee K, Nowak MA. 2023. Evolutionary dynamics of mutants that modify population structure. Journal of the Royal Society, Interface. 20(208), 20230355. mla: Tkadlec, Josef, et al. “Evolutionary Dynamics of Mutants That Modify Population Structure.” Journal of the Royal Society, Interface, vol. 20, no. 208, 20230355, The Royal Society, 2023, doi:10.1098/rsif.2023.0355. short: J. Tkadlec, K. Kaveh, K. Chatterjee, M.A. Nowak, Journal of the Royal Society, Interface 20 (2023). date_created: 2023-12-10T23:00:58Z date_published: 2023-11-29T00:00:00Z date_updated: 2023-12-11T11:17:53Z day: '29' ddc: - '000' - '570' department: - _id: KrCh doi: 10.1098/rsif.2023.0355 ec_funded: 1 external_id: pmid: - '38016637' file: - access_level: open_access checksum: 2eefab13127c7786dbd33303c482a004 content_type: application/pdf creator: dernst date_created: 2023-12-11T11:10:32Z date_updated: 2023-12-11T11:10:32Z file_id: '14673' file_name: 2023_RoyalInterface_Tkadlec.pdf file_size: 1720243 relation: main_file success: 1 file_date_updated: 2023-12-11T11:10:32Z has_accepted_license: '1' intvolume: ' 20' issue: '208' language: - iso: eng month: '11' oa: 1 oa_version: Published Version pmid: 1 project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' publication: Journal of the Royal Society, Interface publication_identifier: eissn: - 1742-5662 publication_status: published publisher: The Royal Society quality_controlled: '1' scopus_import: '1' status: public title: Evolutionary dynamics of mutants that modify population structure tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 20 year: '2023' ... --- _id: '13258' abstract: - lang: eng text: Many human interactions feature the characteristics of social dilemmas where individual actions have consequences for the group and the environment. The feedback between behavior and environment can be studied with the framework of stochastic games. In stochastic games, the state of the environment can change, depending on the choices made by group members. Past work suggests that such feedback can reinforce cooperative behaviors. In particular, cooperation can evolve in stochastic games even if it is infeasible in each separate repeated game. In stochastic games, participants have an interest in conditioning their strategies on the state of the environment. Yet in many applications, precise information about the state could be scarce. Here, we study how the availability of information (or lack thereof) shapes evolution of cooperation. Already for simple examples of two state games we find surprising effects. In some cases, cooperation is only possible if there is precise information about the state of the environment. In other cases, cooperation is most abundant when there is no information about the state of the environment. We systematically analyze all stochastic games of a given complexity class, to determine when receiving information about the environment is better, neutral, or worse for evolution of cooperation. acknowledgement: 'This work was supported by the European Research Council CoG 863818 (ForM-SMArt) (to K.C.), 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 Sklodowska-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.).' article_number: '4153' article_processing_charge: Yes article_type: original author: - first_name: Maria full_name: Kleshnina, Maria id: 4E21749C-F248-11E8-B48F-1D18A9856A87 last_name: Kleshnina - first_name: Christian full_name: Hilbe, Christian id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87 last_name: Hilbe orcid: 0000-0001-5116-955X - first_name: Stepan full_name: Simsa, Stepan id: 409d615c-2f95-11ee-b934-90a352102c1e last_name: Simsa orcid: 0000-0001-6687-1210 - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin A. full_name: Nowak, Martin A. last_name: Nowak citation: ama: Kleshnina M, Hilbe C, Simsa S, Chatterjee K, Nowak MA. The effect of environmental information on evolution of cooperation in stochastic games. Nature Communications. 2023;14. doi:10.1038/s41467-023-39625-9 apa: Kleshnina, M., Hilbe, C., Simsa, S., Chatterjee, K., & Nowak, M. A. (2023). The effect of environmental information on evolution of cooperation in stochastic games. Nature Communications. Springer Nature. https://doi.org/10.1038/s41467-023-39625-9 chicago: Kleshnina, Maria, Christian Hilbe, Stepan Simsa, Krishnendu Chatterjee, and Martin A. Nowak. “The Effect of Environmental Information on Evolution of Cooperation in Stochastic Games.” Nature Communications. Springer Nature, 2023. https://doi.org/10.1038/s41467-023-39625-9. ieee: M. Kleshnina, C. Hilbe, S. Simsa, K. Chatterjee, and M. A. Nowak, “The effect of environmental information on evolution of cooperation in stochastic games,” Nature Communications, vol. 14. Springer Nature, 2023. ista: Kleshnina M, Hilbe C, Simsa S, Chatterjee K, Nowak MA. 2023. The effect of environmental information on evolution of cooperation in stochastic games. Nature Communications. 14, 4153. mla: Kleshnina, Maria, et al. “The Effect of Environmental Information on Evolution of Cooperation in Stochastic Games.” Nature Communications, vol. 14, 4153, Springer Nature, 2023, doi:10.1038/s41467-023-39625-9. short: M. Kleshnina, C. Hilbe, S. Simsa, K. Chatterjee, M.A. Nowak, Nature Communications 14 (2023). date_created: 2023-07-23T22:01:11Z date_published: 2023-07-12T00:00:00Z date_updated: 2023-12-13T11:42:38Z day: '12' ddc: - '000' department: - _id: KrCh doi: 10.1038/s41467-023-39625-9 ec_funded: 1 external_id: isi: - '001029450400031' pmid: - '37438341' file: - access_level: open_access checksum: 5aceefdfe76686267b93ae4fe81899f1 content_type: application/pdf creator: dernst date_created: 2023-07-31T11:32:36Z date_updated: 2023-07-31T11:32:36Z file_id: '13337' file_name: 2023_NatureComm_Kleshnina.pdf file_size: 1601682 relation: main_file success: 1 file_date_updated: 2023-07-31T11:32:36Z has_accepted_license: '1' intvolume: ' 14' isi: 1 language: - iso: eng month: '07' oa: 1 oa_version: Published Version pmid: 1 project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' - _id: 260C2330-B435-11E9-9278-68D0E5697425 call_identifier: H2020 grant_number: '754411' name: ISTplus - Postdoctoral Fellowships publication: Nature Communications publication_identifier: eissn: - 2041-1723 publication_status: published publisher: Springer Nature quality_controlled: '1' related_material: record: - id: '13336' relation: research_data status: public scopus_import: '1' status: public title: The effect of environmental information on evolution of cooperation in stochastic games tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 14 year: '2023' ... --- _id: '13336' article_processing_charge: No author: - first_name: Maria full_name: Kleshnina, Maria id: 4E21749C-F248-11E8-B48F-1D18A9856A87 last_name: Kleshnina citation: ama: 'Kleshnina M. kleshnina/stochgames_info: The effect of environmental information on evolution of cooperation in stochastic games. 2023. doi:10.5281/ZENODO.8059564' apa: 'Kleshnina, M. (2023). kleshnina/stochgames_info: The effect of environmental information on evolution of cooperation in stochastic games. Zenodo. https://doi.org/10.5281/ZENODO.8059564' chicago: 'Kleshnina, Maria. “Kleshnina/Stochgames_info: The Effect of Environmental Information on Evolution of Cooperation in Stochastic Games.” Zenodo, 2023. https://doi.org/10.5281/ZENODO.8059564.' ieee: 'M. Kleshnina, “kleshnina/stochgames_info: The effect of environmental information on evolution of cooperation in stochastic games.” Zenodo, 2023.' ista: 'Kleshnina M. 2023. kleshnina/stochgames_info: The effect of environmental information on evolution of cooperation in stochastic games, Zenodo, 10.5281/ZENODO.8059564.' mla: 'Kleshnina, Maria. Kleshnina/Stochgames_info: The Effect of Environmental Information on Evolution of Cooperation in Stochastic Games. Zenodo, 2023, doi:10.5281/ZENODO.8059564.' short: M. Kleshnina, (2023). date_created: 2023-07-31T11:30:46Z date_published: 2023-06-20T00:00:00Z date_updated: 2023-12-13T11:42:37Z day: '20' ddc: - '000' department: - _id: KrCh doi: 10.5281/ZENODO.8059564 main_file_link: - open_access: '1' url: https://doi.org/10.5281/zenodo.8059564 month: '06' oa: 1 oa_version: Published Version publisher: Zenodo related_material: record: - id: '13258' relation: used_in_publication status: public status: public title: 'kleshnina/stochgames_info: The effect of environmental information on evolution of cooperation in stochastic games' type: research_data_reference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2023' ... --- _id: '13967' abstract: - lang: eng text: 'A classic solution technique for Markov decision processes (MDP) and stochastic games (SG) is value iteration (VI). Due to its good practical performance, this approximative approach is typically preferred over exact techniques, even though no practical bounds on the imprecision of the result could be given until recently. As a consequence, even the most used model checkers could return arbitrarily wrong results. Over the past decade, different works derived stopping criteria, indicating when the precision reaches the desired level, for various settings, in particular MDP with reachability, total reward, and mean payoff, and SG with reachability.In this paper, we provide the first stopping criteria for VI on SG with total reward and mean payoff, yielding the first anytime algorithms in these settings. To this end, we provide the solution in two flavours: First through a reduction to the MDP case and second directly on SG. The former is simpler and automatically utilizes any advances on MDP. The latter allows for more local computations, heading towards better practical efficiency.Our solution unifies the previously mentioned approaches for MDP and SG and their underlying ideas. To achieve this, we isolate objective-specific subroutines as well as identify objective-independent concepts. These structural concepts, while surprisingly simple, form the very essence of the unified solution.' acknowledgement: This research was funded in part by DFG projects 383882557 “SUV” and 427755713 “GOPro”. article_processing_charge: No author: - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Tobias full_name: Meggendorfer, Tobias id: b21b0c15-30a2-11eb-80dc-f13ca25802e1 last_name: Meggendorfer orcid: 0000-0002-1712-2165 - first_name: Maximilian full_name: Weininger, Maximilian id: 02ab0197-cc70-11ed-ab61-918e71f56881 last_name: Weininger citation: ama: 'Kretinsky J, Meggendorfer T, Weininger M. Stopping criteria for value iteration on stochastic games with quantitative objectives. In: 38th Annual ACM/IEEE Symposium on Logic in Computer Science. Vol 2023. Institute of Electrical and Electronics Engineers; 2023. doi:10.1109/LICS56636.2023.10175771' apa: 'Kretinsky, J., Meggendorfer, T., & Weininger, M. (2023). Stopping criteria for value iteration on stochastic games with quantitative objectives. In 38th Annual ACM/IEEE Symposium on Logic in Computer Science (Vol. 2023). Boston, MA, United States: Institute of Electrical and Electronics Engineers. https://doi.org/10.1109/LICS56636.2023.10175771' chicago: Kretinsky, Jan, Tobias Meggendorfer, and Maximilian Weininger. “Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives.” In 38th Annual ACM/IEEE Symposium on Logic in Computer Science, Vol. 2023. Institute of Electrical and Electronics Engineers, 2023. https://doi.org/10.1109/LICS56636.2023.10175771. ieee: J. Kretinsky, T. Meggendorfer, and M. Weininger, “Stopping criteria for value iteration on stochastic games with quantitative objectives,” in 38th Annual ACM/IEEE Symposium on Logic in Computer Science, Boston, MA, United States, 2023, vol. 2023. ista: 'Kretinsky J, Meggendorfer T, Weininger M. 2023. Stopping criteria for value iteration on stochastic games with quantitative objectives. 38th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Symposium on Logic in Computer Science vol. 2023.' mla: Kretinsky, Jan, et al. “Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives.” 38th Annual ACM/IEEE Symposium on Logic in Computer Science, vol. 2023, Institute of Electrical and Electronics Engineers, 2023, doi:10.1109/LICS56636.2023.10175771. short: J. Kretinsky, T. Meggendorfer, M. Weininger, in:, 38th Annual ACM/IEEE Symposium on Logic in Computer Science, Institute of Electrical and Electronics Engineers, 2023. conference: end_date: 2023-06-29 location: Boston, MA, United States name: 'LICS: Symposium on Logic in Computer Science' start_date: 2023-06-26 date_created: 2023-08-06T22:01:10Z date_published: 2023-07-01T00:00:00Z date_updated: 2023-12-13T12:06:10Z day: '01' department: - _id: KrCh doi: 10.1109/LICS56636.2023.10175771 external_id: arxiv: - '2304.09930' isi: - '001036707700042' intvolume: ' 2023' isi: 1 language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.48550/arXiv.2304.09930 month: '07' oa: 1 oa_version: Preprint publication: 38th Annual ACM/IEEE Symposium on Logic in Computer Science publication_identifier: isbn: - '9798350335873' issn: - 1043-6871 publication_status: published publisher: Institute of Electrical and Electronics Engineers quality_controlled: '1' scopus_import: '1' status: public title: Stopping criteria for value iteration on stochastic games with quantitative objectives type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 2023 year: '2023' ... --- _id: '12833' abstract: - lang: eng text: 'The input to the token swapping problem is a graph with vertices v1, v2, . . . , vn, and n tokens with labels 1,2, . . . , n, one on each vertex. The goal is to get token i to vertex vi for all i= 1, . . . , n using a minimum number of swaps, where a swap exchanges the tokens on the endpoints of an edge.Token swapping on a tree, also known as “sorting with a transposition tree,” is not known to be in P nor NP-complete. We present some partial results: 1. An optimum swap sequence may need to perform a swap on a leaf vertex that has the correct token (a “happy leaf”), disproving a conjecture of Vaughan. 2. Any algorithm that fixes happy leaves—as all known approximation algorithms for the problem do—has approximation factor at least 4/3. Furthermore, the two best-known 2-approximation algorithms have approximation factor exactly 2. 3. A generalized problem—weighted coloured token swapping—is NP-complete on trees, but solvable in polynomial time on paths and stars. In this version, tokens and vertices have colours, and colours have weights. The goal is to get every token to a vertex of the same colour, and the cost of a swap is the sum of the weights of the two tokens involved.' acknowledgement: "This work was begun at the University of Waterloo and was partially supported by the Natural Sciences and Engineering Council of Canada (NSERC).\r\n" article_number: '9' article_processing_charge: No article_type: original author: - first_name: Ahmad full_name: Biniaz, Ahmad last_name: Biniaz - first_name: Kshitij full_name: Jain, Kshitij last_name: Jain - first_name: Anna full_name: Lubiw, Anna last_name: Lubiw - first_name: Zuzana full_name: Masárová, Zuzana id: 45CFE238-F248-11E8-B48F-1D18A9856A87 last_name: Masárová orcid: 0000-0002-6660-1322 - first_name: Tillmann full_name: Miltzow, Tillmann last_name: Miltzow - first_name: Debajyoti full_name: Mondal, Debajyoti last_name: Mondal - first_name: Anurag Murty full_name: Naredla, Anurag Murty last_name: Naredla - first_name: Josef full_name: Tkadlec, Josef id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87 last_name: Tkadlec orcid: 0000-0002-1097-9684 - first_name: Alexi full_name: Turcotte, Alexi last_name: Turcotte citation: ama: Biniaz A, Jain K, Lubiw A, et al. Token swapping on trees. Discrete Mathematics and Theoretical Computer Science. 2023;24(2). doi:10.46298/DMTCS.8383 apa: Biniaz, A., Jain, K., Lubiw, A., Masárová, Z., Miltzow, T., Mondal, D., … Turcotte, A. (2023). Token swapping on trees. Discrete Mathematics and Theoretical Computer Science. EPI Sciences. https://doi.org/10.46298/DMTCS.8383 chicago: Biniaz, Ahmad, Kshitij Jain, Anna Lubiw, Zuzana Masárová, Tillmann Miltzow, Debajyoti Mondal, Anurag Murty Naredla, Josef Tkadlec, and Alexi Turcotte. “Token Swapping on Trees.” Discrete Mathematics and Theoretical Computer Science. EPI Sciences, 2023. https://doi.org/10.46298/DMTCS.8383. ieee: A. Biniaz et al., “Token swapping on trees,” Discrete Mathematics and Theoretical Computer Science, vol. 24, no. 2. EPI Sciences, 2023. ista: Biniaz A, Jain K, Lubiw A, Masárová Z, Miltzow T, Mondal D, Naredla AM, Tkadlec J, Turcotte A. 2023. Token swapping on trees. Discrete Mathematics and Theoretical Computer Science. 24(2), 9. mla: Biniaz, Ahmad, et al. “Token Swapping on Trees.” Discrete Mathematics and Theoretical Computer Science, vol. 24, no. 2, 9, EPI Sciences, 2023, doi:10.46298/DMTCS.8383. short: A. Biniaz, K. Jain, A. Lubiw, Z. Masárová, T. Miltzow, D. Mondal, A.M. Naredla, J. Tkadlec, A. Turcotte, Discrete Mathematics and Theoretical Computer Science 24 (2023). date_created: 2023-04-16T22:01:08Z date_published: 2023-01-18T00:00:00Z date_updated: 2024-01-04T12:42:09Z day: '18' ddc: - '000' department: - _id: KrCh - _id: HeEd - _id: UlWa doi: 10.46298/DMTCS.8383 external_id: arxiv: - '1903.06981' file: - access_level: open_access checksum: 439102ea4f6e2aeefd7107dfb9ccf532 content_type: application/pdf creator: dernst date_created: 2023-04-17T08:10:28Z date_updated: 2023-04-17T08:10:28Z file_id: '12844' file_name: 2022_DMTCS_Biniaz.pdf file_size: 2072197 relation: main_file success: 1 file_date_updated: 2023-04-17T08:10:28Z has_accepted_license: '1' intvolume: ' 24' issue: '2' language: - iso: eng month: '01' oa: 1 oa_version: Published Version publication: Discrete Mathematics and Theoretical Computer Science publication_identifier: eissn: - 1365-8050 issn: - 1462-7264 publication_status: published publisher: EPI Sciences quality_controlled: '1' related_material: record: - id: '7950' relation: earlier_version status: public scopus_import: '1' status: public title: Token swapping on trees tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 24 year: '2023' ... --- _id: '14736' abstract: - lang: eng text: Payment channel networks (PCNs) are a promising technology to improve the scalability of cryptocurrencies. PCNs, however, face the challenge that the frequent usage of certain routes may deplete channels in one direction, and hence prevent further transactions. In order to reap the full potential of PCNs, recharging and rebalancing mechanisms are required to provision channels, as well as an admission control logic to decide which transactions to reject in case capacity is insufficient. This paper presents a formal model of this optimisation problem. In particular, we consider an online algorithms perspective, where transactions arrive over time in an unpredictable manner. Our main contributions are competitive online algorithms which come with provable guarantees over time. We empirically evaluate our algorithms on randomly generated transactions to compare the average performance of our algorithms to our theoretical bounds. We also show how this model and approach differs from related problems in classic communication networks. acknowledgement: Supported by the German Federal Ministry of Education and Research (BMBF), grant 16KISK020K (6G-RIC), 2021–2025, and ERC CoG 863818 (ForM-SMArt). alternative_title: - LNCS article_processing_charge: No author: - first_name: Mahsa full_name: Bastankhah, Mahsa last_name: Bastankhah - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Mohammad Ali full_name: Maddah-Ali, Mohammad Ali last_name: Maddah-Ali - first_name: Stefan full_name: Schmid, Stefan last_name: Schmid - first_name: Jakub full_name: Svoboda, Jakub id: 130759D2-D7DD-11E9-87D2-DE0DE6697425 last_name: Svoboda orcid: 0000-0002-1419-3267 - first_name: Michelle X full_name: Yeo, Michelle X id: 2D82B818-F248-11E8-B48F-1D18A9856A87 last_name: Yeo citation: ama: 'Bastankhah M, Chatterjee K, Maddah-Ali MA, Schmid S, Svoboda J, Yeo MX. R2: Boosting liquidity in payment channel networks with online admission control. In: 27th International Conference on Financial Cryptography and Data Security. Vol 13950. Springer Nature; 2023:309-325. doi:10.1007/978-3-031-47754-6_18' apa: 'Bastankhah, M., Chatterjee, K., Maddah-Ali, M. A., Schmid, S., Svoboda, J., & Yeo, M. X. (2023). R2: Boosting liquidity in payment channel networks with online admission control. In 27th International Conference on Financial Cryptography and Data Security (Vol. 13950, pp. 309–325). Bol, Brac, Croatia: Springer Nature. https://doi.org/10.1007/978-3-031-47754-6_18' chicago: 'Bastankhah, Mahsa, Krishnendu Chatterjee, Mohammad Ali Maddah-Ali, Stefan Schmid, Jakub Svoboda, and Michelle X Yeo. “R2: Boosting Liquidity in Payment Channel Networks with Online Admission Control.” In 27th International Conference on Financial Cryptography and Data Security, 13950:309–25. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-47754-6_18.' ieee: 'M. Bastankhah, K. Chatterjee, M. A. Maddah-Ali, S. Schmid, J. Svoboda, and M. X. Yeo, “R2: Boosting liquidity in payment channel networks with online admission control,” in 27th International Conference on Financial Cryptography and Data Security, Bol, Brac, Croatia, 2023, vol. 13950, pp. 309–325.' ista: 'Bastankhah M, Chatterjee K, Maddah-Ali MA, Schmid S, Svoboda J, Yeo MX. 2023. R2: Boosting liquidity in payment channel networks with online admission control. 27th International Conference on Financial Cryptography and Data Security. FC: Financial Cryptography and Data Security, LNCS, vol. 13950, 309–325.' mla: 'Bastankhah, Mahsa, et al. “R2: Boosting Liquidity in Payment Channel Networks with Online Admission Control.” 27th International Conference on Financial Cryptography and Data Security, vol. 13950, Springer Nature, 2023, pp. 309–25, doi:10.1007/978-3-031-47754-6_18.' short: M. Bastankhah, K. Chatterjee, M.A. Maddah-Ali, S. Schmid, J. Svoboda, M.X. Yeo, in:, 27th International Conference on Financial Cryptography and Data Security, Springer Nature, 2023, pp. 309–325. conference: end_date: 2023-05-05 location: Bol, Brac, Croatia name: 'FC: Financial Cryptography and Data Security' start_date: 2023-05-01 date_created: 2024-01-08T09:30:22Z date_published: 2023-12-01T00:00:00Z date_updated: 2024-01-08T09:36:36Z day: '01' department: - _id: KrCh - _id: KrPi doi: 10.1007/978-3-031-47754-6_18 ec_funded: 1 intvolume: ' 13950' language: - iso: eng month: '12' oa_version: None page: 309-325 project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' publication: 27th International Conference on Financial Cryptography and Data Security publication_identifier: eisbn: - '9783031477546' eissn: - 1611-3349 isbn: - '9783031477539' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' status: public title: 'R2: Boosting liquidity in payment channel networks with online admission control' type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 13950 year: '2023' ... --- _id: '14539' abstract: - lang: eng text: "Stochastic systems provide a formal framework for modelling and quantifying uncertainty in systems and have been widely adopted in many application domains. Formal\r\nverification and control of finite state stochastic systems, a subfield of formal methods\r\nalso known as probabilistic model checking, is well studied. In contrast, formal verification and control of infinite state stochastic systems have received comparatively\r\nless attention. However, infinite state stochastic systems commonly arise in practice.\r\nFor instance, probabilistic models that contain continuous probability distributions such\r\nas normal or uniform, or stochastic dynamical systems which are a classical model for\r\ncontrol under uncertainty, both give rise to infinite state systems.\r\nThe goal of this thesis is to contribute to laying theoretical and algorithmic foundations\r\nof fully automated formal verification and control of infinite state stochastic systems,\r\nwith a particular focus on systems that may be executed over a long or infinite time.\r\nWe consider formal verification of infinite state stochastic systems in the setting of\r\nstatic analysis of probabilistic programs and formal control in the setting of controller\r\nsynthesis in stochastic dynamical systems. For both problems, we present some of the\r\nfirst fully automated methods for probabilistic (a.k.a. quantitative) reachability and\r\nsafety analysis applicable to infinite time horizon systems. We also advance the state\r\nof the art of probability 1 (a.k.a. qualitative) reachability analysis for both problems.\r\nFinally, for formal controller synthesis in stochastic dynamical systems, we present a\r\nnovel framework for learning neural network control policies in stochastic dynamical\r\nsystems with formal guarantees on correctness with respect to quantitative reachability,\r\nsafety or reach-avoid specifications.\r\n" alternative_title: - ISTA Thesis article_processing_charge: No author: - first_name: Dorde full_name: Zikelic, Dorde id: 294AA7A6-F248-11E8-B48F-1D18A9856A87 last_name: Zikelic orcid: 0000-0002-4681-1699 citation: ama: Zikelic D. Automated verification and control of infinite state stochastic systems. 2023. doi:10.15479/14539 apa: Zikelic, D. (2023). Automated verification and control of infinite state stochastic systems. Institute of Science and Technology Austria. https://doi.org/10.15479/14539 chicago: Zikelic, Dorde. “Automated Verification and Control of Infinite State Stochastic Systems.” Institute of Science and Technology Austria, 2023. https://doi.org/10.15479/14539. ieee: D. Zikelic, “Automated verification and control of infinite state stochastic systems,” Institute of Science and Technology Austria, 2023. ista: Zikelic D. 2023. Automated verification and control of infinite state stochastic systems. Institute of Science and Technology Austria. mla: Zikelic, Dorde. Automated Verification and Control of Infinite State Stochastic Systems. Institute of Science and Technology Austria, 2023, doi:10.15479/14539. short: D. Zikelic, Automated Verification and Control of Infinite State Stochastic Systems, Institute of Science and Technology Austria, 2023. date_created: 2023-11-15T13:39:10Z date_published: 2023-11-15T00:00:00Z date_updated: 2024-01-16T11:58:15Z day: '15' ddc: - '000' degree_awarded: PhD department: - _id: KrCh - _id: GradSch doi: 10.15479/14539 ec_funded: 1 file: - access_level: open_access checksum: f23e002b0059ca78e1fbb864da52dd7e content_type: application/pdf creator: cchlebak date_created: 2023-11-15T13:43:28Z date_updated: 2023-11-15T13:43:28Z file_id: '14540' file_name: main.pdf file_size: 2116426 relation: main_file success: 1 - access_level: closed checksum: 80ca37618a3c7b59866875f8be9b15ed content_type: application/x-zip-compressed creator: cchlebak date_created: 2023-11-15T13:44:24Z date_updated: 2023-11-15T13:44:24Z file_id: '14541' file_name: thesis_source.zip file_size: 35884057 relation: source_file file_date_updated: 2023-11-15T13:44:24Z language: - iso: eng month: '11' oa: 1 oa_version: Published Version page: '256' project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' - _id: 2564DBCA-B435-11E9-9278-68D0E5697425 call_identifier: H2020 grant_number: '665385' name: International IST Doctoral Program publication_identifier: isbn: - 978-3-99078-036-7 issn: - 2663 - 337X publication_status: published publisher: Institute of Science and Technology Austria related_material: record: - id: '1194' relation: part_of_dissertation status: public - id: '12000' relation: part_of_dissertation status: public - id: '9644' relation: part_of_dissertation status: public - id: '12511' relation: part_of_dissertation status: public - id: '14600' relation: part_of_dissertation status: public - id: '14601' relation: part_of_dissertation status: public - id: '10414' relation: part_of_dissertation status: public status: public supervisor: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X title: Automated verification and control of infinite state stochastic systems tmp: image: /images/cc_by_nc_sa.png legal_code_url: https://creativecommons.org/licenses/by-nc-sa/4.0/legalcode name: Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International (CC BY-NC-SA 4.0) short: CC BY-NC-SA (4.0) type: dissertation user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9 year: '2023' ... --- _id: '14778' abstract: - lang: eng text: 'We consider the almost-sure (a.s.) termination problem for probabilistic programs, which are a stochastic extension of classical imperative programs. Lexicographic ranking functions provide a sound and practical approach for termination of non-probabilistic programs, and their extension to probabilistic programs is achieved via lexicographic ranking supermartingales (LexRSMs). However, LexRSMs introduced in the previous work have a limitation that impedes their automation: all of their components have to be non-negative in all reachable states. This might result in a LexRSM not existing even for simple terminating programs. Our contributions are twofold. First, we introduce a generalization of LexRSMs that allows for some components to be negative. This standard feature of non-probabilistic termination proofs was hitherto not known to be sound in the probabilistic setting, as the soundness proof requires a careful analysis of the underlying stochastic process. Second, we present polynomial-time algorithms using our generalized LexRSMs for proving a.s. termination in broad classes of linear-arithmetic programs.' acknowledgement: This research was partially supported by the ERC CoG (grant no. 863818; ForM-SMArt), the Czech Science Foundation (grant no. GA21-24711S), and the European Union’s Horizon 2020 research and innovation program under the Marie Skłodowska-Curie Grant Agreement No. 665385. article_number: '11' article_processing_charge: Yes (via OA deal) article_type: original author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Ehsan full_name: Kafshdar Goharshady, Ehsan last_name: Kafshdar Goharshady - first_name: Petr full_name: Novotný, Petr id: 3CC3B868-F248-11E8-B48F-1D18A9856A87 last_name: Novotný - first_name: Jiří full_name: Zárevúcky, Jiří last_name: Zárevúcky - first_name: Dorde full_name: Zikelic, Dorde id: 294AA7A6-F248-11E8-B48F-1D18A9856A87 last_name: Zikelic orcid: 0000-0002-4681-1699 citation: ama: Chatterjee K, Kafshdar Goharshady E, Novotný P, Zárevúcky J, Zikelic D. On lexicographic proof rules for probabilistic termination. Formal Aspects of Computing. 2023;35(2). doi:10.1145/3585391 apa: Chatterjee, K., Kafshdar Goharshady, E., Novotný, P., Zárevúcky, J., & Zikelic, D. (2023). On lexicographic proof rules for probabilistic termination. Formal Aspects of Computing. Association for Computing Machinery. https://doi.org/10.1145/3585391 chicago: Chatterjee, Krishnendu, Ehsan Kafshdar Goharshady, Petr Novotný, Jiří Zárevúcky, and Dorde Zikelic. “On Lexicographic Proof Rules for Probabilistic Termination.” Formal Aspects of Computing. Association for Computing Machinery, 2023. https://doi.org/10.1145/3585391. ieee: K. Chatterjee, E. Kafshdar Goharshady, P. Novotný, J. Zárevúcky, and D. Zikelic, “On lexicographic proof rules for probabilistic termination,” Formal Aspects of Computing, vol. 35, no. 2. Association for Computing Machinery, 2023. ista: Chatterjee K, Kafshdar Goharshady E, Novotný P, Zárevúcky J, Zikelic D. 2023. On lexicographic proof rules for probabilistic termination. Formal Aspects of Computing. 35(2), 11. mla: Chatterjee, Krishnendu, et al. “On Lexicographic Proof Rules for Probabilistic Termination.” Formal Aspects of Computing, vol. 35, no. 2, 11, Association for Computing Machinery, 2023, doi:10.1145/3585391. short: K. Chatterjee, E. Kafshdar Goharshady, P. Novotný, J. Zárevúcky, D. Zikelic, Formal Aspects of Computing 35 (2023). date_created: 2024-01-10T09:27:43Z date_published: 2023-06-23T00:00:00Z date_updated: 2024-01-17T08:19:41Z day: '23' ddc: - '000' department: - _id: KrCh doi: 10.1145/3585391 ec_funded: 1 external_id: arxiv: - '2108.02188' file: - access_level: open_access checksum: 3bb133eeb27ec01649a9a36445d952d9 content_type: application/pdf creator: dernst date_created: 2024-01-16T08:11:24Z date_updated: 2024-01-16T08:11:24Z file_id: '14804' file_name: 2023_FormalAspectsComputing_Chatterjee.pdf file_size: 502522 relation: main_file success: 1 file_date_updated: 2024-01-16T08:11:24Z has_accepted_license: '1' intvolume: ' 35' issue: '2' keyword: - Theoretical Computer Science - Software language: - iso: eng month: '06' oa: 1 oa_version: Published Version project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' - _id: 2564DBCA-B435-11E9-9278-68D0E5697425 call_identifier: H2020 grant_number: '665385' name: International IST Doctoral Program publication: Formal Aspects of Computing publication_identifier: eissn: - 1433-299X issn: - 0934-5043 publication_status: published publisher: Association for Computing Machinery quality_controlled: '1' related_material: record: - id: '10414' relation: earlier_version status: public status: public title: On lexicographic proof rules for probabilistic termination tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 35 year: '2023' ... --- _id: '14456' abstract: - lang: eng text: In this paper, we present novel algorithms that efficiently compute a shortest reconfiguration sequence between two given dominating sets in trees and interval graphs under the TOKEN SLIDING model. In this problem, a graph is provided along with its two dominating sets, which can be imagined as tokens placed on vertices. The objective is to find a shortest sequence of dominating sets that transforms one set into the other, with each set in the sequence resulting from sliding a single token in the previous set. While identifying any sequence has been well studied, our work presents the first polynomial algorithms for this optimization variant in the context of dominating sets. alternative_title: - LNCS article_processing_charge: No author: - first_name: Jan Matyáš full_name: Křišťan, Jan Matyáš last_name: Křišťan - first_name: Jakub full_name: Svoboda, Jakub id: 130759D2-D7DD-11E9-87D2-DE0DE6697425 last_name: Svoboda orcid: 0000-0002-1419-3267 citation: ama: 'Křišťan JM, Svoboda J. Shortest dominating set reconfiguration under token sliding. In: 24th International Symposium on Fundamentals of Computation Theory. Vol 14292. Springer Nature; 2023:333-347. doi:10.1007/978-3-031-43587-4_24' apa: 'Křišťan, J. M., & Svoboda, J. (2023). Shortest dominating set reconfiguration under token sliding. In 24th International Symposium on Fundamentals of Computation Theory (Vol. 14292, pp. 333–347). Trier, Germany: Springer Nature. https://doi.org/10.1007/978-3-031-43587-4_24' chicago: Křišťan, Jan Matyáš, and Jakub Svoboda. “Shortest Dominating Set Reconfiguration under Token Sliding.” In 24th International Symposium on Fundamentals of Computation Theory, 14292:333–47. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-43587-4_24. ieee: J. M. Křišťan and J. Svoboda, “Shortest dominating set reconfiguration under token sliding,” in 24th International Symposium on Fundamentals of Computation Theory, Trier, Germany, 2023, vol. 14292, pp. 333–347. ista: 'Křišťan JM, Svoboda J. 2023. Shortest dominating set reconfiguration under token sliding. 24th International Symposium on Fundamentals of Computation Theory. FCT: Fundamentals of Computation Theory, LNCS, vol. 14292, 333–347.' mla: Křišťan, Jan Matyáš, and Jakub Svoboda. “Shortest Dominating Set Reconfiguration under Token Sliding.” 24th International Symposium on Fundamentals of Computation Theory, vol. 14292, Springer Nature, 2023, pp. 333–47, doi:10.1007/978-3-031-43587-4_24. short: J.M. Křišťan, J. Svoboda, in:, 24th International Symposium on Fundamentals of Computation Theory, Springer Nature, 2023, pp. 333–347. conference: end_date: 2023-09-21 location: Trier, Germany name: 'FCT: Fundamentals of Computation Theory' start_date: 2023-09-18 date_created: 2023-10-29T23:01:16Z date_published: 2023-09-21T00:00:00Z date_updated: 2024-01-22T08:10:49Z day: '21' department: - _id: KrCh doi: 10.1007/978-3-031-43587-4_24 external_id: arxiv: - '2307.10847' intvolume: ' 14292' language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.48550/arXiv.2307.10847 month: '09' oa: 1 oa_version: Preprint page: 333-347 publication: 24th International Symposium on Fundamentals of Computation Theory publication_identifier: eissn: - 1611-3349 isbn: - '9783031435867' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' related_material: link: - relation: erratum url: https://doi.org/10.1007/978-3-031-43587-4_31 scopus_import: '1' status: public title: Shortest dominating set reconfiguration under token sliding type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 14292 year: '2023' ... --- _id: '14830' abstract: - lang: eng text: We study the problem of learning controllers for discrete-time non-linear stochastic dynamical systems with formal reach-avoid guarantees. This work presents the first method for providing formal reach-avoid guarantees, which combine and generalize stability and safety guarantees, with a tolerable probability threshold p in [0,1] over the infinite time horizon. Our method leverages advances in machine learning literature and it represents formal certificates as neural networks. In particular, we learn a certificate in the form of a reach-avoid supermartingale (RASM), a novel notion that we introduce in this work. Our RASMs provide reachability and avoidance guarantees by imposing constraints on what can be viewed as a stochastic extension of level sets of Lyapunov functions for deterministic systems. Our approach solves several important problems -- it can be used to learn a control policy from scratch, to verify a reach-avoid specification for a fixed control policy, or to fine-tune a pre-trained policy if it does not satisfy the reach-avoid specification. We validate our approach on 3 stochastic non-linear reinforcement learning tasks. acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385. article_processing_charge: No author: - first_name: Dorde full_name: Zikelic, Dorde id: 294AA7A6-F248-11E8-B48F-1D18A9856A87 last_name: Zikelic orcid: 0000-0002-4681-1699 - first_name: Mathias full_name: Lechner, Mathias id: 3DC22916-F248-11E8-B48F-1D18A9856A87 last_name: Lechner - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X citation: ama: 'Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies for stochastic systems with reach-avoid guarantees. In: Proceedings of the 37th AAAI Conference on Artificial Intelligence. Vol 37. Association for the Advancement of Artificial Intelligence; 2023:11926-11935. doi:10.1609/aaai.v37i10.26407' apa: 'Zikelic, D., Lechner, M., Henzinger, T. A., & Chatterjee, K. (2023). Learning control policies for stochastic systems with reach-avoid guarantees. In Proceedings of the 37th AAAI Conference on Artificial Intelligence (Vol. 37, pp. 11926–11935). Washington, DC, United States: Association for the Advancement of Artificial Intelligence. https://doi.org/10.1609/aaai.v37i10.26407' chicago: Zikelic, Dorde, Mathias Lechner, Thomas A Henzinger, and Krishnendu Chatterjee. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” In Proceedings of the 37th AAAI Conference on Artificial Intelligence, 37:11926–35. Association for the Advancement of Artificial Intelligence, 2023. https://doi.org/10.1609/aaai.v37i10.26407. ieee: D. Zikelic, M. Lechner, T. A. Henzinger, and K. Chatterjee, “Learning control policies for stochastic systems with reach-avoid guarantees,” in Proceedings of the 37th AAAI Conference on Artificial Intelligence, Washington, DC, United States, 2023, vol. 37, no. 10, pp. 11926–11935. ista: 'Zikelic D, Lechner M, Henzinger TA, Chatterjee K. 2023. Learning control policies for stochastic systems with reach-avoid guarantees. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 37, 11926–11935.' mla: Zikelic, Dorde, et al. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” Proceedings of the 37th AAAI Conference on Artificial Intelligence, vol. 37, no. 10, Association for the Advancement of Artificial Intelligence, 2023, pp. 11926–35, doi:10.1609/aaai.v37i10.26407. short: D. Zikelic, M. Lechner, T.A. Henzinger, K. Chatterjee, in:, Proceedings of the 37th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2023, pp. 11926–11935. conference: end_date: 2023-02-14 location: Washington, DC, United States name: 'AAAI: Conference on Artificial Intelligence' start_date: 2023-02-07 date_created: 2024-01-18T07:44:31Z date_published: 2023-06-26T00:00:00Z date_updated: 2024-01-22T14:08:29Z day: '26' department: - _id: ToHe - _id: KrCh doi: 10.1609/aaai.v37i10.26407 ec_funded: 1 external_id: arxiv: - '2210.05308' intvolume: ' 37' issue: '10' keyword: - General Medicine language: - iso: eng month: '06' oa_version: Preprint page: 11926-11935 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' - _id: 2564DBCA-B435-11E9-9278-68D0E5697425 call_identifier: H2020 grant_number: '665385' name: International IST Doctoral Program publication: Proceedings of the 37th AAAI Conference on Artificial Intelligence publication_identifier: eissn: - 2374-3468 issn: - 2159-5399 publication_status: published publisher: Association for the Advancement of Artificial Intelligence quality_controlled: '1' related_material: record: - id: '14600' relation: earlier_version status: public status: public title: Learning control policies for stochastic systems with reach-avoid guarantees type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 37 year: '2023' ... --- _id: '13139' abstract: - lang: eng text: A classical problem for Markov chains is determining their stationary (or steady-state) distribution. This problem has an equally classical solution based on eigenvectors and linear equation systems. However, this approach does not scale to large instances, and iterative solutions are desirable. It turns out that a naive approach, as used by current model checkers, may yield completely wrong results. We present a new approach, which utilizes recent advances in partial exploration and mean payoff computation to obtain a correct, converging approximation. alternative_title: - LNCS article_processing_charge: No author: - first_name: Tobias full_name: Meggendorfer, Tobias id: b21b0c15-30a2-11eb-80dc-f13ca25802e1 last_name: Meggendorfer orcid: 0000-0002-1712-2165 citation: ama: 'Meggendorfer T. Correct approximation of stationary distributions. In: TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems. Vol 13993. Springer Nature; 2023:489-507. doi:10.1007/978-3-031-30823-9_25' apa: 'Meggendorfer, T. (2023). Correct approximation of stationary distributions. In TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems (Vol. 13993, pp. 489–507). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30823-9_25' chicago: 'Meggendorfer, Tobias. “Correct Approximation of Stationary Distributions.” In TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, 13993:489–507. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30823-9_25.' ieee: 'T. Meggendorfer, “Correct approximation of stationary distributions,” in TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, Paris, France, 2023, vol. 13993, pp. 489–507.' ista: 'Meggendorfer T. 2023. Correct approximation of stationary distributions. TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13993, 489–507.' mla: 'Meggendorfer, Tobias. “Correct Approximation of Stationary Distributions.” TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, vol. 13993, Springer Nature, 2023, pp. 489–507, doi:10.1007/978-3-031-30823-9_25.' short: 'T. Meggendorfer, in:, TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023, pp. 489–507.' conference: end_date: 2023-04-27 location: Paris, France name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems' start_date: 2023-04-22 date_created: 2023-06-18T22:00:46Z date_published: 2023-04-22T00:00:00Z date_updated: 2024-02-27T07:19:33Z day: '22' ddc: - '000' department: - _id: KrCh doi: 10.1007/978-3-031-30823-9_25 external_id: arxiv: - '2301.08137' file: - access_level: open_access checksum: 59f707a3949c03793251b0d04c62542a content_type: application/pdf creator: dernst date_created: 2023-06-19T07:18:40Z date_updated: 2023-06-19T07:18:40Z file_id: '13148' file_name: 2023_LNCS_Meggendorfer.pdf file_size: 521951 relation: main_file success: 1 file_date_updated: 2023-06-19T07:18:40Z has_accepted_license: '1' intvolume: ' 13993' language: - iso: eng month: '04' oa: 1 oa_version: Published Version page: 489-507 publication: 'TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems' publication_identifier: eissn: - 1611-3349 isbn: - '9783031308222' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' related_material: record: - id: '14990' relation: research_data status: public scopus_import: '1' status: public title: Correct approximation of stationary distributions tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 13993 year: '2023' ... --- _id: '14990' abstract: - lang: eng text: The software artefact to evaluate the approximation of stationary distributions implementation. article_processing_charge: No author: - first_name: Tobias full_name: Meggendorfer, Tobias id: b21b0c15-30a2-11eb-80dc-f13ca25802e1 last_name: Meggendorfer orcid: 0000-0002-1712-2165 citation: ama: 'Meggendorfer T. Artefact for: Correct Approximation of Stationary Distributions. 2023. doi:10.5281/ZENODO.7548214' apa: 'Meggendorfer, T. (2023). Artefact for: Correct Approximation of Stationary Distributions. Zenodo. https://doi.org/10.5281/ZENODO.7548214' chicago: 'Meggendorfer, Tobias. “Artefact for: Correct Approximation of Stationary Distributions.” Zenodo, 2023. https://doi.org/10.5281/ZENODO.7548214.' ieee: 'T. Meggendorfer, “Artefact for: Correct Approximation of Stationary Distributions.” Zenodo, 2023.' ista: 'Meggendorfer T. 2023. Artefact for: Correct Approximation of Stationary Distributions, Zenodo, 10.5281/ZENODO.7548214.' mla: 'Meggendorfer, Tobias. Artefact for: Correct Approximation of Stationary Distributions. Zenodo, 2023, doi:10.5281/ZENODO.7548214.' short: T. Meggendorfer, (2023). date_created: 2024-02-14T14:27:06Z date_published: 2023-01-18T00:00:00Z date_updated: 2024-02-27T07:19:32Z day: '18' ddc: - '000' department: - _id: KrCh doi: 10.5281/ZENODO.7548214 has_accepted_license: '1' main_file_link: - open_access: '1' url: https://doi.org/10.5281/zenodo.7548214 month: '01' oa: 1 oa_version: Published Version publisher: Zenodo related_material: record: - id: '13139' relation: used_in_publication status: public status: public title: 'Artefact for: Correct Approximation of Stationary Distributions' tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: research_data_reference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2023' ... --- _id: '15023' abstract: - lang: eng text: Reinforcement learning has shown promising results in learning neural network policies for complicated control tasks. However, the lack of formal guarantees about the behavior of such policies remains an impediment to their deployment. We propose a novel method for learning a composition of neural network policies in stochastic environments, along with a formal certificate which guarantees that a specification over the policy's behavior is satisfied with the desired probability. Unlike prior work on verifiable RL, our approach leverages the compositional nature of logical specifications provided in SpectRL, to learn over graphs of probabilistic reach-avoid specifications. The formal guarantees are provided by learning neural network policies together with reach-avoid supermartingales (RASM) for the graph’s sub-tasks and then composing them into a global policy. We also derive a tighter lower bound compared to previous work on the probability of reach-avoidance implied by a RASM, which is required to find a compositional policy with an acceptable probabilistic threshold for complex tasks with multiple edge policies. We implement a prototype of our approach and evaluate it on a Stochastic Nine Rooms environment. acknowledgement: "This work was supported in part by the ERC-2020-AdG 101020093 (VAMOS) and the ERC-2020-\r\nCoG 863818 (FoRM-SMArt)." article_processing_charge: No author: - first_name: Dorde full_name: Zikelic, Dorde id: 294AA7A6-F248-11E8-B48F-1D18A9856A87 last_name: Zikelic orcid: 0000-0002-4681-1699 - first_name: Mathias full_name: Lechner, Mathias id: 3DC22916-F248-11E8-B48F-1D18A9856A87 last_name: Lechner - first_name: Abhinav full_name: Verma, Abhinav id: a235593c-d7fa-11eb-a0c5-b22ca3c66ee6 last_name: Verma - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 citation: ama: 'Zikelic D, Lechner M, Verma A, Chatterjee K, Henzinger TA. Compositional policy learning in stochastic control systems with formal guarantees. In: 37th Conference on Neural Information Processing Systems. ; 2023.' apa: Zikelic, D., Lechner, M., Verma, A., Chatterjee, K., & Henzinger, T. A. (2023). Compositional policy learning in stochastic control systems with formal guarantees. In 37th Conference on Neural Information Processing Systems. New Orleans, LO, United States. chicago: Zikelic, Dorde, Mathias Lechner, Abhinav Verma, Krishnendu Chatterjee, and Thomas A Henzinger. “Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees.” In 37th Conference on Neural Information Processing Systems, 2023. ieee: D. Zikelic, M. Lechner, A. Verma, K. Chatterjee, and T. A. Henzinger, “Compositional policy learning in stochastic control systems with formal guarantees,” in 37th Conference on Neural Information Processing Systems, New Orleans, LO, United States, 2023. ista: 'Zikelic D, Lechner M, Verma A, Chatterjee K, Henzinger TA. 2023. Compositional policy learning in stochastic control systems with formal guarantees. 37th Conference on Neural Information Processing Systems. NeurIPS: Neural Information Processing Systems.' mla: Zikelic, Dorde, et al. “Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees.” 37th Conference on Neural Information Processing Systems, 2023. short: D. Zikelic, M. Lechner, A. Verma, K. Chatterjee, T.A. Henzinger, in:, 37th Conference on Neural Information Processing Systems, 2023. conference: end_date: 2023-12-16 location: New Orleans, LO, United States name: 'NeurIPS: Neural Information Processing Systems' start_date: 2023-12-10 date_created: 2024-02-25T09:23:24Z date_published: 2023-12-15T00:00:00Z date_updated: 2024-02-28T12:20:11Z day: '15' department: - _id: ToHe - _id: KrCh ec_funded: 1 external_id: arxiv: - '2312.01456' language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.48550/arXiv.2312.01456 month: '12' oa: 1 oa_version: Preprint project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: 37th Conference on Neural Information Processing Systems publication_status: epub_ahead quality_controlled: '1' status: public title: Compositional policy learning in stochastic control systems with formal guarantees type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2023' ... --- _id: '12102' abstract: - lang: eng text: 'Given a Markov chain M = (V, v_0, δ), with state space V and a starting state v_0, and a probability threshold ε, an ε-core is a subset C of states that is left with probability at most ε. More formally, C ⊆ V is an ε-core, iff ℙ[reach (V\C)] ≤ ε. Cores have been applied in a wide variety of verification problems over Markov chains, Markov decision processes, and probabilistic programs, as a means of discarding uninteresting and low-probability parts of a probabilistic system and instead being able to focus on the states that are likely to be encountered in a real-world run. In this work, we focus on the problem of computing a minimal ε-core in a Markov chain. Our contributions include both negative and positive results: (i) We show that the decision problem on the existence of an ε-core of a given size is NP-complete. This solves an open problem posed in [Jan Kretínský and Tobias Meggendorfer, 2020]. We additionally show that the problem remains NP-complete even when limited to acyclic Markov chains with bounded maximal vertex degree; (ii) We provide a polynomial time algorithm for computing a minimal ε-core on Markov chains over control-flow graphs of structured programs. A straightforward combination of our algorithm with standard branch prediction techniques allows one to apply the idea of cores to find a subset of program lines that are left with low probability and then focus any desired static analysis on this core subset.' acknowledgement: "The research was partially supported by the Hong Kong Research Grants Council ECS\r\nProject No. 26208122, ERC CoG 863818 (FoRM-SMArt), the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385, HKUST– Kaisa Joint Research Institute Project Grant HKJRI3A-055 and HKUST Startup Grant R9272. Ali Ahmadi and Roodabeh Safavi were interns at HKUST." article_number: '29' article_processing_charge: No author: - first_name: Ali full_name: Ahmadi, Ali last_name: Ahmadi - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Amir Kafshdar full_name: Goharshady, Amir Kafshdar id: 391365CE-F248-11E8-B48F-1D18A9856A87 last_name: Goharshady orcid: 0000-0003-1702-6584 - first_name: Tobias full_name: Meggendorfer, Tobias id: b21b0c15-30a2-11eb-80dc-f13ca25802e1 last_name: Meggendorfer orcid: 0000-0002-1712-2165 - first_name: Roodabeh full_name: Safavi Hemami, Roodabeh id: 72ed2640-8972-11ed-ae7b-f9c81ec75154 last_name: Safavi Hemami - first_name: Dorde full_name: Zikelic, Dorde id: 294AA7A6-F248-11E8-B48F-1D18A9856A87 last_name: Zikelic citation: ama: 'Ahmadi A, Chatterjee K, Goharshady AK, Meggendorfer T, Safavi Hemami R, Zikelic D. Algorithms and hardness results for computing cores of Markov chains. In: 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Vol 250. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2022. doi:10.4230/LIPIcs.FSTTCS.2022.29' apa: 'Ahmadi, A., Chatterjee, K., Goharshady, A. K., Meggendorfer, T., Safavi Hemami, R., & Zikelic, D. (2022). Algorithms and hardness results for computing cores of Markov chains. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (Vol. 250). Madras, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.FSTTCS.2022.29' chicago: Ahmadi, Ali, Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, Roodabeh Safavi Hemami, and Dorde Zikelic. “Algorithms and Hardness Results for Computing Cores of Markov Chains.” In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Vol. 250. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. https://doi.org/10.4230/LIPIcs.FSTTCS.2022.29. ieee: A. Ahmadi, K. Chatterjee, A. K. Goharshady, T. Meggendorfer, R. Safavi Hemami, and D. Zikelic, “Algorithms and hardness results for computing cores of Markov chains,” in 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Madras, India, 2022, vol. 250. ista: 'Ahmadi A, Chatterjee K, Goharshady AK, Meggendorfer T, Safavi Hemami R, Zikelic D. 2022. Algorithms and hardness results for computing cores of Markov chains. 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. FSTTC: Foundations of Software Technology and Theoretical Computer Science vol. 250, 29.' mla: Ahmadi, Ali, et al. “Algorithms and Hardness Results for Computing Cores of Markov Chains.” 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, vol. 250, 29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, doi:10.4230/LIPIcs.FSTTCS.2022.29. short: A. Ahmadi, K. Chatterjee, A.K. Goharshady, T. Meggendorfer, R. Safavi Hemami, D. Zikelic, in:, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. conference: end_date: 2022-12-20 location: Madras, India name: 'FSTTC: Foundations of Software Technology and Theoretical Computer Science' start_date: 2022-12-18 date_created: 2023-01-01T23:00:50Z date_published: 2022-12-14T00:00:00Z date_updated: 2023-02-07T09:19:43Z day: '14' ddc: - '000' department: - _id: KrCh - _id: GradSch doi: 10.4230/LIPIcs.FSTTCS.2022.29 ec_funded: 1 file: - access_level: open_access checksum: 6660c802489013f034c9e8bd57f4d46e content_type: application/pdf creator: dernst date_created: 2023-01-20T10:39:44Z date_updated: 2023-01-20T10:39:44Z file_id: '12324' file_name: 2022_LIPICs_Ahmadi.pdf file_size: 872534 relation: main_file success: 1 file_date_updated: 2023-01-20T10:39:44Z has_accepted_license: '1' intvolume: ' 250' language: - iso: eng month: '12' oa: 1 oa_version: Published Version project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' - _id: 2564DBCA-B435-11E9-9278-68D0E5697425 call_identifier: H2020 grant_number: '665385' name: International IST Doctoral Program publication: 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science publication_identifier: isbn: - '9783959772617' issn: - 1868-8969 publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik quality_controlled: '1' scopus_import: '1' status: public title: Algorithms and hardness results for computing cores of Markov chains tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 250 year: '2022' ... --- _id: '12101' abstract: - lang: eng text: 'Spatial games form a widely-studied class of games from biology and physics modeling the evolution of social behavior. Formally, such a game is defined by a square (d by d) payoff matrix M and an undirected graph G. Each vertex of G represents an individual, that initially follows some strategy i ∈ {1,2,…,d}. In each round of the game, every individual plays the matrix game with each of its neighbors: An individual following strategy i meeting a neighbor following strategy j receives a payoff equal to the entry (i,j) of M. Then, each individual updates its strategy to its neighbors'' strategy with the highest sum of payoffs, and the next round starts. The basic computational problems consist of reachability between configurations and the average frequency of a strategy. For general spatial games and graphs, these problems are in PSPACE. In this paper, we examine restricted setting: the game is a prisoner’s dilemma; and G is a subgraph of grid. We prove that basic computational problems for spatial games with prisoner’s dilemma on a subgraph of a grid are PSPACE-hard.' acknowledgement: "Krishnendu Chatterjee: The research was partially supported by the ERC CoG 863818\r\n(ForM-SMArt).\r\nIsmaël Jecker: The research was partially supported by the ERC grant 950398 (INFSYS).\r\nJakub Svoboda: The research was partially supported by the ERC CoG 863818 (ForM-SMArt)" article_number: 11:1-11:14 article_processing_charge: No author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Rasmus full_name: Ibsen-Jensen, Rasmus id: 3B699956-F248-11E8-B48F-1D18A9856A87 last_name: Ibsen-Jensen orcid: 0000-0003-4783-0389 - first_name: Ismael R full_name: Jecker, Ismael R id: 85D7C63E-7D5D-11E9-9C0F-98C4E5697425 last_name: Jecker - first_name: Jakub full_name: Svoboda, Jakub id: 130759D2-D7DD-11E9-87D2-DE0DE6697425 last_name: Svoboda citation: ama: 'Chatterjee K, Ibsen-Jensen R, Jecker IR, Svoboda J. Complexity of spatial games. In: 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Vol 250. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2022. doi:10.4230/LIPIcs.FSTTCS.2022.11' apa: 'Chatterjee, K., Ibsen-Jensen, R., Jecker, I. R., & Svoboda, J. (2022). Complexity of spatial games. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (Vol. 250). Madras, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.FSTTCS.2022.11' chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Ismael R Jecker, and Jakub Svoboda. “Complexity of Spatial Games.” In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Vol. 250. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. https://doi.org/10.4230/LIPIcs.FSTTCS.2022.11. ieee: K. Chatterjee, R. Ibsen-Jensen, I. R. Jecker, and J. Svoboda, “Complexity of spatial games,” in 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Madras, India, 2022, vol. 250. ista: 'Chatterjee K, Ibsen-Jensen R, Jecker IR, Svoboda J. 2022. Complexity of spatial games. 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. FSTTC: Foundations of Software Technology and Theoretical Computer Science vol. 250, 11:1-11:14.' mla: Chatterjee, Krishnendu, et al. “Complexity of Spatial Games.” 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, vol. 250, 11:1-11:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, doi:10.4230/LIPIcs.FSTTCS.2022.11. short: K. Chatterjee, R. Ibsen-Jensen, I.R. Jecker, J. Svoboda, in:, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. conference: end_date: 2022-12-20 location: Madras, India name: 'FSTTC: Foundations of Software Technology and Theoretical Computer Science' start_date: 2022-12-18 date_created: 2023-01-01T23:00:50Z date_published: 2022-12-14T00:00:00Z date_updated: 2023-02-13T09:06:43Z day: '14' ddc: - '000' department: - _id: KrCh doi: 10.4230/LIPIcs.FSTTCS.2022.11 ec_funded: 1 file: - access_level: open_access checksum: a21e3ba2421e2c4a06aa2cb6d530ede1 content_type: application/pdf creator: dernst date_created: 2023-01-20T10:19:19Z date_updated: 2023-01-20T10:19:19Z file_id: '12323' file_name: 2022_LIPICs_Chatterjee.pdf file_size: 657396 relation: main_file success: 1 file_date_updated: 2023-01-20T10:19:19Z has_accepted_license: '1' intvolume: ' 250' language: - iso: eng month: '12' oa: 1 oa_version: Published Version project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' publication: 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science publication_identifier: isbn: - '9783959772617' issn: - 1868-8969 publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik quality_controlled: '1' scopus_import: '1' status: public title: Complexity of spatial games tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 250 year: '2022' ... --- _id: '12568' abstract: - lang: eng text: We treat the problem of risk-aware control for stochastic shortest path (SSP) on Markov decision processes (MDP). Typically, expectation is considered for SSP, which however is oblivious to the incurred risk. We present an alternative view, instead optimizing conditional value-at-risk (CVaR), an established risk measure. We treat both Markov chains as well as MDP and introduce, through novel insights, two algorithms, based on linear programming and value iteration, respectively. Both algorithms offer precise and provably correct solutions. Evaluation of our prototype implementation shows that risk-aware control is feasible on several moderately sized models. article_processing_charge: No author: - first_name: Tobias full_name: Meggendorfer, Tobias id: b21b0c15-30a2-11eb-80dc-f13ca25802e1 last_name: Meggendorfer orcid: 0000-0002-1712-2165 citation: ama: 'Meggendorfer T. Risk-aware stochastic shortest path. In: Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022. Vol 36. Association for the Advancement of Artificial Intelligence; 2022:9858-9867. doi:10.1609/aaai.v36i9.21222' apa: 'Meggendorfer, T. (2022). Risk-aware stochastic shortest path. In Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022 (Vol. 36, pp. 9858–9867). Virtual: Association for the Advancement of Artificial Intelligence. https://doi.org/10.1609/aaai.v36i9.21222' chicago: Meggendorfer, Tobias. “Risk-Aware Stochastic Shortest Path.” In Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022, 36:9858–67. Association for the Advancement of Artificial Intelligence, 2022. https://doi.org/10.1609/aaai.v36i9.21222. ieee: T. Meggendorfer, “Risk-aware stochastic shortest path,” in Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022, Virtual, 2022, vol. 36, no. 9, pp. 9858–9867. ista: Meggendorfer T. 2022. Risk-aware stochastic shortest path. Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022. Conference on Artificial Intelligence vol. 36, 9858–9867. mla: Meggendorfer, Tobias. “Risk-Aware Stochastic Shortest Path.” Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022, vol. 36, no. 9, Association for the Advancement of Artificial Intelligence, 2022, pp. 9858–67, doi:10.1609/aaai.v36i9.21222. short: T. Meggendorfer, in:, Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022, Association for the Advancement of Artificial Intelligence, 2022, pp. 9858–9867. conference: end_date: 2022-03-01 location: Virtual name: Conference on Artificial Intelligence start_date: 2022-02-22 date_created: 2023-02-19T23:00:56Z date_published: 2022-06-28T00:00:00Z date_updated: 2023-02-20T07:19:12Z day: '28' department: - _id: KrCh doi: 10.1609/aaai.v36i9.21222 external_id: arxiv: - '2203.01640' intvolume: ' 36' issue: '9' language: - iso: eng main_file_link: - open_access: '1' url: ' https://doi.org/10.48550/arXiv.2203.01640' month: '06' oa: 1 oa_version: Preprint page: 9858-9867 publication: Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022 publication_identifier: eissn: - 2374-3468 isbn: - '1577358767' publication_status: published publisher: Association for the Advancement of Artificial Intelligence quality_controlled: '1' scopus_import: '1' status: public title: Risk-aware stochastic shortest path type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 36 year: '2022' ... --- _id: '11938' abstract: - lang: eng text: A matching is compatible to two or more labeled point sets of size n with labels {1, . . . , n} if its straight-line drawing on each of these point sets is crossing-free. We study the maximum number of edges in a matching compatible to two or more labeled point sets in general position in the plane. We show that for any two labeled sets of n points in convex position there exists a compatible matching with ⌊√2n + 1 − 1⌋ edges. More generally, for any ℓ labeled point sets we construct compatible matchings of size Ω(n1/ℓ). As a corresponding upper bound, we use probabilistic arguments to show that for any ℓ given sets of n points there exists a labeling of each set such that the largest compatible matching has O(n2/(ℓ+1)) edges. Finally, we show that Θ(log n) copies of any set of n points are necessary and sufficient for the existence of labelings of these point sets such that any compatible matching consists only of a single edge. acknowledgement: 'A.A. funded by the Marie Sklodowska-Curie grant agreement No 754411. Z.M. partially funded by Wittgenstein Prize, Austrian Science Fund (FWF), grant no. Z 342-N31. I.P., D.P., and B.V. partially supported by FWF within the collaborative DACH project Arrangements and Drawings as FWF project I 3340-N35. A.P. supported by a Schrödinger fellowship of the FWF: J-3847-N35. J.T. partially supported by ERC Start grant no. (279307: Graph Games), FWF grant no. P23499-N23 and S11407-N23 (RiSE).' article_processing_charge: No article_type: original author: - first_name: Oswin full_name: Aichholzer, Oswin last_name: Aichholzer - first_name: Alan M full_name: Arroyo Guevara, Alan M id: 3207FDC6-F248-11E8-B48F-1D18A9856A87 last_name: Arroyo Guevara orcid: 0000-0003-2401-8670 - first_name: Zuzana full_name: Masárová, Zuzana id: 45CFE238-F248-11E8-B48F-1D18A9856A87 last_name: Masárová orcid: 0000-0002-6660-1322 - first_name: Irene full_name: Parada, Irene last_name: Parada - first_name: Daniel full_name: Perz, Daniel last_name: Perz - first_name: Alexander full_name: Pilz, Alexander last_name: Pilz - first_name: Josef full_name: Tkadlec, Josef id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87 last_name: Tkadlec orcid: 0000-0002-1097-9684 - first_name: Birgit full_name: Vogtenhuber, Birgit last_name: Vogtenhuber citation: ama: Aichholzer O, Arroyo Guevara AM, Masárová Z, et al. On compatible matchings. Journal of Graph Algorithms and Applications. 2022;26(2):225-240. doi:10.7155/jgaa.00591 apa: Aichholzer, O., Arroyo Guevara, A. M., Masárová, Z., Parada, I., Perz, D., Pilz, A., … Vogtenhuber, B. (2022). On compatible matchings. Journal of Graph Algorithms and Applications. Brown University. https://doi.org/10.7155/jgaa.00591 chicago: Aichholzer, Oswin, Alan M Arroyo Guevara, Zuzana Masárová, Irene Parada, Daniel Perz, Alexander Pilz, Josef Tkadlec, and Birgit Vogtenhuber. “On Compatible Matchings.” Journal of Graph Algorithms and Applications. Brown University, 2022. https://doi.org/10.7155/jgaa.00591. ieee: O. Aichholzer et al., “On compatible matchings,” Journal of Graph Algorithms and Applications, vol. 26, no. 2. Brown University, pp. 225–240, 2022. ista: Aichholzer O, Arroyo Guevara AM, Masárová Z, Parada I, Perz D, Pilz A, Tkadlec J, Vogtenhuber B. 2022. On compatible matchings. Journal of Graph Algorithms and Applications. 26(2), 225–240. mla: Aichholzer, Oswin, et al. “On Compatible Matchings.” Journal of Graph Algorithms and Applications, vol. 26, no. 2, Brown University, 2022, pp. 225–40, doi:10.7155/jgaa.00591. short: O. Aichholzer, A.M. Arroyo Guevara, Z. Masárová, I. Parada, D. Perz, A. Pilz, J. Tkadlec, B. Vogtenhuber, Journal of Graph Algorithms and Applications 26 (2022) 225–240. date_created: 2022-08-21T22:01:56Z date_published: 2022-06-01T00:00:00Z date_updated: 2023-02-23T13:54:21Z day: '01' ddc: - '000' department: - _id: UlWa - _id: HeEd - _id: KrCh doi: 10.7155/jgaa.00591 ec_funded: 1 external_id: arxiv: - '2101.03928' file: - access_level: open_access checksum: dc6e255e3558faff924fd9e370886c11 content_type: application/pdf creator: dernst date_created: 2022-08-22T06:42:42Z date_updated: 2022-08-22T06:42:42Z file_id: '11940' file_name: 2022_JourGraphAlgorithmsApplic_Aichholzer.pdf file_size: 694538 relation: main_file success: 1 file_date_updated: 2022-08-22T06:42:42Z has_accepted_license: '1' intvolume: ' 26' issue: '2' language: - iso: eng month: '06' oa: 1 oa_version: Published Version page: 225-240 project: - _id: 260C2330-B435-11E9-9278-68D0E5697425 call_identifier: H2020 grant_number: '754411' name: ISTplus - Postdoctoral Fellowships - _id: 268116B8-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z00342 name: The Wittgenstein Prize - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory publication: Journal of Graph Algorithms and Applications publication_identifier: issn: - 1526-1719 publication_status: published publisher: Brown University quality_controlled: '1' related_material: record: - id: '9296' relation: earlier_version status: public scopus_import: '1' status: public title: On compatible matchings tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 26 year: '2022' ... --- _id: '12677' abstract: - lang: eng text: "In modern sample-driven Prophet Inequality, an adversary chooses a sequence of n items with values v1,v2,…,vn to be presented to a decision maker (DM). The process follows in two phases. In the first phase (sampling phase), some items, possibly selected at random, are revealed to the DM, but she can never accept them. In the second phase, the DM is presented with the other items in a random order and online fashion. For each item, she must make an irrevocable decision to either accept the item and stop the process or reject the item forever and proceed to the next item. The goal of the DM is to maximize the expected value as compared to a Prophet (or offline algorithm) that has access to all information. In this setting, the sampling phase has no cost and is not part of the optimization process. However, in many scenarios, the samples are obtained as part of the decision-making process.\r\nWe model this aspect as a two-phase Prophet Inequality where an adversary chooses a sequence of 2n items with values v1,v2,…,v2n and the items are randomly ordered. Finally, there are two phases of the Prophet Inequality problem with the first n-items and the rest of the items, respectively. We show that some basic algorithms achieve a ratio of at most 0.450. We present an algorithm that achieves a ratio of at least 0.495. Finally, we show that for every algorithm the ratio it can achieve is at most 0.502. Hence our algorithm is near-optimal." acknowledgement: This research was partially supported by the ERC CoG 863818 (ForM-SMArt) grant. article_number: '2209.14368' article_processing_charge: No author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Mona full_name: Mohammadi, Mona id: 4363614d-b686-11ed-a7d5-ac9e4a24bc2e last_name: Mohammadi - first_name: Raimundo J full_name: Saona Urmeneta, Raimundo J id: BD1DF4C4-D767-11E9-B658-BC13E6697425 last_name: Saona Urmeneta orcid: 0000-0001-5103-038X citation: ama: Chatterjee K, Mohammadi M, Saona Urmeneta RJ. Repeated prophet inequality with near-optimal bounds. arXiv. doi:10.48550/ARXIV.2209.14368 apa: Chatterjee, K., Mohammadi, M., & Saona Urmeneta, R. J. (n.d.). Repeated prophet inequality with near-optimal bounds. arXiv. https://doi.org/10.48550/ARXIV.2209.14368 chicago: Chatterjee, Krishnendu, Mona Mohammadi, and Raimundo J Saona Urmeneta. “Repeated Prophet Inequality with Near-Optimal Bounds.” ArXiv, n.d. https://doi.org/10.48550/ARXIV.2209.14368. ieee: K. Chatterjee, M. Mohammadi, and R. J. Saona Urmeneta, “Repeated prophet inequality with near-optimal bounds,” arXiv. . ista: Chatterjee K, Mohammadi M, Saona Urmeneta RJ. Repeated prophet inequality with near-optimal bounds. arXiv, 2209.14368. mla: Chatterjee, Krishnendu, et al. “Repeated Prophet Inequality with Near-Optimal Bounds.” ArXiv, 2209.14368, doi:10.48550/ARXIV.2209.14368. short: K. Chatterjee, M. Mohammadi, R.J. Saona Urmeneta, ArXiv (n.d.). date_created: 2023-02-24T12:21:40Z date_published: 2022-09-28T00:00:00Z date_updated: 2023-02-27T10:07:40Z day: '28' department: - _id: GradSch - _id: KrCh doi: 10.48550/ARXIV.2209.14368 ec_funded: 1 external_id: arxiv: - '2209.14368' language: - iso: eng main_file_link: - open_access: '1' url: ' https://doi.org/10.48550/arXiv.2209.14368' month: '09' oa: 1 oa_version: Preprint project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' publication: arXiv publication_status: submitted status: public title: Repeated prophet inequality with near-optimal bounds type: preprint user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2022' ... --- _id: '10602' abstract: - lang: eng text: Transforming ω-automata into parity automata is traditionally done using appearance records. We present an efficient variant of this idea, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and show that our method produces significantly smaller automata than previous approaches. acknowledgement: This work is partially funded by the German Research Foundation (DFG) projects Verified Model Checkers (No. 317422601) and Statistical Unbounded Verification (No. 383882557), and the Alexander von Humboldt Foundation with funds from the German Federal Ministry of Education and Research. It is an extended version of [21], including all proofs together with further explanations and examples. Moreover, we provide a new, more efficient construction based on (total) preorders, unifying previous optimizations. Experiments are performed with a new, performant implementation, comparing our approach to the current state of the art. article_processing_charge: Yes (via OA deal) article_type: original author: - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Tobias full_name: Meggendorfer, Tobias id: b21b0c15-30a2-11eb-80dc-f13ca25802e1 last_name: Meggendorfer orcid: 0000-0002-1712-2165 - first_name: Clara full_name: Waldmann, Clara last_name: Waldmann - first_name: Maximilian full_name: Weininger, Maximilian last_name: Weininger citation: ama: Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record with preorders. Acta Informatica. 2022;59:585-618. doi:10.1007/s00236-021-00412-y apa: Kretinsky, J., Meggendorfer, T., Waldmann, C., & Weininger, M. (2022). Index appearance record with preorders. Acta Informatica. Springer Nature. https://doi.org/10.1007/s00236-021-00412-y chicago: Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger. “Index Appearance Record with Preorders.” Acta Informatica. Springer Nature, 2022. https://doi.org/10.1007/s00236-021-00412-y. ieee: J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance record with preorders,” Acta Informatica, vol. 59. Springer Nature, pp. 585–618, 2022. ista: Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2022. Index appearance record with preorders. Acta Informatica. 59, 585–618. mla: Kretinsky, Jan, et al. “Index Appearance Record with Preorders.” Acta Informatica, vol. 59, Springer Nature, 2022, pp. 585–618, doi:10.1007/s00236-021-00412-y. short: J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, Acta Informatica 59 (2022) 585–618. date_created: 2022-01-06T12:37:27Z date_published: 2022-10-01T00:00:00Z date_updated: 2023-08-02T13:49:28Z day: '01' ddc: - '000' department: - _id: KrCh doi: 10.1007/s00236-021-00412-y external_id: isi: - '000735765500001' file: - access_level: open_access checksum: bf1c195b6aaf59e8530cf9e3a9d731f7 content_type: application/pdf creator: cchlebak date_created: 2022-01-07T07:50:31Z date_updated: 2022-01-07T07:50:31Z file_id: '10603' file_name: 2021_ActaInfor_Křetínský.pdf file_size: 1066082 relation: main_file success: 1 file_date_updated: 2022-01-07T07:50:31Z has_accepted_license: '1' intvolume: ' 59' isi: 1 keyword: - computer networks and communications - information systems - software language: - iso: eng month: '10' oa: 1 oa_version: Published Version page: 585-618 project: - _id: B67AFEDC-15C9-11EA-A837-991A96BB2854 name: IST Austria Open Access Fund publication: Acta Informatica publication_identifier: eissn: - 1432-0525 issn: - 0001-5903 publication_status: published publisher: Springer Nature quality_controlled: '1' scopus_import: '1' status: public title: Index appearance record with preorders tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8 volume: 59 year: '2022' ... --- _id: '10731' abstract: - lang: eng text: Motivated by COVID-19, we develop and analyze a simple stochastic model for the spread of disease in human population. We track how the number of infected and critically ill people develops over time in order to estimate the demand that is imposed on the hospital system. To keep this demand under control, we consider a class of simple policies for slowing down and reopening society and we compare their efficiency in mitigating the spread of the virus from several different points of view. We find that in order to avoid overwhelming of the hospital system, a policy must impose a harsh lockdown or it must react swiftly (or both). While reacting swiftly is universally beneficial, being harsh pays off only when the country is patient about reopening and when the neighboring countries coordinate their mitigation efforts. Our work highlights the importance of acting decisively when closing down and the importance of patience and coordination between neighboring countries when reopening. acknowledgement: 'K.C. acknowledges support from ERC Consolidator Grant No. (863818: ForM-SMart). A.P. acknowledges support from FWF Grant No. J-4220. M.A.N. acknowledges support from Office of Naval Research grant N00014-16-1-2914 and from the John Templeton Foundation.' article_number: '1526' article_processing_charge: No article_type: original author: - first_name: Jakub full_name: Svoboda, Jakub id: 130759D2-D7DD-11E9-87D2-DE0DE6697425 last_name: Svoboda - first_name: Josef full_name: Tkadlec, Josef last_name: Tkadlec - first_name: Andreas full_name: Pavlogiannis, Andreas id: 49704004-F248-11E8-B48F-1D18A9856A87 last_name: Pavlogiannis orcid: 0000-0002-8943-0722 - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin A. full_name: Nowak, Martin A. last_name: Nowak citation: ama: Svoboda J, Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. Infection dynamics of COVID-19 virus under lockdown and reopening. Scientific Reports. 2022;12(1). doi:10.1038/s41598-022-05333-5 apa: Svoboda, J., Tkadlec, J., Pavlogiannis, A., Chatterjee, K., & Nowak, M. A. (2022). Infection dynamics of COVID-19 virus under lockdown and reopening. Scientific Reports. Springer Nature. https://doi.org/10.1038/s41598-022-05333-5 chicago: Svoboda, Jakub, Josef Tkadlec, Andreas Pavlogiannis, Krishnendu Chatterjee, and Martin A. Nowak. “Infection Dynamics of COVID-19 Virus under Lockdown and Reopening.” Scientific Reports. Springer Nature, 2022. https://doi.org/10.1038/s41598-022-05333-5. ieee: J. Svoboda, J. Tkadlec, A. Pavlogiannis, K. Chatterjee, and M. A. Nowak, “Infection dynamics of COVID-19 virus under lockdown and reopening,” Scientific Reports, vol. 12, no. 1. Springer Nature, 2022. ista: Svoboda J, Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. 2022. Infection dynamics of COVID-19 virus under lockdown and reopening. Scientific Reports. 12(1), 1526. mla: Svoboda, Jakub, et al. “Infection Dynamics of COVID-19 Virus under Lockdown and Reopening.” Scientific Reports, vol. 12, no. 1, 1526, Springer Nature, 2022, doi:10.1038/s41598-022-05333-5. short: J. Svoboda, J. Tkadlec, A. Pavlogiannis, K. Chatterjee, M.A. Nowak, Scientific Reports 12 (2022). date_created: 2022-02-06T23:01:30Z date_published: 2022-01-27T00:00:00Z date_updated: 2023-08-02T14:13:07Z day: '27' ddc: - '570' department: - _id: KrCh doi: 10.1038/s41598-022-05333-5 ec_funded: 1 external_id: arxiv: - '2012.15155' isi: - '000749198000039' file: - access_level: open_access checksum: 247afd30c173390940f099ead35a28ed content_type: application/pdf creator: alisjak date_created: 2022-02-07T14:57:59Z date_updated: 2022-02-07T14:57:59Z file_id: '10744' file_name: 2022_ScientificReports_Svoboda.pdf file_size: 2971922 relation: main_file success: 1 file_date_updated: 2022-02-07T14:57:59Z has_accepted_license: '1' intvolume: ' 12' isi: 1 issue: '1' language: - iso: eng month: '01' oa: 1 oa_version: Published Version project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' publication: Scientific Reports publication_identifier: eissn: - 2045-2322 publication_status: published publisher: Springer Nature quality_controlled: '1' scopus_import: '1' status: public title: Infection dynamics of COVID-19 virus under lockdown and reopening tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8 volume: 12 year: '2022' ...